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

Notes & Queries

...

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>