# Directory talk:Jon Awbrey/Papers/Functional Logic : Higher Order Propositions

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

...

## Work Area

### Discussion

This is a Section for discussion.

### Exploration

This is a Section for pursuing questions I haven't thought out to the end yet.

#### Higher order propositions, group actions and characters

• Character is revealed by action. —Aristotle
<table align="center" border="1" cellpadding="0" cellspacing="0" markdown="1" style="text-align:center">

<caption><font size="+2">$\texttt{Table A3.} \quad \operatorname{E}f ~\texttt{Expanded over Differential Features}~ \{ \operatorname{d}p, \operatorname{d}q \}$</font></caption>

<td>
$\array{ \arrayopts{ \collines{solid} \rowlines{solid solid none none none solid none solid none solid none solid none none none solid}} & \phantom{xxxx} f \phantom{xxxx} & \phantom{xxxx} \array{\operatorname{T}_{11}f \\ \operatorname{E}f|_{\operatorname{d}p ~ \operatorname{d}q} } \phantom{xxxx} & \phantom{xxxx} \array{\operatorname{T}_{10}f \\ \operatorname{E}f|_{\operatorname{d}p ~ \texttt{(} \operatorname{d}q \texttt{)}} } \phantom{xxxx} & \phantom{xxxx} \array{\operatorname{T}_{01}f \\ \operatorname{E}f|_{\texttt{(} \operatorname{d}p \texttt{)} ~ \operatorname{d}q} } \phantom{xxxx} & \phantom{xxxx} \array{\operatorname{T}_{00}f \\ \operatorname{E}f|_{\texttt{(} \operatorname{d}p \texttt{)(} \operatorname{d}q \texttt{)}} } \phantom{xxxx} \\ f_{0} & \texttt{(} ~ \texttt{)} & \texttt{(} ~ \texttt{)} & \texttt{(} ~ \texttt{)} & \texttt{(} ~ \texttt{)} & \texttt{(} ~ \texttt{)} \\ f_{1} & \texttt{(} p \texttt{)(} q \texttt{)} & p ~ q & p ~ \texttt{(} q \texttt{)} & \texttt{(} p \texttt{)} ~ q & \texttt{(} p \texttt{)(} q \texttt{)} \\ f_{2} & \texttt{(} p \texttt{)} ~ q & p ~ \texttt{(} q \texttt{)} & p ~ q & \texttt{(} p \texttt{)(} q \texttt{)} & \texttt{(} p \texttt{)} ~ q \\ f_{4} & p ~ \texttt{(} q \texttt{)} & \texttt{(} p \texttt{)} ~ q & \texttt{(} p \texttt{)(} q \texttt{)} & p ~ q & p ~ \texttt{(} q \texttt{)} \\ f_{8} & p ~ q & \texttt{(} p \texttt{)(} q \texttt{)} & \texttt{(} p \texttt{)} q & p \texttt{(} q \texttt{)} & p ~ q \\ f_{3} & \texttt{(} p \texttt{)} & p & p & \texttt{(} p \texttt{)} & \texttt{(} p \texttt{)} \\ f_{12} & p & \texttt{(} p \texttt{)} & \texttt{(} p \texttt{)} & p & p \\ f_{6} & \texttt{(} p \texttt{,} q \texttt{)} & \texttt{(} p \texttt{,} q \texttt{)} & \texttt{((} p \texttt{,} q \texttt{))} & \texttt{((} p \texttt{,} q \texttt{))} & \texttt{(} p \texttt{,} q \texttt{)} \\ f_{9} & \texttt{((} p \texttt{,} q \texttt{))} & \texttt{((} p \texttt{,} q \texttt{))} & \texttt{(} p \texttt{,} q \texttt{)} & \texttt{(} p \texttt{,} q \texttt{)} & \texttt{((} p \texttt{,} q \texttt{))} \\ f_{5} & \texttt{(} q \texttt{)} & q & \texttt{(} q \texttt{)} & q & \texttt{(} q \texttt{)} \\ f_{10} & q & \texttt{(} q \texttt{)} & q & \texttt{(} q \texttt{)} & q \\ f_{7} & \texttt{(} p ~ q \texttt{)} & \texttt{((} p \texttt{)(} q \texttt{))} & \texttt{((} p \texttt{)} ~ q \texttt{)} & \texttt{(} p ~ \texttt{(} q \texttt{))} & \texttt{(} p ~ q \texttt{)} \\ f_{11} & \texttt{(} p ~ \texttt{(} q \texttt{))} & \texttt{((} p \texttt{)} ~ q \texttt{)} & \texttt{((} p \texttt{)(} q \texttt{))} & \texttt{(} p ~ q \texttt{)} & \texttt{(} p ~ \texttt{(} q \texttt{))} \\ f_{13} & \texttt{((} p \texttt{)} ~ q \texttt{)} & \texttt{(} p ~ \texttt{(} q \texttt{))} & \texttt{(} p ~ q \texttt{)} & \texttt{((} p \texttt{)(} q \texttt{))} & \texttt{((} p \texttt{)} ~ q \texttt{)} \\ f_{14} & \texttt{((} p \texttt{)(} q \texttt{))} & \texttt{(} p ~ q \texttt{)} & \texttt{(} p ~ \texttt{(} q \texttt{))} & \texttt{((} p \texttt{)} ~ q \texttt{)} & \texttt{((} p \texttt{)(} q \texttt{))} \\ f_{15} & \texttt{((} ~ \texttt{))} & \texttt{((} ~ \texttt{))} & \texttt{((} ~ \texttt{))} & \texttt{((} ~ \texttt{))} & \texttt{((} ~ \texttt{))} \\ \cellopts{\colspan{2}} \texttt{Fixed Point Total} & 4 & 4 & 4 & 16 }$

