Changes

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%"   | &nbsp;
+
| width="2%" | &nbsp;
 
|}
 
|}
 
|-
 
|-
Line 1,451: Line 1,451:  
| &nbsp;
 
| &nbsp;
 
| <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"
 
| &nbsp;
 
| &nbsp;
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:  
| &nbsp;
 
| &nbsp;
 
| 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:  
| &nbsp;
 
| &nbsp;
 
| 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:  
| &nbsp;
 
| &nbsp;
 
| 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:  
| &nbsp;
 
| &nbsp;
 
| 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:  
| &nbsp;
 
| &nbsp;
 
| 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:  
| &nbsp;
 
| &nbsp;
 
| 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:  
| &nbsp;
 
| &nbsp;
 
| 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:  
| &nbsp;
 
| &nbsp;
 
| 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:  
| &nbsp;
 
| &nbsp;
 
| 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:  
| &nbsp;
 
| &nbsp;
 
| 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:  
| &nbsp;
 
| &nbsp;
 
| 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:  
| &nbsp;
 
| &nbsp;
 
| 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:  
| &nbsp;
 
| &nbsp;
 
| 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:  
| &nbsp;
 
| &nbsp;
 
| 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:  
| &nbsp;
 
| &nbsp;
 
| 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>
12,089

edits