Axiomatic definitions of sublanguages of Loglan'82 - Historia wersji

AndrzejSalwicki: /* Characters */

2014-11-27T14:21:18Z

‎Characters

2014-11-27T12:01:12Z

‎Characters

2014-11-27T12:00:02Z

‎Characters

2014-11-27T11:59:06Z

‎Characters

2014-11-27T11:57:40Z

‎Characters

2014-11-27T11:33:07Z

‎Characters

2014-11-27T11:31:28Z

‎Characters

2014-11-27T11:29:29Z

‎Characters

2014-11-27T11:28:54Z

‎Characters

2014-11-27T11:27:05Z

‎Characters

@@ Linia 83: / Linia 83: @@
 I.e. ''the execution of three instructions causes swap of the values of variables'' <math> c_1, c_2 </math>.<br />
 '''Proof''' uses two axioms of algorithmic logic: <br />
-<math>\begin{equation}\tag{Ax:=}\fbox{[x:=\tau]\alpha \Leftrightarrow \alpha(x/\tau)} \end{equation} </math> <br />
+<math>\begin{equation}\tag{Ax:=}[x:=\tau]\alpha \Leftrightarrow \alpha(x/\tau) \end{equation} </math> <br />
 this axiom of assignment instruction reads: ''formula '' <math>\alpha(x/\tau)</math> '' holds iff after execution of instruction  '' <math>x:=\tau</math> ''formula  ''<math>\alpha</math> '' holds.''<br />
-<math>\begin{equation}\tag{Ax ;}\fbox{[K; M]\alpha \Leftrightarrow [K][M]\alpha } \end{equation} </math><br />
+<math>\begin{equation}\tag{Ax ;}[K; M]\alpha \Leftrightarrow [K][M]\alpha  \end{equation} </math><br />
 and the inference rule
 <math>\begin{equation}\tag{R2}\dfrac{\alpha \Rightarrow \beta}{M\alpha \Rightarrow M\beta}   \end{equation} </math>

@@ Linia 87: / Linia 87: @@
 <math>\begin{equation}\tag{Ax ;}\fbox{[K; M]\alpha \Leftrightarrow [K][M]\alpha } \end{equation} </math><br />
 and the inference rule
-<math>\begin{equation}\tag{R2}\fbox{\dfrac{\alpha \Rightarrow \beta}{M\alpha \Rightarrow M\beta} }  \end{equation} </math>
+<math>\begin{equation}\tag{R2}\dfrac{\alpha \Rightarrow \beta}{M\alpha \Rightarrow M\beta}   \end{equation} </math>
 Now observe that the following formulas are equivalent<br />
 <math>\begin{align*}{}

@@ Linia 87: / Linia 87: @@
 <math>\begin{equation}\tag{Ax ;}\fbox{[K; M]\alpha \Leftrightarrow [K][M]\alpha } \end{equation} </math><br />
 and the inference rule
-<math>\begin{equation}\fbox{\tag{R2}\dfrac{\alpha \Rightarrow \beta}{M\alpha \Rightarrow M\beta} }  \end{equation} </math>
+<math>\begin{equation}\tag{R2}\fbox{\dfrac{\alpha \Rightarrow \beta}{M\alpha \Rightarrow M\beta} }  \end{equation} </math>
 Now observe that the following formulas are equivalent<br />
 <math>\begin{align*}{}

@@ Linia 87: / Linia 87: @@
 <math>\begin{equation}\tag{Ax ;}\fbox{[K; M]\alpha \Leftrightarrow [K][M]\alpha } \end{equation} </math><br />
 and the inference rule
-<math>\begin{equation}\tag{R2}\dfrac{\alpha \Rightarrow \beta}{M\alpha \Rightarrow M\beta}  \end{equation} </math>
+<math>\begin{equation}\fbox{\tag{R2}\dfrac{\alpha \Rightarrow \beta}{M\alpha \Rightarrow M\beta} }  \end{equation} </math>
 Now observe that the following formulas are equivalent<br />
 <math>\begin{align*}{}

@@ Linia 83: / Linia 83: @@
 I.e. ''the execution of three instructions causes swap of the values of variables'' <math> c_1, c_2 </math>.<br />
 '''Proof''' uses two axioms of algorithmic logic: <br />
