Axioms of algorithmic logic: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
(→‎Axioms of AL)
(→‎Axioms of algorithmic logic)
 
(Nie pokazano 19 pośrednich wersji utworzonych przez tego samego użytkownika)
Linia 2: Linia 2:
 
== Axioms of propositional logic ==
 
== Axioms of propositional logic ==
 
We are quoting the axiom system of Helena Rasiowa and Roman Sikorski<br />
 
We are quoting the axiom system of Helena Rasiowa and Roman Sikorski<br />
−
 
+
Any formula of a scheme listed below is an axiom of algorithmic logic. The signs <math>\alpha, \beta,  \delta</math>  are to be replaced by a formula.
 
<span style="color: Blue"><math>Ax_1 \qquad ((\alpha\Rightarrow\beta
 
<span style="color: Blue"><math>Ax_1 \qquad ((\alpha\Rightarrow\beta
 
)\Rightarrow((\beta\Rightarrow\delta)\Rightarrow(\alpha
 
)\Rightarrow((\beta\Rightarrow\delta)\Rightarrow(\alpha
 
\Rightarrow\delta)))</math>
 
\Rightarrow\delta)))</math>
  
−
<span style="color: Blue"><math>Ax_2$] $(\alpha\Longrightarrow(\alpha
+
<span style="color: Blue"><math>Ax_2 \qquad(\alpha\Rightarrow(\alpha
−
\vee\beta))$
+
\vee\beta))</math>
  
−
<span style="color: Blue"><math>Ax_3$] $(\beta\Longrightarrow(\alpha\vee\beta))$%
+
<span style="color: Blue"><math>Ax_3 \qquad (\beta\Longrightarrow(\alpha\vee\beta))</math>
  
−
<span style="color: Blue"><math>Ax_4$] $((\alpha\Longrightarrow\delta)~\Longrightarrow((\beta
+
<span style="color: Blue"><math>Ax_4 \qquad((\alpha\Longrightarrow\delta)~\Longrightarrow((\beta
 
\Longrightarrow\delta)~\Longrightarrow~((\alpha\vee\beta
 
\Longrightarrow\delta)~\Longrightarrow~((\alpha\vee\beta
−
)\Longrightarrow\delta)))$
+
)\Longrightarrow\delta)))</math>
  
−
<span style="color: Blue"><math>Ax_5$] $((\alpha\wedge\beta
+
<span style="color: Blue"><math>Ax_5 \qquad((\alpha\wedge\beta
−
)\Longrightarrow\alpha)$
+
)\Longrightarrow\alpha)</math>
  
−
<span style="color: Blue"><math>Ax_6$] $((\alpha\wedge\beta
+
<span style="color: Blue"><math>Ax_6 \qquad((\alpha\wedge\beta
−
)\Longrightarrow\beta)$
+
)\Longrightarrow\beta)</math>
  
−
<span style="color: Blue"><math>Ax_7$] $((\delta\Longrightarrow\alpha
+
<span style="color: Blue"><math>Ax_7 \qquad((\delta\Longrightarrow\alpha
 
)\Longrightarrow((\delta\Longrightarrow\beta)\Longrightarrow(\delta
 
)\Longrightarrow((\delta\Longrightarrow\beta)\Longrightarrow(\delta
−
\Longrightarrow(\alpha\wedge\beta))))$
+
\Longrightarrow(\alpha\wedge\beta))))</math>
  
−
<span style="color: Blue"><math>Ax_8$] $((\alpha
+
<span style="color: Blue"><math>Ax_8 \qquad ((\alpha
 
\Longrightarrow(\beta\Longrightarrow\delta))\equiv((\alpha\wedge\beta
 
\Longrightarrow(\beta\Longrightarrow\delta))\equiv((\alpha\wedge\beta
−
)\Longrightarrow\delta))$
+
)\Longrightarrow\delta))</math>
  
