Axioms of algorithmic logic: Różnice pomiędzy wersjami
(→Axioms of propositional logic) |
(→Axioms of algorithmic logic) |
||
(Nie pokazano 14 pośrednich wersji utworzonych przez tego samego użytkownika) | |||
Linia 39: | Linia 39: | ||
== Axioms of predicate calculus == | == Axioms of predicate calculus == | ||
− | + | <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))) | + | (x))) \\ |
− | \qquad\qquad{\small where term } | + | \qquad\qquad {\small where\ term\ }\tau {\ \small\ is\ of\ the\ same\ type\ as\ |
− | the variable x} | + | the\ variable\ x}</math> |
− | + | <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> |
− | + | ||
− | (x))\equiv(\exists y)(K\alpha(x/y)) | + | <span style="color: Blue"><math>Ax_{14} \qquad K((\exists x)\alpha |
− | == Axioms of algorithmic logic == | + | (x))\equiv(\exists y)(K\alpha(x/y))\ \ \ \ \ \ \ \ \ \ \ \ \ \ for\ y\notin V(K) </math></span> |
− | \ | + | |
− | + | == Axioms of algorithmic logic == | |
− | + | <span style="color: Blue"><math>Ax_{14} \qquad K((\exists x)\alpha | |
− | + | (x))\equiv(\exists y)(K\alpha(x/y)) </math></span> for <math> y\notin V(K) </math> | |
− | (x:=\tau)true))~\wedge((q:=\gamma\prime)\gamma\equiv\gamma(q/\gamma | + | |
− | \prime)) | + | <span style="color: Blue"><math>Ax_{15} \qquad K(\alpha\vee\beta)\equiv((K\alpha)\vee(K\beta))</math></span> |
− | + | ||
− | \equiv K(M\alpha) | + | <span style="color: Blue"><math>Ax_{16} \qquad K(\alpha\wedge\beta)\equiv((K\alpha)\wedge(K\beta))</math></span> |
− | + | ||
− | + | <span style="color: Blue"><math>Ax_{17} \qquad K(\lnot\alpha)\Longrightarrow\lnot(K\alpha)</math></span> | |
− | )\vee(\gamma\wedge K\alpha)) | + | |
− | + | <span style="color: Blue"><math>Ax_{18} \qquad ((x:=\tau)\gamma\equiv(\gamma(x/\tau)\wedge | |
− | + | (x:=\tau)true))~\wedge((q:=\gamma^\prime)\gamma\equiv\gamma(q/\gamma^ | |
− | )\vee(\gamma\wedge K( | + | \prime))</math></span> |
− | (\lnot\gamma\wedge\alpha)))) | + | |
− | + | <span style="color: Blue"><math>Ax_{19} \qquad \textbf{begin } K;M \textbf{ end}\, \alpha | |
− | (\alpha\wedge(K\bigcap K\alpha)) | + | \equiv K(M\alpha)</math></span> |
− | + | ||
− | \equiv(\alpha\vee(K\bigcup K\alpha)) | + | <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]