-<math>\begin{equation}\tag{Ax:=}[x:=\tau]\alpha \Leftrightarrow \alpha(x/\tau) \end{equation} </math> <br />
+<math>\begin{equation}\tag{Ax:=}\fbox{[x:=\tau]\alpha \Leftrightarrow \alpha(x/\tau)} \end{equation} </math> <br />
 this axiom of assignment instruction reads: ''formula '' <math>\alpha(x/\tau)</math> '' holds iff after execution of instruction  '' <math>x:=\tau</math> ''formula  ''<math>\alpha</math> '' holds.''<br />
-<math>\begin{equation}\tag{Ax ;}[K; M]\alpha \Leftrightarrow [K][M]\alpha  \end{equation} </math><br />
+<math>\begin{equation}\tag{Ax ;}\fbox{[K; M]\alpha \Leftrightarrow [K][M]\alpha } \end{equation} </math><br />
 and the inference rule
 <math>\begin{equation}\tag{R2}\dfrac{\alpha \Rightarrow \beta}{M\alpha \Rightarrow M\beta}  \end{equation} </math>

@@ Linia 91: / Linia 91: @@
 <math>\begin{align*}{}
 &(c_1 =a \land c_2=b)&             & \\
-\Rightleftarrow &(c_1 =a \land c_2=b \land c1=a)&             & \mbox{by propositional calculus} \\
+\Leftrightarrow &(c_1 =a \land c_2=b \land c1=a)&             & \mbox{by propositional calculus} \\
-\Rightleftarrow & [c_3:=c_1](c_3=a \land c_2 =b \land c_3=a) &       & \mbox{by Ax :=} \\
+\Leftrightarrow & [c_3:=c_1](c_3=a \land c_2 =b \land c_3=a) &       & \mbox{by Ax :=} \\
-\Rightleftarrow &  [c_3:=c_1][c_1:=c_2](c_3=a \land c_1 =b \land c_3=a) &       & \mbox{by Ax := and R2} \\
+\Leftrightarrow &  [c_3:=c_1][c_1:=c_2](c_3=a \land c_1 =b \land c_3=a) &       & \mbox{by Ax := and R2} \\
-\Rightleftarrow &  [c_3:=c_1; c_1:=c_2](c_3=a \land c_1 =b \land c_3=a) &       & \mbox{by Ax ;} \\
+\Leftrightarrow &  [c_3:=c_1; c_1:=c_2](c_3=a \land c_1 =b \land c_3=a) &       & \mbox{by Ax ;} \\
-\Rightleftarrow &  [c_3:=c_1; c_1:=c_2][c_2 :=c_3](c_2=a \land c_1 =b \land c_3=a) &       & \mbox{by Ax := and R2}\\
+\Leftrightarrow &  [c_3:=c_1; c_1:=c_2][c_2 :=c_3](c_2=a \land c_1 =b \land c_3=a) &       & \mbox{by Ax := and R2}\\
-\Rightleftarrow &  [c_3:=c_1; c_1:=c_2; c_2 :=c_3](c_2=a \land c_1 =b \land c_3=a) &       & \mbox{by Ax ;} \\
+\Leftrightarrow &  [c_3:=c_1; c_1:=c_2; c_2 :=c_3](c_2=a \land c_1 =b \land c_3=a) &       & \mbox{by Ax ;} \\
 \end{align*}  </math>

@@ Linia 81: / Linia 81: @@
 <big>Lemma</big><br />
 <math>(c_1=a \land c_2=b)\Rightarrow [c_3:=c_1; c_1:=c_2; c_2:=c_3](c_1=b \land c_2=a) </math><br />
-I.e. ''the execution of three instructions causes swap of the values of variables'' <math> c_1, c_2 </math>.,br />
+I.e. ''the execution of three instructions causes swap of the values of variables'' <math> c_1, c_2 </math>.<br />
 '''Proof''' uses two axioms of algorithmic logic: <br />
 <math>\begin{equation}\tag{Ax:=}[x:=\tau]\alpha \Leftrightarrow \alpha(x/\tau) \end{equation} </math> <br />

@@ Linia 78: / Linia 78: @@
 Guess what will print this program.
-One need not to guess. We have much better tool.
+One need not to guess. We have much better tool. <br />
 <big>Lemma</big><br />
 <math>(c_1=a \land c_2=b)\Rightarrow [c_3:=c_1; c_1:=c_2; c_2:=c_3](c_1=b \land c_2=a) </math>