−
<span style="color: Blue"><math>Ax_9$] $((\alpha\wedge\lnot\alpha
+
<span style="color: Blue"><math>Ax_9 \qquad\ ((\alpha\wedge\lnot\alpha
−
)\Longrightarrow\beta)$
+
)\Longrightarrow\beta)</math>
 +
 
 +
<span style="color: Blue"><math>Ax_{10} \qquad ((\alpha\Longrightarrow
 +
(\alpha\wedge\lnot\alpha))\Longrightarrow\lnot\alpha)</math>
 +
 
 +
<span style="color: Blue"><math>Ax_{11} \qquad (\alpha\vee\lnot\alpha)</math><span>
  
−
<span style="color: Blue"><math>Ax_{10}$] $((\alpha\Longrightarrow
 
−
(\alpha\wedge\lnot\alpha))\Longrightarrow\lnot\alpha)$
 
−
\item[$Ax_{11}$] $(\alpha\vee\lnot\alpha)$<span>
 
 
== Axioms of predicate calculus ==
 
== Axioms of predicate calculus ==
−
\item[$Ax_{12}$] $((x:=\tau
+
<span style="color: Blue"><math>Ax_{12} \qquad ((x:=\tau
 
)true\Longrightarrow((\forall x)\alpha(x)\Longrightarrow(x:=\tau)\alpha
 
)true\Longrightarrow((\forall x)\alpha(x)\Longrightarrow(x:=\tau)\alpha
−
(x)))$ \ \ \newline
+
(x))) \\  
−
\qquad\qquad{\small where term }$\tau${\small\ is of the same type as
+
\qquad\qquad {\small where\ term\ }\tau {\ \small\ is\ of\ the\ same\ type\ as\
−
the variable x}
+
the\ variable\ x}</math>
−
\item[$Ax_{13}$] $(\forall x)\alpha(x)\equiv\lnot
+
<span style="color: Blue"><math>Ax_{13} \qquad (\forall x)\alpha(x)\equiv\lnot
−
(\exists x)\lnot\alpha(x)$
+
(\exists x)\lnot\alpha(x)</math>
−
\item[$Ax_{14}$] $K((\exists x)\alpha
+
 
−
(x))\equiv(\exists y)(K\alpha(x/y))$ \begin{small}for $y\notin V(K)$                                                      \end{small}
+
<span style="color: Blue"><math>Ax_{14} \qquad K((\exists x)\alpha
−
\item[$Ax_{15}$] $K(\alpha\vee\beta)\equiv((K\alpha)\vee(K\beta))$
+
(x))\equiv(\exists y)(K\alpha(x/y))\ \ \ \ \ \ \ \ \ \ \ \ \  \ for\ y\notin V(K) </math></span>
−
\item[$Ax_{16}$] $K(\alpha\wedge\beta)\equiv((K\alpha)\wedge(K\beta))$%
+
 
−
\item[$Ax_{17}$] $K(\lnot\alpha)\Longrightarrow\lnot(K\alpha)$%
+
== Axioms of algorithmic logic == 
−
\item[$Ax_{18}$] $((x:=\tau)\gamma\equiv(\gamma(x/\tau)\wedge
+
<span style="color: Blue"><math>Ax_{14} \qquad K((\exists x)\alpha
−
(x:=\tau)true))~\wedge((q:=\gamma\prime)\gamma\equiv\gamma(q/\gamma
+
(x))\equiv(\exists y)(K\alpha(x/y)) </math></span> for <math> y\notin V(K) </math>
−
\prime))$
+
                                             
−
\item[$Ax_{19}$] \textbf{begin} $K;M$ \textbf{end} $\alpha
+
<span style="color: Blue"><math>Ax_{15} \qquad K(\alpha\vee\beta)\equiv((K\alpha)\vee(K\beta))</math></span>
−
\equiv K(M\alpha)$
+
 
