Algorithmic theory of natural numbers - Historia wersji

AndrzejSalwicki o 14:34, 11 lis 2024

2024-11-11T14:34:59Z

2024-11-11T14:33:48Z

2024-11-11T14:32:51Z

2024-11-11T14:25:25Z

2024-11-11T14:23:02Z

2024-11-11T14:21:24Z

2024-11-11T14:01:56Z

2024-11-11T14:00:17Z

2024-11-11T13:59:00Z

2024-11-11T13:57:54Z

@@ Linia 2: / Linia 2: @@
 '''Axioms''' <br />
 <math>    \begin{align*}
-& \tag{I}  \forall_n s(n) &\neq 0 &\\
+ \tag{I}  \forall_n s(n) &\neq 0 &\\
-&\tag{M}  \forall_n \forall_m s(n)=s(m) &\implies n=m &\\
+\tag{M}  \forall_n \forall_m s(n)=s(m) &\implies n=m &\\
-& \tag{S}  \forall_n \left\{ \begin{array}{l}m:=0; \\ \mathbf{while}\ n\neq m\ \mathbf{do}\\ \quad  m:=s(m)\\ \mathbf{od}  \end{array}\right\}&(n=m) &
+ \tag{S}  \forall_n \left\{ \begin{array}{l}m:=0; \\ \mathbf{while}\ n\neq m\ \mathbf{do}\\ \quad  m:=s(m)\\ \mathbf{od}  \end{array}\right\}&(n=m) &
 \end{align*}    </math><br />
 This set of formulas gives a complete specification of the structure <math>\mathfrak{N} </math>  of natural numbers with the successor operation. It means that any implementation whether hardware or software (e.g. by means of a class) that satisfies three  axioms listed above is correct.

@@ Linia 1: / Linia 1: @@
 The theory <math>\mathcal{ATN} </math>  of one constant 0, one one-argument functor <math>s</math> and predicate of equality =.<br />
 '''Axioms''' <br />
-<math>   \begin{center} \begin{align*}
+<math>    \begin{align*}
 & \tag{I}  \forall_n s(n) &\neq 0 &\\
 &\tag{M}  \forall_n \forall_m s(n)=s(m) &\implies n=m &\\
 & \tag{S}  \forall_n \left\{ \begin{array}{l}m:=0; \\ \mathbf{while}\ n\neq m\ \mathbf{do}\\ \quad  m:=s(m)\\ \mathbf{od}  \end{array}\right\}&(n=m) &
-\end{align*}  \end{center}  </math><br />
+\end{align*}    </math><br />
 This set of formulas gives a complete specification of the structure <math>\mathfrak{N} </math>  of natural numbers with the successor operation. It means that any implementation whether hardware or software (e.g. by means of a class) that satisfies three  axioms listed above is correct.
 It means also that if an algorithmic formula is valid in the standard model of these axioms then it has a proof with the use of program calculus.<br />

@@ Linia 1: / Linia 1: @@
 The theory <math>\mathcal{ATN} </math>  of one constant 0, one one-argument functor <math>s</math> and predicate of equality =.<br />
 '''Axioms''' <br />
-<math>   \begin{align*}
+<math>   \begin{center} \begin{align*}
 & \tag{I}  \forall_n s(n) &\neq 0 &\\
 &\tag{M}  \forall_n \forall_m s(n)=s(m) &\implies n=m &\\
 & \tag{S}  \forall_n \left\{ \begin{array}{l}m:=0; \\ \mathbf{while}\ n\neq m\ \mathbf{do}\\ \quad  m:=s(m)\\ \mathbf{od}  \end{array}\right\}&(n=m) &
-\end{align*}    </math><br />
+\end{align*}  \end{center}  </math><br />
 This set of formulas gives a complete specification of the structure <math>\mathfrak{N} </math>  of natural numbers with the successor operation. It means that any implementation whether hardware or software (e.g. by means of a class) that satisfies three  axioms listed above is correct.
 It means also that if an algorithmic formula is valid in the standard model of these axioms then it has a proof with the use of program calculus.<br />

@@ Linia 2: / Linia 2: @@
 '''Axioms''' <br />
 <math>   \begin{align*}
