From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 11 Oct 2005 08:28:47 +0000 (+0000)
Subject: realizability for the induction principle.
X-Git-Tag: V_0_7_2_3~222
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0e1469c982280f2606c4b35253a2d5ba91cb16e4;p=helm.git

realizability for the induction principle.
---

diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex
index 30cbd5732..d3ca4e6a1 100644
--- a/helm/papers/system_T/t.tex
+++ b/helm/papers/system_T/t.tex
@@ -1,11 +1,12 @@
 \documentclass[a4paper]{article}
 \pagestyle{headings}
 %\usepackage{graphicx}
-\usepackage{amssymb,amsmath}
+\usepackage{amssymb,amsmath,mathrsfs}
 %\usepackage{hyperref}
 %\usepackage{picins}
 
 \newcommand{\sem}[1]{[\![ #1 ]\!]}
+\newcommand{\R}{\,\mathscr{R}\,}
 \title{...}
 \author{...}
 
@@ -105,22 +106,39 @@ For any type T of system T $\bot_T: 1 \to T$  is inuctively defined as follows:
 
 In the case of structured proofs:
 \begin{itemize}
-\item \sem{M N} = \sem{M} \sem{N}
-\item \sem{\lambda x:A.M} = \lambda x:\sem{A}.\sem{M}
-\item \sem{\lambda x:N.M} = \lambda x:N.\sem{M}
-\item \sem{M t} = \sem{M} \sem{t}
+\item $\sem{M N} = \sem{M} \sem{N}$
+\item $\sem{\lambda x:A.M} = \lambda x:\sem{A}.\sem{M}$
+\item $\sem{\lambda x:N.M} = \lambda x:N.\sem{M}$
+\item $\sem{M t} = \sem{M} \sem{t}$
 \end{itemize}
 
 \section{Realizability}
-The realizability relation is a relation $f \, R \, P$ where $f: \sem{P}$.
+The realizability relation is a relation $f \R P$ where $f: \sem{P}$.
 In particular:
 \begin{itemize}
-\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})$.
 \end{itemize}
 
 \begin{thebibliography}{}