Line 601: |
Line 601: |
| <math>(\mathbb{B}^n\ +\!\to \mathbb{B})</math><br> | | <math>(\mathbb{B}^n\ +\!\to \mathbb{B})</math><br> |
| <math>[\mathbb{B}^n]</math> | | <math>[\mathbb{B}^n]</math> |
− | |}<br> | + | |} |
| + | <br> |
| | | |
| ====Differential Propositions==== | | ====Differential Propositions==== |
Line 731: |
Line 732: |
| <math>(\mathbb{D}^n\ +\!\to \mathbb{B})</math><br> | | <math>(\mathbb{D}^n\ +\!\to \mathbb{B})</math><br> |
| <math>[\mathbb{D}^n]</math> | | <math>[\mathbb{D}^n]</math> |
− | |}<br> | + | |} |
| + | <br> |
| | | |
| '''…''' | | '''…''' |
Line 2,078: |
Line 2,080: |
| <br> | | <br> |
| | | |
− | =Work Area 1= | + | =Archive 1= |
| | | |
| {| align="center" border="1" cellpadding="8" cellspacing="0" style="background:lightcyan; text-align:center; width:96%" | | {| align="center" border="1" cellpadding="8" cellspacing="0" style="background:lightcyan; text-align:center; width:96%" |
Line 2,234: |
Line 2,236: |
| <math>(\mathbb{B}^n\ +\!\to \mathbb{B})</math><br> | | <math>(\mathbb{B}^n\ +\!\to \mathbb{B})</math><br> |
| <math>[\mathbb{B}^n]</math> | | <math>[\mathbb{B}^n]</math> |
− | |}<br> | + | |} |
| + | <br> |
| | | |
| A proposition in the tangent universe [E<font face="lucida calligraphy">A</font>] is called a ''differential proposition'' and forms the analogue of a system of differential equations, constraints, or relations in ordinary calculus. | | A proposition in the tangent universe [E<font face="lucida calligraphy">A</font>] is called a ''differential proposition'' and forms the analogue of a system of differential equations, constraints, or relations in ordinary calculus. |
Line 2,308: |
Line 2,311: |
| <math>(\mathbb{D}^n\ +\!\to \mathbb{B})</math><br> | | <math>(\mathbb{D}^n\ +\!\to \mathbb{B})</math><br> |
| <math>[\mathbb{D}^n]</math> | | <math>[\mathbb{D}^n]</math> |
− | |}<br> | + | |} |
| + | <br> |
| | | |
− | =Work Area 2= | + | =Archive 2= |
| | | |
| {| align="center" border="1" cellpadding="4" cellspacing="0" style="font-weight:bold; text-align:center; width:96%" | | {| align="center" border="1" cellpadding="4" cellspacing="0" style="font-weight:bold; text-align:center; width:96%" |
Line 2,339: |
Line 2,343: |
| | <math>f_{0000}\!</math> | | | <math>f_{0000}\!</math> |
| | 0 0 0 0 | | | 0 0 0 0 |
− | | <math>(\!|~|\!)</math> | + | | <math>(~)\!</math> |
| | false | | | false |
| | <math>0\!</math> | | | <math>0\!</math> |
Line 2,346: |
Line 2,350: |
| | <math>f_{0001}\!</math> | | | <math>f_{0001}\!</math> |
| | 0 0 0 1 | | | 0 0 0 1 |
− | | <math>(\!|x|\!)(\!|y|\!)</math> | + | | <math>(x)(y)\!</math> |
| | neither x nor y | | | neither x nor y |
− | | <math>\lnot x \land \lnot y</math> | + | | <math>\lnot x \land \lnot y\!</math> |
| |- | | |- |
| | <math>f_{2}\!</math> | | | <math>f_{2}\!</math> |
| | <math>f_{0010}\!</math> | | | <math>f_{0010}\!</math> |
| | 0 0 1 0 | | | 0 0 1 0 |
− | | <math>(\!|x|\!)\ y</math> | + | | <math>(x)\ y\!</math> |
| | y and not x | | | y and not x |
− | | <math>\lnot x \land y</math> | + | | <math>\lnot x \land y\!</math> |
| |- | | |- |
| | <math>f_{3}\!</math> | | | <math>f_{3}\!</math> |
| | <math>f_{0011}\!</math> | | | <math>f_{0011}\!</math> |
| | 0 0 1 1 | | | 0 0 1 1 |
− | | <math>(\!|x|\!)</math> | + | | <math>(x)\!</math> |
| | not x | | | not x |
− | | <math>\lnot x</math> | + | | <math>\lnot x\!</math> |
| |- | | |- |
| | <math>f_{4}\!</math> | | | <math>f_{4}\!</math> |
| | <math>f_{0100}\!</math> | | | <math>f_{0100}\!</math> |
| | 0 1 0 0 | | | 0 1 0 0 |
− | | <math>x\ (\!|y|\!)</math> | + | | <math>x\ (y)\!</math> |
| | x and not y | | | x and not y |
− | | <math>x \land \lnot y</math> | + | | <math>x \land \lnot y\!</math> |
| |- | | |- |
| | <math>f_{5}\!</math> | | | <math>f_{5}\!</math> |
| | <math>f_{0101}\!</math> | | | <math>f_{0101}\!</math> |
| | 0 1 0 1 | | | 0 1 0 1 |
− | | <math>(\!|y|\!)</math> | + | | <math>(y)\!</math> |
| | not y | | | not y |
− | | <math>\lnot y</math> | + | | <math>\lnot y\!</math> |
| |- | | |- |
| | <math>f_{6}\!</math> | | | <math>f_{6}\!</math> |
| | <math>f_{0110}\!</math> | | | <math>f_{0110}\!</math> |
| | 0 1 1 0 | | | 0 1 1 0 |
− | | <math>(\!|x,\ y|\!)</math> | + | | <math>(x,\ y)\!</math> |
| | x not equal to y | | | x not equal to y |
− | | <math>x \ne y</math> | + | | <math>x \ne y\!</math> |
| |- | | |- |
| | <math>f_{7}\!</math> | | | <math>f_{7}\!</math> |
| | <math>f_{0111}\!</math> | | | <math>f_{0111}\!</math> |
| | 0 1 1 1 | | | 0 1 1 1 |
− | | <math>(\!|x\ y|\!)</math> | + | | <math>(x\ y)\!</math> |
| | not both x and y | | | not both x and y |
− | | <math>\lnot x \lor \lnot y</math> | + | | <math>\lnot x \lor \lnot y\!</math> |
| |- | | |- |
| | <math>f_{8}\!</math> | | | <math>f_{8}\!</math> |
| | <math>f_{1000}\!</math> | | | <math>f_{1000}\!</math> |
| | 1 0 0 0 | | | 1 0 0 0 |
− | | <math>x\ y</math> | + | | <math>x\ y\!</math> |
| | x and y | | | x and y |
− | | <math>x \land y</math> | + | | <math>x \land y\!</math> |
| |- | | |- |
| | <math>f_{9}\!</math> | | | <math>f_{9}\!</math> |
| | <math>f_{1001}\!</math> | | | <math>f_{1001}\!</math> |
| | 1 0 0 1 | | | 1 0 0 1 |
− | | <math>(\!|(\!|x,\ y|\!)|\!)</math> | + | | <math>((x,\ y))\!</math> |
| | x equal to y | | | x equal to y |
| | <math>x = y\!</math> | | | <math>x = y\!</math> |
Line 2,416: |
Line 2,420: |
| | <math>f_{1011}\!</math> | | | <math>f_{1011}\!</math> |
| | 1 0 1 1 | | | 1 0 1 1 |
− | | <math>(\!|x\ (\!|y|\!)|\!)</math> | + | | <math>(x\ (y))\!</math> |
| | not x without y | | | not x without y |
− | | <math>x \Rightarrow y</math> | + | | <math>x \Rightarrow y\!</math> |
| |- | | |- |
| | <math>f_{12}\!</math> | | | <math>f_{12}\!</math> |
Line 2,430: |
Line 2,434: |
| | <math>f_{1101}\!</math> | | | <math>f_{1101}\!</math> |
| | 1 1 0 1 | | | 1 1 0 1 |
− | | <math>(\!|(\!|x|\!)\ y|\!)</math> | + | | <math>((x)\ y)\!</math> |
| | not y without x | | | not y without x |
− | | <math>x \Leftarrow y</math> | + | | <math>x \Leftarrow y\!</math> |
| |- | | |- |
| | <math>f_{14}\!</math> | | | <math>f_{14}\!</math> |
| | <math>f_{1110}\!</math> | | | <math>f_{1110}\!</math> |
| | 1 1 1 0 | | | 1 1 1 0 |
− | | <math>(\!|(\!|x|\!)(\!|y|\!)|\!)</math> | + | | <math>((x)(y))\!</math> |
| | x or y | | | x or y |
− | | <math>x \lor y</math> | + | | <math>x \lor y\!</math> |
| |- | | |- |
| | <math>f_{15}\!</math> | | | <math>f_{15}\!</math> |
| | <math>f_{1111}\!</math> | | | <math>f_{1111}\!</math> |
| | 1 1 1 1 | | | 1 1 1 1 |
− | | <math>(\!|(\!|~|\!)|\!)</math> | + | | <math>((~))\!</math> |
| | true | | | true |
| | <math>1\!</math> | | | <math>1\!</math> |
− | |}<br> | + | |} |
| + | <br> |
| | | |
| {| align="center" border="1" cellpadding="4" cellspacing="0" style="font-weight:bold; text-align:center; width:96%" | | {| align="center" border="1" cellpadding="4" cellspacing="0" style="font-weight:bold; text-align:center; width:96%" |
− | |+ '''Table 2. <math>\operatorname{E}f</math> Expanded Over Ordinary Features <math>\{ x, y \}\!</math>''' | + | |+ '''Table 1. Propositional Forms on Two Variables''' |
| |- style="background:ghostwhite" | | |- style="background:ghostwhite" |
− | | style="width:16%" | | + | | style="width:16%" | <math>\mathcal{L}_1</math> |
− | | style="width:16%" | <math>f\!</math> | + | | style="width:16%" | <math>\mathcal{L}_2</math> |
− | | style="width:16%" | <math>\operatorname{E}f|_{xy}</math> | + | | style="width:16%" | <math>\mathcal{L}_3</math> |
− | | style="width:16%" | <math>\operatorname{E}f|_{x(\!|y|\!)}</math> | + | | style="width:16%" | <math>\mathcal{L}_4</math> |
− | | style="width:16%" | <math>\operatorname{E}f|_{(\!|x|\!)y}</math> | + | | style="width:16%" | <math>\mathcal{L}_5</math> |
− | | style="width:16%" | <math>\operatorname{E}f|_{(\!|x|\!)(\!|y|\!)}</math> | + | | style="width:16%" | <math>\mathcal{L}_6</math> |
| + | |- style="background:ghostwhite" |
| + | | |
| + | | align="right" | <math>x\!</math> : |
| + | | 1 1 0 0 |
| + | | |
| + | | |
| + | | |
| + | |- style="background:ghostwhite" |
| + | | |
| + | | align="right" | <math>y\!</math> : |
| + | | 1 0 1 0 |
| + | | |
| + | | |
| + | | |
| |- | | |- |
| | <math>f_{0}\!</math> | | | <math>f_{0}\!</math> |
| + | | <math>f_{0000}\!</math> |
| + | | 0 0 0 0 |
| | <math>(\!|~|\!)</math> | | | <math>(\!|~|\!)</math> |
− | | <math>(\!|~|\!)</math> | + | | false |
− | | <math>(\!|~|\!)</math>
| + | | <math>0\!</math> |
− | | <math>(\!|~|\!)</math>
| |
− | | <math>(\!|~|\!)</math> | |
| |- | | |- |
| | <math>f_{1}\!</math> | | | <math>f_{1}\!</math> |
| + | | <math>f_{0001}\!</math> |
| + | | 0 0 0 1 |
| | <math>(\!|x|\!)(\!|y|\!)</math> | | | <math>(\!|x|\!)(\!|y|\!)</math> |
− | | <math>\operatorname{d}x\ \operatorname{d}y</math> | + | | neither x nor y |
− | | <math>\operatorname{d}x (\!|\operatorname{d}y|\!)</math>
| + | | <math>\lnot x \land \lnot y</math> |
− | | <math>(\!|\operatorname{d}x|\!) \operatorname{d}y</math>
| |
− | | <math>(\!|\operatorname{d}x|\!)(\!|\operatorname{d}y|\!)</math> | |
| |- | | |- |
| | <math>f_{2}\!</math> | | | <math>f_{2}\!</math> |
− | | <math>(\!|x|\!) y</math>
| + | | <math>f_{0010}\!</math> |
− | | <math>\operatorname{d}x (\!|\operatorname{d}y|\!)</math>
| + | | 0 0 1 0 |
− | | <math>\operatorname{d}x\ \operatorname{d}y</math>
| + | | <math>(\!|x|\!)\ y</math> |
− | | <math>(\!|\operatorname{d}x|\!)(\!|\operatorname{d}y|\!)</math>
| + | | y and not x |
− | | <math>(\!|\operatorname{d}x|\!) \operatorname{d}y</math>
| + | | <math>\lnot x \land y</math> |
− | |-
| |
− | | <math>f_{4}\!</math> | |
− | | <math>x (\!|y|\!)</math> | |
− | | <math>(\!|\operatorname{d}x|\!) \operatorname{d}y</math> | |
− | | <math>(\!|\operatorname{d}x|\!)(\!|\operatorname{d}y|\!)</math> | |
− | | <math>\operatorname{d}x\ \operatorname{d}y</math>
| |
− | | <math>\operatorname{d}x (\!|\operatorname{d}y|\!)</math>
| |
− | |-
| |
− | | <math>f_{8}\!</math>
| |
− | | <math>x y\!</math>
| |
− | | <math>(\!|\operatorname{d}x|\!)(\!|\operatorname{d}y|\!)</math>
| |
− | | <math>(\!|\operatorname{d}x|\!) \operatorname{d}y</math> | |
− | | <math>\operatorname{d}x (\!|\operatorname{d}y|\!)</math>
| |
− | | <math>\operatorname{d}x\ \operatorname{d}y</math>
| |
| |- | | |- |
| | <math>f_{3}\!</math> | | | <math>f_{3}\!</math> |
| + | | <math>f_{0011}\!</math> |
| + | | 0 0 1 1 |
| | <math>(\!|x|\!)</math> | | | <math>(\!|x|\!)</math> |
− | | <math>\operatorname{d}x</math> | + | | not x |
− | | <math>\operatorname{d}x</math> | + | | <math>\lnot x</math> |
− | | <math>(\!|\operatorname{d}x|\!)</math> | + | |- |
− | | <math>(\!|\operatorname{d}x|\!)</math> | + | | <math>f_{4}\!</math> |
| + | | <math>f_{0100}\!</math> |
| + | | 0 1 0 0 |
| + | | <math>x\ (\!|y|\!)</math> |
| + | | x and not y |
| + | | <math>x \land \lnot y</math> |
| |- | | |- |
− | | <math>f_{12}\!</math> | + | | <math>f_{5}\!</math> |
− | | <math>x\!</math> | + | | <math>f_{0101}\!</math> |
− | | <math>(\!|\operatorname{d}x|\!)</math> | + | | 0 1 0 1 |
− | | <math>(\!|\operatorname{d}x|\!)</math> | + | | <math>(\!|y|\!)</math> |
− | | <math>\operatorname{d}x</math> | + | | not y |
− | | <math>\operatorname{d}x</math> | + | | <math>\lnot y</math> |
| |- | | |- |
| | <math>f_{6}\!</math> | | | <math>f_{6}\!</math> |
− | | <math>(\!|x, y|\!)</math> | + | | <math>f_{0110}\!</math> |
− | | <math>(\!|\operatorname{d}x, \operatorname{d}y|\!)</math> | + | | 0 1 1 0 |
− | | <math>(\!|(\!|\operatorname{d}x, \operatorname{d}y|\!)|\!)</math> | + | | <math>(\!|x,\ y|\!)</math> |
− | | <math>(\!|(\!|\operatorname{d}x, \operatorname{d}y|\!)|\!)</math> | + | | x not equal to y |
− | | <math>(\!|\operatorname{d}x, \operatorname{d}y|\!)</math> | + | | <math>x \ne y</math> |
| + | |- |
| + | | <math>f_{7}\!</math> |
| + | | <math>f_{0111}\!</math> |
| + | | 0 1 1 1 |
| + | | <math>(\!|x\ y|\!)</math> |
| + | | not both x and y |
| + | | <math>\lnot x \lor \lnot y</math> |
| |- | | |- |
− | | <math>f_{9}\!</math> | + | | <math>f_{8}\!</math> |
− | | <math>(\!|(\!|x, y|\!)|\!)</math> | + | | <math>f_{1000}\!</math> |
− | | <math>(\!|(\!|\operatorname{d}x, \operatorname{d}y|\!)|\!)</math> | + | | 1 0 0 0 |
− | | <math>(\!|\operatorname{d}x, \operatorname{d}y|\!)</math> | + | | <math>x\ y</math> |
− | | <math>(\!|\operatorname{d}x, \operatorname{d}y|\!)</math> | + | | x and y |
− | | <math>(\!|(\!|\operatorname{d}x, \operatorname{d}y|\!)|\!)</math> | + | | <math>x \land y</math> |
| |- | | |- |
− | | <math>f_{5}\!</math> | + | | <math>f_{9}\!</math> |
− | | <math>(\!|y|\!)</math> | + | | <math>f_{1001}\!</math> |
− | | <math>\operatorname{d}y</math> | + | | 1 0 0 1 |
− | | <math>(\!|\operatorname{d}y|\!)</math> | + | | <math>(\!|(\!|x,\ y|\!)|\!)</math> |
− | | <math>\operatorname{d}y</math> | + | | x equal to y |
− | | <math>(\!|\operatorname{d}y|\!)</math> | + | | <math>x = y\!</math> |
| |- | | |- |
| | <math>f_{10}\!</math> | | | <math>f_{10}\!</math> |
| + | | <math>f_{1010}\!</math> |
| + | | 1 0 1 0 |
| + | | <math>y\!</math> |
| + | | y |
| | <math>y\!</math> | | | <math>y\!</math> |
− | | <math>(\!|\operatorname{d}y|\!)</math>
| |
− | | <math>\operatorname{d}y</math>
| |
− | | <math>(\!|\operatorname{d}y|\!)</math>
| |
− | | <math>\operatorname{d}y</math>
| |
− | |-
| |
− | | <math>f_{7}\!</math>
| |
− | | <math>(\!|x y|\!)</math>
| |
− | | <math>(\!|(\!|\operatorname{d}x|\!)(\!|\operatorname{d}y|\!)|\!)</math>
| |
− | | <math>(\!|(\!|\operatorname{d}x|\!) \operatorname{d}y|\!)</math>
| |
− | | <math>(\!|\operatorname{d}x (\!|\operatorname{d}y|\!)|\!)</math>
| |
− | | <math>(\!|\operatorname{d}x\ \operatorname{d}y|\!)</math>
| |
| |- | | |- |
| | <math>f_{11}\!</math> | | | <math>f_{11}\!</math> |
− | | <math>(\!|x (\!|y|\!)|\!)</math> | + | | <math>f_{1011}\!</math> |
− | | <math>(\!|(\!|\operatorname{d}x|\!) \operatorname{d}y|\!)</math> | + | | 1 0 1 1 |
− | | <math>(\!|(\!|\operatorname{d}x|\!)(\!|\operatorname{d}y|\!)|\!)</math> | + | | <math>(\!|x\ (\!|y|\!)|\!)</math> |
− | | <math>(\!|\operatorname{d}x\ \operatorname{d}y|\!)</math> | + | | not x without y |
− | | <math>(\!|\operatorname{d}x (\!|\operatorname{d}y|\!)|\!)</math> | + | | <math>x \Rightarrow y</math> |
| + | |- |
| + | | <math>f_{12}\!</math> |
| + | | <math>f_{1100}\!</math> |
| + | | 1 1 0 0 |
| + | | <math>x\!</math> |
| + | | x |
| + | | <math>x\!</math> |
| |- | | |- |
| | <math>f_{13}\!</math> | | | <math>f_{13}\!</math> |
− | | <math>(\!|(\!|x|\!) y|\!)</math> | + | | <math>f_{1101}\!</math> |
− | | <math>(\!|\operatorname{d}x (\!|\operatorname{d}y|\!)|\!)</math>
| + | | 1 1 0 1 |
− | | <math>(\!|\operatorname{d}x\ \operatorname{d}y|\!)</math> | + | | <math>(\!|(\!|x|\!)\ y|\!)</math> |
− | | <math>(\!|(\!|\operatorname{d}x|\!)(\!|\operatorname{d}y|\!)|\!)</math> | + | | not y without x |
− | | <math>(\!|(\!|\operatorname{d}x|\!) \operatorname{d}y|\!)</math> | + | | <math>x \Leftarrow y</math> |
| |- | | |- |
| | <math>f_{14}\!</math> | | | <math>f_{14}\!</math> |
| + | | <math>f_{1110}\!</math> |
| + | | 1 1 1 0 |
| | <math>(\!|(\!|x|\!)(\!|y|\!)|\!)</math> | | | <math>(\!|(\!|x|\!)(\!|y|\!)|\!)</math> |
− | | <math>(\!|\operatorname{d}x\ \operatorname{d}y|\!)</math> | + | | x or y |
− | | <math>(\!|\operatorname{d}x (\!|\operatorname{d}y|\!)|\!)</math>
| + | | <math>x \lor y</math> |
− | | <math>(\!|(\!|\operatorname{d}x|\!) \operatorname{d}y|\!)</math>
| |
− | | <math>(\!|(\!|\operatorname{d}x|\!)(\!|\operatorname{d}y|\!)|\!)</math> | |
| |- | | |- |
| | <math>f_{15}\!</math> | | | <math>f_{15}\!</math> |
| + | | <math>f_{1111}\!</math> |
| + | | 1 1 1 1 |
| | <math>(\!|(\!|~|\!)|\!)</math> | | | <math>(\!|(\!|~|\!)|\!)</math> |
− | | <math>(\!|(\!|~|\!)|\!)</math> | + | | true |
− | | <math>(\!|(\!|~|\!)|\!)</math> | + | | <math>1\!</math> |
− | | <math>(\!|(\!|~|\!)|\!)</math> | + | |} |
− | | <math>(\!|(\!|~|\!)|\!)</math>
| + | <br> |
− | |}<br>
| |
| | | |
− | =Work Area 3=
| + | {| align="center" border="1" cellpadding="4" cellspacing="0" style="font-weight:bold; text-align:center; width:96%" |
− | | + | |+ '''Table 2. <math>\operatorname{E}f</math> Expanded Over Ordinary Features <math>\{ x, y \}\!</math>''' |
− | ==Propositional Forms on Two Variables==
| |
− | | |
− | To broaden our experience with simple examples, let us now contemplate the sixteen functions of concrete type <math>X \times Y \to \mathbb{B}</math> and abstract type <math>\mathbb{B} \times \mathbb{B} \to \mathbb{B}.</math> For future reference, I will set here a few Tables that detail the actions of <math>\operatorname{E}</math> and <math>\operatorname{D}</math> on each of these functions, allowing us to view the results in several different ways.
| |
− | | |
− | By way of initial orientation, Table 1 lists equivalent expressions for the sixteen functions in a number of different languages for zeroth order logic.
| |
− | | |
− | ===Variant 1===
| |
− | | |
− | {| align="center" border="1" cellpadding="4" cellspacing="0" style="font-weight:bold; text-align:center; width:96%" | |
− | |+ '''Table 1. Propositional Forms on Two Variables''' | |
| |- style="background:ghostwhite" | | |- style="background:ghostwhite" |
− | | style="width:16%" | <math>\mathcal{L}_1</math> | + | | style="width:16%" | |
− | | style="width:16%" | <math>\mathcal{L}_2</math> | + | | style="width:16%" | <math>f\!</math> |
− | | style="width:16%" | <math>\mathcal{L}_3</math> | + | | style="width:16%" | <math>\operatorname{E}f|_{xy}</math> |
− | | style="width:16%" | <math>\mathcal{L}_4</math> | + | | style="width:16%" | <math>\operatorname{E}f|_{x(\!|y|\!)}</math> |
− | | style="width:16%" | <math>\mathcal{L}_5</math> | + | | style="width:16%" | <math>\operatorname{E}f|_{(\!|x|\!)y}</math> |
− | | style="width:16%" | <math>\mathcal{L}_6</math> | + | | style="width:16%" | <math>\operatorname{E}f|_{(\!|x|\!)(\!|y|\!)}</math> |
− | |- style="background:ghostwhite" | |
− | | | |
− | | align="right" | <math>x\!</math> : | |
− | | 1 1 0 0 | |
− | |
| |
− | |
| |
− | |
| |
− | |- style="background:ghostwhite"
| |
− | | | |
− | | align="right" | <math>y\!</math> :
| |
− | | 1 0 1 0
| |
− | |
| |
− | |
| |
− | |
| |
| |- | | |- |
| | <math>f_{0}\!</math> | | | <math>f_{0}\!</math> |
− | | <math>f_{0000}\!</math> | + | | <math>(\!|~|\!)</math> |
− | | 0 0 0 0 | + | | <math>(\!|~|\!)</math> |
− | | <math>(~)\!</math> | + | | <math>(\!|~|\!)</math> |
− | | false | + | | <math>(\!|~|\!)</math> |
− | | <math>0\!</math> | + | | <math>(\!|~|\!)</math> |
| |- | | |- |
| | <math>f_{1}\!</math> | | | <math>f_{1}\!</math> |
− | | <math>f_{0001}\!</math> | + | | <math>(\!|x|\!)(\!|y|\!)</math> |
− | | 0 0 0 1 | + | | <math>\operatorname{d}x\ \operatorname{d}y</math> |
− | | <math>(x)(y)\!</math> | + | | <math>\operatorname{d}x (\!|\operatorname{d}y|\!)</math> |
− | | neither x nor y | + | | <math>(\!|\operatorname{d}x|\!) \operatorname{d}y</math> |
− | | <math>\lnot x \land \lnot y\!</math> | + | | <math>(\!|\operatorname{d}x|\!)(\!|\operatorname{d}y|\!)</math> |
| |- | | |- |
| | <math>f_{2}\!</math> | | | <math>f_{2}\!</math> |
− | | <math>f_{0010}\!</math> | + | | <math>(\!|x|\!) y</math> |
− | | 0 0 1 0
| + | | <math>\operatorname{d}x (\!|\operatorname{d}y|\!)</math> |
− | | <math>(x)\ y\!</math> | + | | <math>\operatorname{d}x\ \operatorname{d}y</math> |
− | | y and not x
| + | | <math>(\!|\operatorname{d}x|\!)(\!|\operatorname{d}y|\!)</math> |
− | | <math>\lnot x \land y\!</math> | + | | <math>(\!|\operatorname{d}x|\!) \operatorname{d}y</math> |
− | |-
| |
− | | <math>f_{3}\!</math> | |
− | | <math>f_{0011}\!</math> | |
− | | 0 0 1 1
| |
− | | <math>(x)\!</math> | |
− | | not x | |
− | | <math>\lnot x\!</math> | |
| |- | | |- |
| | <math>f_{4}\!</math> | | | <math>f_{4}\!</math> |
− | | <math>f_{0100}\!</math> | + | | <math>x (\!|y|\!)</math> |
− | | 0 1 0 0
| + | | <math>(\!|\operatorname{d}x|\!) \operatorname{d}y</math> |
− | | <math>x\ (y)\!</math> | + | | <math>(\!|\operatorname{d}x|\!)(\!|\operatorname{d}y|\!)</math> |
− | | x and not y | + | | <math>\operatorname{d}x\ \operatorname{d}y</math> |
− | | <math>x \land \lnot y\!</math> | + | | <math>\operatorname{d}x (\!|\operatorname{d}y|\!)</math> |
| |- | | |- |
− | | <math>f_{5}\!</math> | + | | <math>f_{8}\!</math> |
− | | <math>f_{0101}\!</math> | + | | <math>x y\!</math> |
− | | 0 1 0 1
| + | | <math>(\!|\operatorname{d}x|\!)(\!|\operatorname{d}y|\!)</math> |
− | | <math>(y)\!</math> | + | | <math>(\!|\operatorname{d}x|\!) \operatorname{d}y</math> |
− | | not y | + | | <math>\operatorname{d}x (\!|\operatorname{d}y|\!)</math> |
− | | <math>\lnot y\!</math> | + | | <math>\operatorname{d}x\ \operatorname{d}y</math> |
| |- | | |- |
− | | <math>f_{6}\!</math> | + | | <math>f_{3}\!</math> |
− | | <math>f_{0110}\!</math> | + | | <math>(\!|x|\!)</math> |
− | | 0 1 1 0 | + | | <math>\operatorname{d}x</math> |
− | | <math>(x,\ y)\!</math> | + | | <math>\operatorname{d}x</math> |
− | | x not equal to y
| + | | <math>(\!|\operatorname{d}x|\!)</math> |
− | | <math>x \ne y\!</math> | + | | <math>(\!|\operatorname{d}x|\!)</math> |
| |- | | |- |
− | | <math>f_{7}\!</math> | + | | <math>f_{12}\!</math> |
− | | <math>f_{0111}\!</math> | + | | <math>x\!</math> |
− | | 0 1 1 1
| + | | <math>(\!|\operatorname{d}x|\!)</math> |
− | | <math>(x\ y)\!</math> | + | | <math>(\!|\operatorname{d}x|\!)</math> |
− | | not both x and y | + | | <math>\operatorname{d}x</math> |
− | | <math>\lnot x \lor \lnot y\!</math> | + | | <math>\operatorname{d}x</math> |
| |- | | |- |
− | | <math>f_{8}\!</math> | + | | <math>f_{6}\!</math> |
− | | <math>f_{1000}\!</math> | + | | <math>(\!|x, y|\!)</math> |
− | | 1 0 0 0
| + | | <math>(\!|\operatorname{d}x, \operatorname{d}y|\!)</math> |
− | | <math>x\ y\!</math> | + | | <math>(\!|(\!|\operatorname{d}x, \operatorname{d}y|\!)|\!)</math> |
− | | x and y | + | | <math>(\!|(\!|\operatorname{d}x, \operatorname{d}y|\!)|\!)</math> |
− | | <math>x \land y\!</math> | + | | <math>(\!|\operatorname{d}x, \operatorname{d}y|\!)</math> |
| |- | | |- |
| | <math>f_{9}\!</math> | | | <math>f_{9}\!</math> |
− | | <math>f_{1001}\!</math> | + | | <math>(\!|(\!|x, y|\!)|\!)</math> |
− | | 1 0 0 1
| + | | <math>(\!|(\!|\operatorname{d}x, \operatorname{d}y|\!)|\!)</math> |
− | | <math>((x,\ y))\!</math> | + | | <math>(\!|\operatorname{d}x, \operatorname{d}y|\!)</math> |
− | | x equal to y | + | | <math>(\!|\operatorname{d}x, \operatorname{d}y|\!)</math> |
− | | <math>x = y\!</math> | + | | <math>(\!|(\!|\operatorname{d}x, \operatorname{d}y|\!)|\!)</math> |
| |- | | |- |
− | | <math>f_{10}\!</math> | + | | <math>f_{5}\!</math> |
− | | <math>f_{1010}\!</math> | + | | <math>(\!|y|\!)</math> |
− | | 1 0 1 0 | + | | <math>\operatorname{d}y</math> |
− | | <math>y\!</math> | + | | <math>(\!|\operatorname{d}y|\!)</math> |
− | | y | + | | <math>\operatorname{d}y</math> |
| + | | <math>(\!|\operatorname{d}y|\!)</math> |
| + | |- |
| + | | <math>f_{10}\!</math> |
| | <math>y\!</math> | | | <math>y\!</math> |
| + | | <math>(\!|\operatorname{d}y|\!)</math> |
| + | | <math>\operatorname{d}y</math> |
| + | | <math>(\!|\operatorname{d}y|\!)</math> |
| + | | <math>\operatorname{d}y</math> |
| + | |- |
| + | | <math>f_{7}\!</math> |
| + | | <math>(\!|x y|\!)</math> |
| + | | <math>(\!|(\!|\operatorname{d}x|\!)(\!|\operatorname{d}y|\!)|\!)</math> |
| + | | <math>(\!|(\!|\operatorname{d}x|\!) \operatorname{d}y|\!)</math> |
| + | | <math>(\!|\operatorname{d}x (\!|\operatorname{d}y|\!)|\!)</math> |
| + | | <math>(\!|\operatorname{d}x\ \operatorname{d}y|\!)</math> |
| |- | | |- |
| | <math>f_{11}\!</math> | | | <math>f_{11}\!</math> |
− | | <math>f_{1011}\!</math> | + | | <math>(\!|x (\!|y|\!)|\!)</math> |
− | | 1 0 1 1
| + | | <math>(\!|(\!|\operatorname{d}x|\!) \operatorname{d}y|\!)</math> |
− | | <math>(x\ (y))\!</math> | + | | <math>(\!|(\!|\operatorname{d}x|\!)(\!|\operatorname{d}y|\!)|\!)</math> |
− | | not x without y | + | | <math>(\!|\operatorname{d}x\ \operatorname{d}y|\!)</math> |
− | | <math>x \Rightarrow y\!</math> | + | | <math>(\!|\operatorname{d}x (\!|\operatorname{d}y|\!)|\!)</math> |
− | |-
| |
− | | <math>f_{12}\!</math> | |
− | | <math>f_{1100}\!</math> | |
− | | 1 1 0 0
| |
− | | <math>x\!</math> | |
− | | x | |
− | | <math>x\!</math> | |
| |- | | |- |
| | <math>f_{13}\!</math> | | | <math>f_{13}\!</math> |
− | | <math>f_{1101}\!</math> | + | | <math>(\!|(\!|x|\!) y|\!)</math> |
− | | 1 1 0 1 | + | | <math>(\!|\operatorname{d}x (\!|\operatorname{d}y|\!)|\!)</math> |
− | | <math>((x)\ y)\!</math> | + | | <math>(\!|\operatorname{d}x\ \operatorname{d}y|\!)</math> |
− | | not y without x
| + | | <math>(\!|(\!|\operatorname{d}x|\!)(\!|\operatorname{d}y|\!)|\!)</math> |
− | | <math>x \Leftarrow y\!</math> | + | | <math>(\!|(\!|\operatorname{d}x|\!) \operatorname{d}y|\!)</math> |
| |- | | |- |
| | <math>f_{14}\!</math> | | | <math>f_{14}\!</math> |
− | | <math>f_{1110}\!</math> | + | | <math>(\!|(\!|x|\!)(\!|y|\!)|\!)</math> |
− | | 1 1 1 0
| + | | <math>(\!|\operatorname{d}x\ \operatorname{d}y|\!)</math> |
− | | <math>((x)(y))\!</math> | + | | <math>(\!|\operatorname{d}x (\!|\operatorname{d}y|\!)|\!)</math> |
− | | x or y | + | | <math>(\!|(\!|\operatorname{d}x|\!) \operatorname{d}y|\!)</math> |
− | | <math>x \lor y\!</math> | + | | <math>(\!|(\!|\operatorname{d}x|\!)(\!|\operatorname{d}y|\!)|\!)</math> |
| |- | | |- |
| | <math>f_{15}\!</math> | | | <math>f_{15}\!</math> |
− | | <math>f_{1111}\!</math> | + | | <math>(\!|(\!|~|\!)|\!)</math> |
− | | 1 1 1 1 | + | | <math>(\!|(\!|~|\!)|\!)</math> |
− | | <math>((~))\!</math> | + | | <math>(\!|(\!|~|\!)|\!)</math> |
− | | true | + | | <math>(\!|(\!|~|\!)|\!)</math> |
− | | <math>1\!</math> | + | | <math>(\!|(\!|~|\!)|\!)</math> |
| |} | | |} |
| <br> | | <br> |
| | | |
− | ===Variant 2=== | + | =Work Area 1= |
| + | |
| + | ==Propositional Forms on Two Variables== |
| + | |
| + | To broaden our experience with simple examples, let us now contemplate the sixteen functions of concrete type <math>X \times Y \to \mathbb{B}</math> and abstract type <math>\mathbb{B} \times \mathbb{B} \to \mathbb{B}.</math> For future reference, I will set here a few Tables that detail the actions of <math>\operatorname{E}</math> and <math>\operatorname{D}</math> on each of these functions, allowing us to view the results in several different ways. |
| + | |
| + | By way of initial orientation, Table 1 lists equivalent expressions for the sixteen functions in a number of different languages for zeroth order logic. |
| + | |
| + | ===Variant 1=== |
| | | |
| {| align="center" border="1" cellpadding="4" cellspacing="0" style="font-weight:bold; text-align:center; width:96%" | | {| align="center" border="1" cellpadding="4" cellspacing="0" style="font-weight:bold; text-align:center; width:96%" |
Line 2,860: |
Line 2,864: |
| <br> | | <br> |
| | | |
− | ===Variant 3=== | + | ===Variant 2=== |
| | | |
| {| align="center" border="1" cellpadding="4" cellspacing="0" style="font-weight:bold; text-align:center; width:96%" | | {| align="center" border="1" cellpadding="4" cellspacing="0" style="font-weight:bold; text-align:center; width:96%" |
Line 3,104: |
Line 3,108: |
| <br> | | <br> |
| | | |
− | ===Variant 4=== | + | ===Variant 3=== |
| | | |
| {| align="center" border="1" cellpadding="4" cellspacing="0" style="font-weight:bold; text-align:center; width:96%" | | {| align="center" border="1" cellpadding="4" cellspacing="0" style="font-weight:bold; text-align:center; width:96%" |
Line 3,348: |
Line 3,352: |
| <br> | | <br> |
| | | |
− | ===Variant 5=== | + | ===Variant 4=== |
| | | |
| {| align="center" border="1" cellpadding="4" cellspacing="0" style="font-weight:bold; text-align:center; width:96%" | | {| align="center" border="1" cellpadding="4" cellspacing="0" style="font-weight:bold; text-align:center; width:96%" |
Line 3,691: |
Line 3,695: |
| | <math>((~))\!</math> | | | <math>((~))\!</math> |
| | <math>((~))\!</math> | | | <math>((~))\!</math> |
− | |}<br> | + | |} |
| + | <br> |
| | | |
| <pre> | | <pre> |