−
\item[$Ax_{20}$] \textbf{if} $\gamma$ \textbf{then} $K
+
<span style="color: Blue"><math>Ax_{16} \qquad K(\alpha\wedge\beta)\equiv((K\alpha)\wedge(K\beta))</math></span>
−
$ \textbf{else} $M$ \textbf{fi} $\alpha\equiv((\lnot\gamma\wedge M\alpha
+
 
−
)\vee(\gamma\wedge K\alpha))$
+
<span style="color: Blue"><math>Ax_{17} \qquad K(\lnot\alpha)\Longrightarrow\lnot(K\alpha)</math></span>
−
\item[$Ax_{21}$] \textbf{while}~
+
 
−
$\gamma$~\textbf{do}~$K$~\textbf{od}~$\alpha\equiv((\lnot\gamma\wedge\alpha
+
<span style="color: Blue"><math>Ax_{18} \qquad ((x:=\tau)\gamma\equiv(\gamma(x/\tau)\wedge
−
)\vee(\gamma\wedge K($\textbf{while}~$\gamma$~\textbf{do}~$K$~\textbf{od}$%
+
(x:=\tau)true))~\wedge((q:=\gamma^\prime)\gamma\equiv\gamma(q/\gamma^
−
(\lnot\gamma\wedge\alpha))))$
+
\prime))</math></span>
−
\item[$Ax_{22}$] $\displaystyle{\bigcap K\alpha\equiv
+
 
−
(\alpha\wedge(K\bigcap K\alpha))}$
+
<span style="color: Blue"><math>Ax_{19} \qquad \textbf{begin } K;M \textbf{ end}\, \alpha
−
\item[$Ax_{23}$] $\displaystyle{\bigcup K\alpha
+
\equiv K(M\alpha)</math></span>
−
\equiv(\alpha\vee(K\bigcup K\alpha))}$ </span>
+
 
 +
<span style="color: Blue"><math>Ax_{20} \qquad  \textbf{if}\ \gamma\ \textbf{then}\ K
 +
\ \textbf{else } M \textbf{ fi}\, \alpha\equiv((\lnot\gamma\wedge M\alpha
 +
)\vee(\gamma\wedge K\alpha))</math></span>
 +
 
 +
<span style="color: Blue"><math>Ax_{21} \qquad  \textbf{while }\gamma \textbf{ do }K\textbf{ od}\,\alpha\equiv((\lnot\gamma\wedge\alpha
 +
)\vee(\gamma\wedge K(\textbf{while }\gamma\textbf{ do }K\textbf{ od}
 +
(\lnot\gamma\wedge\alpha))))</math></span>
 +
 
 +
<span style="color: Blue"><math>Ax_{22} \qquad \bigcap K\alpha\equiv
 +
(\alpha\wedge(K\bigcap K\alpha))</math></span>
 +
 
 +
<span style="color: Blue"><math>Ax_{23} \qquad \bigcup K\alpha
 +
\equiv(\alpha\vee(K\bigcup K\alpha))</math> </span>

Aktualna wersja na dzień 18:08, 19 lis 2015

The axioms are grouped in three sets

Axioms of propositional logic

We are quoting the axiom system of Helena Rasiowa and Roman Sikorski
Any formula of a scheme listed below is an axiom of algorithmic logic. The signs [math]\alpha, \beta, \delta[/math] are to be replaced by a formula. [math]Ax_1 \qquad ((\alpha\Rightarrow\beta )\Rightarrow((\beta\Rightarrow\delta)\Rightarrow(\alpha \Rightarrow\delta)))[/math]

[math]Ax_2 \qquad(\alpha\Rightarrow(\alpha \vee\beta))[/math]

[math]Ax_3 \qquad (\beta\Longrightarrow(\alpha\vee\beta))[/math]

[math]Ax_4 \qquad((\alpha\Longrightarrow\delta)~\Longrightarrow((\beta \Longrightarrow\delta)~\Longrightarrow~((\alpha\vee\beta )\Longrightarrow\delta)))[/math]

