-\item $\neg (* \, R \bot)$
-\item $* \, R \, (t_1=t_2)$ iff $t_1=t_2$ is true ...
-\item $<f,g> R P\land Q$ iff $f R P$ and $g R Q$
-\item $f R P\to Q$ iff for any $m$ such that $m R P$, $(f m) \, R \, Q$
-\item $f R \forall x.P$ iff for any $n$ $(f \underline{n}) \, R \, P$
-\item $<n,g> R \exists x.P$ iff $g R P[n/x]$
+\item $\neg (* \R \bot)$
+\item $* \R (t_1=t_2)$ iff $t_1=t_2$ is true ...
+\item $<f,g> \R (P\land Q)$ iff $f \R P$ and $g \R Q$
+\item $f \R (P\to Q)$ iff for any $m$ such that $m \R P$, $(f \,m) \R Q$
+\item $f \R (\forall x.P)$ iff for any natural number $n$ $(f n) \R P[\underline{n}/x]$
+\item $<n,g> \R (\exists x.P)$ iff $g \R P[\underline{n}/x]$
+\end{itemize}
+
+\noindent
+We proceed to prove that alla axioms $ax:Ax$ are realized by $\sem{ax}$.
+
+\begin{itemize}
+\item $nat\_ind$. We must prove that the recursion schema $R$ realizes the
+induction principle. To this aim we must prove that for any $a$ and $f$ such that
+$a \R P(0)$ and $f \R \forall x.(P(x) \to P(S(x)))$, and any natural number
+$n$, $(R \,a \,f \,n) \R P(\underline{n})$.\\
+We proceed by induction on n.\\
+If $n=O$, $(R \,a \,f \,O) = a$ and by hypothesis $a \R P(0)$.\\
+Suppose by induction that $(R \,a \,f \,n) \R P(\underline{n})$, and let us prove that
+the relation still holds for $n+1$.
+By definition $(R \,a \,f \,(n+1)) = f \,n \,(R \,a \,f \,n)$,
+and since $f \R \forall x.(P(x) \to P(S(x)))$,
+$(f n (R a f n)) \R P(S(\underline{n}))=P(\underline{n+1})$.