- \tag{I}  \forall_n s(n) &\neq 0 &\\
+& \tag{I}  \forall_n s(n) &\neq 0 &\\
-\tag{M}  \forall_n \forall_m s(n)=s(m) &\implies n=m &\\
+&\tag{M}  \forall_n \forall_m s(n)=s(m) &\implies n=m &\\
- \tag{S}  \forall_n \left\{ \begin{array}{l}m:=0; \\ \mathbf{while}\ n\neq m\ \mathbf{do}\\ \quad \\ m:=s(m)\\ \mathbf{od}  \end{array}\right\}&(n=m) &
+& \tag{S}  \forall_n \left\{ \begin{array}{l}m:=0; \\ \mathbf{while}\ n\neq m\ \mathbf{do}\\ \quad  m:=s(m)\\ \mathbf{od}  \end{array}\right\}&(n=m) &
 \end{align*}    </math><br />
 This set of formulas gives a complete specification of the structure <math>\mathfrak{N} </math>  of natural numbers with the successor operation. It means that any implementation whether hardware or software (e.g. by means of a class) that satisfies three  axioms listed above is correct.

@@ Linia 2: / Linia 2: @@
 '''Axioms''' <br />
 <math>   \begin{align*}
-  \tag{I}  \forall_n s(n) \neq 0 &\\
+  \tag{I}  \forall_n s(n) &\neq 0 &\\
-\tag{M}  \forall_n \forall_m s(n)=s(m) \implies n=m &\\
+\tag{M}  \forall_n \forall_m s(n)=s(m) &\implies n=m &\\
-  \tag{S}  \forall_n \left\{ \begin{array}{l}m:=0; \\ \mathbf{while}\ n\neq m\ \mathbf{do}\\ \quad \\ m:=s(m)\\ \mathbf{od}  \end{array}\right\}(n=m) &
+  \tag{S}  \forall_n \left\{ \begin{array}{l}m:=0; \\ \mathbf{while}\ n\neq m\ \mathbf{do}\\ \quad \\ m:=s(m)\\ \mathbf{od}  \end{array}\right\}&(n=m) &
 \end{align*}    </math><br />
 This set of formulas gives a complete specification of the structure <math>\mathfrak{N} </math>  of natural numbers with the successor operation. It means that any implementation whether hardware or software (e.g. by means of a class) that satisfies three  axioms listed above is correct.

@@ Linia 2: / Linia 2: @@
 '''Axioms''' <br />
 <math>   \begin{align*}
-& \tag{I}  \forall_n& s(n) \neq 0 \\
+& \tag{I}  \forall_n s(n) \neq 0 &\\
-  &\tag{M}  \forall_n \forall_m& s(n)=s(m) \implies n=m \\
+  &\tag{M}  \forall_n \forall_m s(n)=s(m) \implies n=m &\\
-& \tag{S}  \forall_n &\left\{ \begin{array}{l}m:=0; \\ \mathbf{while}\ n\neq m\ \mathbf{do}\\ \quad \\ m:=s(m)\\ \mathbf{od}  \end{array}\right\}(n=m) \\
+& \tag{S}  \forall_n \left\{ \begin{array}{l}m:=0; \\ \mathbf{while}\ n\neq m\ \mathbf{do}\\ \quad \\ m:=s(m)\\ \mathbf{od}  \end{array}\right\}(n=m) &
 \end{align*}    </math><br />
 This set of formulas gives a complete specification of the structure <math>\mathfrak{N} </math>  of natural numbers with the successor operation. It means that any implementation whether hardware or software (e.g. by means of a class) that satisfies three  axioms listed above is correct.

@@ Linia 1: / Linia 1: @@
 The theory <math>\mathcal{ATN} </math>  of one constant 0, one one-argument functor <math>s</math> and predicate of equality =.<br />
 '''Axioms''' <br />
-<math>\begin{array}{|l|}\hline   \begin{align*}
+<math>&   \begin{align*}
- \tag{I}  \forall_n s(n) \neq 0 \\
+& \tag{I}  \forall_n s(n) \neq 0 \\
-  \tag{M}  \forall_n \forall_m s(n)=s(m) \implies n=m \\
+  &\tag{M}  \forall_n \forall_m s(n)=s(m) \implies n=m \\
-  \tag{S}  \forall_n \left\{ \begin{array}{l}m:=0; \\ \mathbf{while}\ n\neq m\ \mathbf{do}\\ \quad \\ m:=s(m)\\ \mathbf{od}  \end{array}\right\}(n=m) \\ \hline
+  \tag{S}  \forall_n \left\{ \begin{array}{l}m:=0; \\ \mathbf{while}\ n\neq m\ \mathbf{do}\\ \quad \\ m:=s(m)\\ \mathbf{od}  \end{array}\right\}(n=m) \\
-\end{align*}  \end{array}  </math><br />
+\end{align*}    </math><br />
 This set of formulas gives a complete specification of the structure <math>\mathfrak{N} </math>  of natural numbers with the successor operation. It means that any implementation whether hardware or software (e.g. by means of a class) that satisfies three  axioms listed above is correct.
 It means also that if an algorithmic formula is valid in the standard model of these axioms then it has a proof with the use of program calculus.<br />