Line 1,429: |
Line 1,429: |
| {| align="center" cellpadding="0" cellspacing="0" width="100%" | | {| align="center" cellpadding="0" cellspacing="0" width="100%" |
| |- style="height:48px; text-align:right" | | |- style="height:48px; text-align:right" |
− | | width="98%" | <math>\text{Logical Translation Rule 2}\!</math> | + | | width="98%" | <math>\text{Geometric Translation Rule 2}\!</math> |
− | | width="2%" | | + | | width="2%" | |
| |} | | |} |
| |- | | |- |
Line 1,451: |
Line 1,451: |
| | | | | |
| | <math>\text{L2a.}\!</math> | | | <math>\text{L2a.}\!</math> |
− | | <math>\downharpoonleft s \downharpoonright ~=~ p \quad \operatorname{and} \quad \downharpoonleft t \downharpoonright ~=~ q</math> | + | | <math>\upharpoonleft s \upharpoonright ~=~ p \quad \operatorname{and} \quad \upharpoonleft t \upharpoonright ~=~ q</math> |
| |- style="height:48px" | | |- style="height:48px" |
| | | | | |
Line 1,464: |
Line 1,464: |
| | width="14%" style="border-top:1px solid black" align="left" | <math>\text{L2b}_{0}.\!</math> | | | width="14%" style="border-top:1px solid black" align="left" | <math>\text{L2b}_{0}.\!</math> |
| | width="32%" style="border-top:1px solid black" | | | | width="32%" style="border-top:1px solid black" | |
− | <math>\downharpoonleft \operatorname{false} \downharpoonright</math> | + | <math>\upharpoonleft \operatorname{false} \upharpoonright</math> |
| | width="4%" style="border-top:1px solid black" | <math>=\!</math> | | | width="4%" style="border-top:1px solid black" | <math>=\!</math> |
| | width="28%" style="border-top:1px solid black" | <math>(~)</math> | | | width="28%" style="border-top:1px solid black" | <math>(~)</math> |
Line 1,472: |
Line 1,472: |
| | | | | |
| | align="left" | <math>\text{L2b}_{1}.\!</math> | | | align="left" | <math>\text{L2b}_{1}.\!</math> |
− | | <math>\downharpoonleft \operatorname{neither}~ s ~\operatorname{nor}~ t \downharpoonright</math> | + | | <math>\upharpoonleft \operatorname{neither}~ s ~\operatorname{nor}~ t \upharpoonright</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
− | | <math>(\downharpoonleft s \downharpoonright)(\downharpoonleft t \downharpoonright)</math> | + | | <math>(\upharpoonleft s \upharpoonright)(\upharpoonleft t \upharpoonright)</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
| | <math>(p)(q)\!</math> | | | <math>(p)(q)\!</math> |
Line 1,480: |
Line 1,480: |
| | | | | |
| | align="left" | <math>\text{L2b}_{2}.\!</math> | | | align="left" | <math>\text{L2b}_{2}.\!</math> |
− | | <math>\downharpoonleft \operatorname{not}~ s ~\operatorname{but}~ t \downharpoonright</math> | + | | <math>\upharpoonleft \operatorname{not}~ s ~\operatorname{but}~ t \upharpoonright</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
− | | <math>(\downharpoonleft s \downharpoonright) \downharpoonleft t \downharpoonright</math> | + | | <math>(\upharpoonleft s \upharpoonright) \upharpoonleft t \upharpoonright</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
| | <math>(p) q\!</math> | | | <math>(p) q\!</math> |
Line 1,488: |
Line 1,488: |
| | | | | |
| | align="left" | <math>\text{L2b}_{3}.\!</math> | | | align="left" | <math>\text{L2b}_{3}.\!</math> |
− | | <math>\downharpoonleft \operatorname{not}~ s \downharpoonright</math> | + | | <math>\upharpoonleft \operatorname{not}~ s \upharpoonright</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
− | | <math>(\downharpoonleft s \downharpoonright)</math> | + | | <math>(\upharpoonleft s \upharpoonright)</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
| | <math>(p)\!</math> | | | <math>(p)\!</math> |
Line 1,496: |
Line 1,496: |
| | | | | |
| | align="left" | <math>\text{L2b}_{4}.\!</math> | | | align="left" | <math>\text{L2b}_{4}.\!</math> |
− | | <math>\downharpoonleft s ~\operatorname{and~not}~ t \downharpoonright</math> | + | | <math>\upharpoonleft s ~\operatorname{and~not}~ t \upharpoonright</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
− | | <math>\downharpoonleft s \downharpoonright (\downharpoonleft t \downharpoonright)</math> | + | | <math>\upharpoonleft s \upharpoonright (\upharpoonleft t \upharpoonright)</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
| | <math>p (q)\!</math> | | | <math>p (q)\!</math> |
Line 1,504: |
Line 1,504: |
| | | | | |
| | align="left" | <math>\text{L2b}_{5}.\!</math> | | | align="left" | <math>\text{L2b}_{5}.\!</math> |
− | | <math>\downharpoonleft \operatorname{not}~ t \downharpoonright</math> | + | | <math>\upharpoonleft \operatorname{not}~ t \upharpoonright</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
− | | <math>(\downharpoonleft t \downharpoonright)</math> | + | | <math>(\upharpoonleft t \upharpoonright)</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
| | <math>(q)\!</math> | | | <math>(q)\!</math> |
Line 1,512: |
Line 1,512: |
| | | | | |
| | align="left" | <math>\text{L2b}_{6}.\!</math> | | | align="left" | <math>\text{L2b}_{6}.\!</math> |
− | | <math>\downharpoonleft s ~\operatorname{or}~ t, ~\operatorname{not~both} \downharpoonright</math> | + | | <math>\upharpoonleft s ~\operatorname{or}~ t, ~\operatorname{not~both} \upharpoonright</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
− | | <math>(\downharpoonleft s \downharpoonright ~,~ \downharpoonleft t \downharpoonright)</math> | + | | <math>(\upharpoonleft s \upharpoonright ~,~ \upharpoonleft t \upharpoonright)</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
| | <math>(p, q)\!</math> | | | <math>(p, q)\!</math> |
Line 1,520: |
Line 1,520: |
| | | | | |
| | align="left" | <math>\text{L2b}_{7}.\!</math> | | | align="left" | <math>\text{L2b}_{7}.\!</math> |
− | | <math>\downharpoonleft \operatorname{not~both}~ s ~\operatorname{and}~ t \downharpoonright</math> | + | | <math>\upharpoonleft \operatorname{not~both}~ s ~\operatorname{and}~ t \upharpoonright</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
− | | <math>(\downharpoonleft s \downharpoonright ~ \downharpoonleft t \downharpoonright)</math> | + | | <math>(\upharpoonleft s \upharpoonright ~ \upharpoonleft t \upharpoonright)</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
| | <math>(p q)\!</math> | | | <math>(p q)\!</math> |
Line 1,528: |
Line 1,528: |
| | | | | |
| | align="left" | <math>\text{L2b}_{8}.\!</math> | | | align="left" | <math>\text{L2b}_{8}.\!</math> |
− | | <math>\downharpoonleft s ~\operatorname{and}~ t \downharpoonright</math> | + | | <math>\upharpoonleft s ~\operatorname{and}~ t \upharpoonright</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
− | | <math>\downharpoonleft s \downharpoonright ~ \downharpoonleft t \downharpoonright</math> | + | | <math>\upharpoonleft s \upharpoonright ~ \upharpoonleft t \upharpoonright</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
| | <math>p q\!</math> | | | <math>p q\!</math> |
Line 1,536: |
Line 1,536: |
| | | | | |
| | align="left" | <math>\text{L2b}_{9}.\!</math> | | | align="left" | <math>\text{L2b}_{9}.\!</math> |
− | | <math>\downharpoonleft s ~\operatorname{is~equivalent~to}~ t \downharpoonright</math> | + | | <math>\upharpoonleft s ~\operatorname{is~equivalent~to}~ t \upharpoonright</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
− | | <math>((\downharpoonleft s \downharpoonright ~,~ \downharpoonleft t \downharpoonright))</math> | + | | <math>((\upharpoonleft s \upharpoonright ~,~ \upharpoonleft t \upharpoonright))</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
| | <math>((p, q))\!</math> | | | <math>((p, q))\!</math> |
Line 1,544: |
Line 1,544: |
| | | | | |
| | align="left" | <math>\text{L2b}_{10}.\!</math> | | | align="left" | <math>\text{L2b}_{10}.\!</math> |
− | | <math>\downharpoonleft t \downharpoonright</math> | + | | <math>\upharpoonleft t \upharpoonright</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
− | | <math>\downharpoonleft t \downharpoonright</math> | + | | <math>\upharpoonleft t \upharpoonright</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
| | <math>q\!</math> | | | <math>q\!</math> |
Line 1,552: |
Line 1,552: |
| | | | | |
| | align="left" | <math>\text{L2b}_{11}.\!</math> | | | align="left" | <math>\text{L2b}_{11}.\!</math> |
− | | <math>\downharpoonleft s ~\operatorname{implies}~ t \downharpoonright</math> | + | | <math>\upharpoonleft s ~\operatorname{implies}~ t \upharpoonright</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
− | | <math>(\downharpoonleft s \downharpoonright (\downharpoonleft t \downharpoonright))</math> | + | | <math>(\upharpoonleft s \upharpoonright (\upharpoonleft t \upharpoonright))</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
| | <math>(p (q))\!</math> | | | <math>(p (q))\!</math> |
Line 1,560: |
Line 1,560: |
| | | | | |
| | align="left" | <math>\text{L2b}_{12}.\!</math> | | | align="left" | <math>\text{L2b}_{12}.\!</math> |
− | | <math>\downharpoonleft s \downharpoonright</math> | + | | <math>\upharpoonleft s \upharpoonright</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
− | | <math>\downharpoonleft s \downharpoonright</math> | + | | <math>\upharpoonleft s \upharpoonright</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
| | <math>p\!</math> | | | <math>p\!</math> |
Line 1,568: |
Line 1,568: |
| | | | | |
| | align="left" | <math>\text{L2b}_{13}.\!</math> | | | align="left" | <math>\text{L2b}_{13}.\!</math> |
− | | <math>\downharpoonleft s ~\operatorname{is~implied~by}~ t \downharpoonright</math> | + | | <math>\upharpoonleft s ~\operatorname{is~implied~by}~ t \upharpoonright</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
− | | <math>((\downharpoonleft s \downharpoonright) \downharpoonleft t \downharpoonright)</math> | + | | <math>((\upharpoonleft s \upharpoonright) \upharpoonleft t \upharpoonright)</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
| | <math>((p) q)\!</math> | | | <math>((p) q)\!</math> |
Line 1,576: |
Line 1,576: |
| | | | | |
| | align="left" | <math>\text{L2b}_{14}.\!</math> | | | align="left" | <math>\text{L2b}_{14}.\!</math> |
− | | <math>\downharpoonleft s ~\operatorname{or}~ t \downharpoonright</math> | + | | <math>\upharpoonleft s ~\operatorname{or}~ t \upharpoonright</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
− | | <math>((\downharpoonleft s \downharpoonright)(\downharpoonleft t \downharpoonright))</math> | + | | <math>((\upharpoonleft s \upharpoonright)(\upharpoonleft t \upharpoonright))</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
| | <math>((p)(q))\!</math> | | | <math>((p)(q))\!</math> |
Line 1,584: |
Line 1,584: |
| | | | | |
| | align="left" | <math>\text{L2b}_{15}.\!</math> | | | align="left" | <math>\text{L2b}_{15}.\!</math> |
− | | <math>\downharpoonleft \operatorname{true} \downharpoonright</math> | + | | <math>\upharpoonleft \operatorname{true} \upharpoonright</math> |
| | <math>=\!</math> | | | <math>=\!</math> |
| | <math>((~))</math> | | | <math>((~))</math> |