</td></table>

#### Double Duals

TeX Array

<div markdown="1"><font size="+1">
\array{ \arrayopts{\colalign{right}} \alpha_{0} f = 1 & \operatorname{iff} & f_{0} \Rightarrow f & \operatorname{iff} & 0 \Rightarrow f, & \operatorname{hence} & \alpha_{0} f = 1 & \operatorname{for~all} ~ f. \\ \alpha_{15} f = 1 & \operatorname{iff} & f_{15} \Rightarrow f & \operatorname{iff} & 1 \Rightarrow f, & \operatorname{hence} & \alpha_{15} f = 1 & \operatorname{iff} ~ f = 1. \\ \beta_{0} f = 1 & \operatorname{iff} & f \Rightarrow f_{0} & \operatorname{iff} & f \Rightarrow 0, & \operatorname{hence} & \beta_{0} f = 1 & \operatorname{iff} ~ f = 0. \\ \beta_{15} f = 1 & \operatorname{iff} & f \Rightarrow f_{15} & \operatorname{iff} & f \Rightarrow 1, & \operatorname{hence} & \beta_{15} f = 1 & \operatorname{for~all} ~ f. }
</font></div>

HTML Table

<font size="1">
<table align="center" cellpadding="8" cellspacing="0" markdown="1" style="border:none; text-align:right">

<tr>
<td style="border:none">$\alpha_{0} f = 1$</td>
<td style="border:none">$\operatorname{iff}$</td>
<td style="border:none">$f_{0} \Rightarrow f$</td>
<td style="border:none">$\operatorname{iff}$</td>
<td style="border:none">$0 \Rightarrow f,$</td>
<td style="border:none">$\operatorname{hence}$</td>
<td style="border:none">$\alpha_{0} f = 1$</td>
<td style="border:none">$\operatorname{for~all} ~ f.$</td></tr>

<tr>
<td style="border:none">$\alpha_{15} f = 1$</td>
<td style="border:none">$\operatorname{iff}$</td>
<td style="border:none">$f_{15} \Rightarrow f$</td>
<td style="border:none">$\operatorname{iff}$</td>
<td style="border:none">$1 \Rightarrow f,$</td>
<td style="border:none">$\operatorname{hence}$</td>
<td style="border:none">$\alpha_{15} f = 1$</td>
<td style="border:none">$\operatorname{iff} ~ f = 1.$</td></tr>

<tr>
<td style="border:none">$\beta_{0} f = 1$</td>
<td style="border:none">$\operatorname{iff}$</td>
<td style="border:none">$f \Rightarrow f_{0}$</td>
<td style="border:none">$\operatorname{iff}$</td>
<td style="border:none">$f \Rightarrow 0,$</td>
<td style="border:none">$\operatorname{hence}$</td>
<td style="border:none">$\beta_{0} f = 1$</td>
<td style="border:none">$\operatorname{iff} ~ f = 0.$</td></tr>

<tr>
<td style="border:none">$\beta_{15} f = 1$</td>
<td style="border:none">$\operatorname{iff}$</td>
<td style="border:none">$f \Rightarrow f_{15}$</td>
<td style="border:none">$\operatorname{iff}$</td>
<td style="border:none">$f \Rightarrow 1,$</td>
<td style="border:none">$\operatorname{hence}$</td>
<td style="border:none">$\beta_{15} f = 1$</td>
<td style="border:none">$\operatorname{for~all} ~ f.$</td></tr>

</table></font>