[math]Ax_5 \qquad((\alpha\wedge\beta )\Longrightarrow\alpha)[/math]

[math]Ax_6 \qquad((\alpha\wedge\beta )\Longrightarrow\beta)[/math]

[math]Ax_7 \qquad((\delta\Longrightarrow\alpha )\Longrightarrow((\delta\Longrightarrow\beta)\Longrightarrow(\delta \Longrightarrow(\alpha\wedge\beta))))[/math]

[math]Ax_8 \qquad ((\alpha \Longrightarrow(\beta\Longrightarrow\delta))\equiv((\alpha\wedge\beta )\Longrightarrow\delta))[/math]

[math]Ax_9 \qquad\ ((\alpha\wedge\lnot\alpha )\Longrightarrow\beta)[/math]

[math]Ax_{10} \qquad ((\alpha\Longrightarrow (\alpha\wedge\lnot\alpha))\Longrightarrow\lnot\alpha)[/math]

[math]Ax_{11} \qquad (\alpha\vee\lnot\alpha)[/math]

Axioms of predicate calculus

[math]Ax_{12} \qquad ((x:=\tau )true\Longrightarrow((\forall x)\alpha(x)\Longrightarrow(x:=\tau)\alpha (x))) \\ \qquad\qquad {\small where\ term\ }\tau {\ \small\ is\ of\ the\ same\ type\ as\ the\ variable\ x}[/math] [math]Ax_{13} \qquad (\forall x)\alpha(x)\equiv\lnot (\exists x)\lnot\alpha(x)[/math]

[math]Ax_{14} \qquad K((\exists x)\alpha (x))\equiv(\exists y)(K\alpha(x/y))\ \ \ \ \ \ \ \ \ \ \ \ \ \ for\ y\notin V(K) [/math]

Axioms of algorithmic logic

[math]Ax_{14} \qquad K((\exists x)\alpha (x))\equiv(\exists y)(K\alpha(x/y)) [/math] for [math] y\notin V(K) [/math]

[math]Ax_{15} \qquad K(\alpha\vee\beta)\equiv((K\alpha)\vee(K\beta))[/math]

[math]Ax_{16} \qquad K(\alpha\wedge\beta)\equiv((K\alpha)\wedge(K\beta))[/math]

[math]Ax_{17} \qquad K(\lnot\alpha)\Longrightarrow\lnot(K\alpha)[/math]

[math]Ax_{18} \qquad ((x:=\tau)\gamma\equiv(\gamma(x/\tau)\wedge (x:=\tau)true))~\wedge((q:=\gamma^\prime)\gamma\equiv\gamma(q/\gamma^ \prime))[/math]

[math]Ax_{19} \qquad \textbf{begin } K;M \textbf{ end}\, \alpha \equiv K(M\alpha)[/math]

[math]Ax_{20} \qquad \textbf{if}\ \gamma\ \textbf{then}\ K \ \textbf{else } M \textbf{ fi}\, \alpha\equiv((\lnot\gamma\wedge M\alpha )\vee(\gamma\wedge K\alpha))[/math]

[math]Ax_{21} \qquad \textbf{while }\gamma \textbf{ do }K\textbf{ od}\,\alpha\equiv((\lnot\gamma\wedge\alpha )\vee(\gamma\wedge K(\textbf{while }\gamma\textbf{ do }K\textbf{ od} (\lnot\gamma\wedge\alpha))))[/math]

[math]Ax_{22} \qquad \bigcap K\alpha\equiv (\alpha\wedge(K\bigcap K\alpha))[/math]

[math]Ax_{23} \qquad \bigcup K\alpha \equiv(\alpha\vee(K\bigcup K\alpha))[/math]

Źródło „http://lem12.uksw.edu.pl/index.php?title=Axioms_of_algorithmic_logic&oldid=2153”