Tekst źródłowy strony Axioms of algorithmic logic

The axioms are grouped in three sets
== Axioms of propositional logic ==
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
)\Rightarrow((\beta\Rightarrow\delta)\Rightarrow(\alpha
\Rightarrow\delta)))</math>

<span style="color: Blue"><math>Ax_2 \qquad(\alpha\Rightarrow(\alpha
\vee\beta))</math>

<span style="color: Blue"><math>Ax_3 \qquad (\beta\Longrightarrow(\alpha\vee\beta))</math>

<span style="color: Blue"><math>Ax_4 \qquad((\alpha\Longrightarrow\delta)~\Longrightarrow((\beta
\Longrightarrow\delta)~\Longrightarrow~((\alpha\vee\beta
)\Longrightarrow\delta)))</math>

<span style="color: Blue"><math>Ax_5 \qquad((\alpha\wedge\beta
)\Longrightarrow\alpha)</math>

<span style="color: Blue"><math>Ax_6 \qquad((\alpha\wedge\beta
)\Longrightarrow\beta)</math>

<span style="color: Blue"><math>Ax_7 \qquad((\delta\Longrightarrow\alpha
)\Longrightarrow((\delta\Longrightarrow\beta)\Longrightarrow(\delta
\Longrightarrow(\alpha\wedge\beta))))</math>

<span style="color: Blue"><math>Ax_8 \qquad ((\alpha
\Longrightarrow(\beta\Longrightarrow\delta))\equiv((\alpha\wedge\beta
)\Longrightarrow\delta))</math>

<span style="color: Blue"><math>Ax_9 \qquad\ ((\alpha\wedge\lnot\alpha
)\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>

== Axioms of predicate calculus ==
<span style="color: Blue"><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>
<span style="color: Blue"><math>Ax_{13} \qquad (\forall x)\alpha(x)\equiv\lnot
(\exists x)\lnot\alpha(x)</math>

<span style="color: Blue"><math>Ax_{14} \qquad K((\exists x)\alpha
(x))\equiv(\exists y)(K\alpha(x/y))\ \ \ \ \ \ \ \ \ \ \ \ \  \ for\ y\notin V(K) </math></span>

== 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))}$ </span>