Axioms of algorithmic logic: Różnice pomiędzy wersjami
(→Axioms of propositional logic) |
(→Axioms of propositional logic) |
||
| Linia 10: | Linia 10: | ||
\vee\beta))</math> | \vee\beta))</math> | ||
| − | <span style="color: Blue"><math>Ax_3 | + | <span style="color: Blue"><math>Ax_3 \qquad (\beta\Longrightarrow(\alpha\vee\beta))</math> |
| − | <span style="color: Blue"><math>Ax_4 | + | <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 | + | <span style="color: Blue"><math>Ax_5 \qquad((\alpha\wedge\beta |
| − | )\Longrightarrow\alpha) | + | )\Longrightarrow\alpha)</math> |
| − | <span style="color: Blue"><math>Ax_6 | + | <span style="color: Blue"><math>Ax_6 \qquad((\alpha\wedge\beta |
| − | )\Longrightarrow\beta) | + | )\Longrightarrow\beta)</math> |
| − | <span style="color: Blue"><math>Ax_7 | + | <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$] $((\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 | + | <span style="color: Blue"><math>Ax_9 \qquad ((\alpha\wedge\lnot\alpha |
| − | )\Longrightarrow\beta) | + | )\Longrightarrow\beta)</math> |
| − | <span style="color: Blue"><math>Ax_{10} | + | <span style="color: Blue"><math>Ax_{10} \qquad ((\alpha\Longrightarrow |
| − | (\alpha\wedge\lnot\alpha))\Longrightarrow\lnot\alpha) | + | (\alpha\wedge\lnot\alpha))\Longrightarrow\lnot\alpha)</math> |
| − | \item[$Ax_{11} | + | |
| + | \item[$Ax_{11} \qquad (\alpha\vee\lnot\alpha)</math><span> | ||
== Axioms of predicate calculus == | == Axioms of predicate calculus == | ||
\item[$Ax_{12}$] $((x:=\tau | \item[$Ax_{12}$] $((x:=\tau | ||
| Linia 45: | Linia 46: | ||
(\exists x)\lnot\alpha(x)$ | (\exists x)\lnot\alpha(x)$ | ||
\item[$Ax_{14}$] $K((\exists x)\alpha | \item[$Ax_{14}$] $K((\exists x)\alpha | ||
| − | (x))\equiv(\exists y)(K\alpha(x/y))$ \begin{small}for $y\notin V(K)$ | + | (x))\equiv(\exists y)(K\alpha(x/y))$ \begin{small}for $y\notin V(K)$ \end{small} |
| + | == Axioms of algorithmic logic == | ||
\item[$Ax_{15}$] $K(\alpha\vee\beta)\equiv((K\alpha)\vee(K\beta))$ | \item[$Ax_{15}$] $K(\alpha\vee\beta)\equiv((K\alpha)\vee(K\beta))$ | ||
\item[$Ax_{16}$] $K(\alpha\wedge\beta)\equiv((K\alpha)\wedge(K\beta))$% | \item[$Ax_{16}$] $K(\alpha\wedge\beta)\equiv((K\alpha)\wedge(K\beta))$% | ||
Wersja z 17:19, 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
[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$] $((\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]
\item[$Ax_{11} \qquad (\alpha\vee\lnot\alpha)</math>
Axioms of predicate calculus
\item[$Ax_{12}$] $((x:=\tau )true\Longrightarrow((\forall x)\alpha(x)\Longrightarrow(x:=\tau)\alpha (x)))$ \ \ \newline \qquad\qquad{\small where term }$\tau${\small\ is of the same type as the variable x} \item[$Ax_{13}$] $(\forall x)\alpha(x)\equiv\lnot (\exists x)\lnot\alpha(x)$ \item[$Ax_{14}$] $K((\exists x)\alpha (x))\equiv(\exists y)(K\alpha(x/y))$ \begin{small}for $y\notin V(K)$ \end{small}
Axioms of algorithmic logic
\item[$Ax_{15}$] $K(\alpha\vee\beta)\equiv((K\alpha)\vee(K\beta))$ \item[$Ax_{16}$] $K(\alpha\wedge\beta)\equiv((K\alpha)\wedge(K\beta))$% \item[$Ax_{17}$] $K(\lnot\alpha)\Longrightarrow\lnot(K\alpha)$% \item[$Ax_{18}$] $((x:=\tau)\gamma\equiv(\gamma(x/\tau)\wedge (x:=\tau)true))~\wedge((q:=\gamma\prime)\gamma\equiv\gamma(q/\gamma \prime))$ \item[$Ax_{19}$] \textbf{begin} $K;M$ \textbf{end} $\alpha \equiv K(M\alpha)$ \item[$Ax_{20}$] \textbf{if} $\gamma$ \textbf{then} $K $ \textbf{else} $M$ \textbf{fi} $\alpha\equiv((\lnot\gamma\wedge M\alpha )\vee(\gamma\wedge K\alpha))$ \item[$Ax_{21}$] \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))))$ \item[$Ax_{22}$] $\displaystyle{\bigcap K\alpha\equiv (\alpha\wedge(K\bigcap K\alpha))}$ \item[$Ax_{23}$] $\displaystyle{\bigcup K\alpha \equiv(\alpha\vee(K\bigcup K\alpha))}$
