added few proofs

diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex
index 1e1b6c46c30ab488598a54077be525408591878b..db212276dd5de6f777fe9cb5ccde04fc82ca1939 100644 (file)
--- a/helm/papers/system_T/t.tex
+++ b/helm/papers/system_T/t.tex
@@ -10,6 +10,9 @@
 \newcommand{\N}{\,\mathbb{N}\,}
 \newcommand{\NT}{\,\mathbb{N}\,}
 \newcommand{\NH}{\,\mathbb{N}\,}
+\renewcommand{\star}{\ast}
+\newcommand{\one}{\mathbb{1}}
+\renewcommand{\times}{\cdot}
 \title{...}
 \author{...}
 
@@ -38,8 +41,8 @@
 \item $injS: \forall x,y.S(x) = S(y) \to x=y$
 \item $plus\_O:\forall x.x+0=x$
 \item $plus\_S:\forall x,y.x+S(y)=S(x+y)$ 
-\item $times\_O:\forall x.x*0=0$
-\item $times\_S:\forall x,y.x*S(y)=x+(x*y)$ 
+\item $times\_O:\forall x.x\times0=0$
+\item $times\_S:\forall x,y.x\times S(y)=x+(x\times y)$ 
 \end{itemize}
 
 \noindent
@@ -97,14 +100,14 @@ For any type T of system T $\bot_T: 1 \to T$  is inuctively defined as follows:
 \item $\sem{ex\_ind} = (\lambda f:(\N \to \sem{P} \to \sem{Q}).
 \lambda p:\N\times \sem{P}.f (fst \,p) (snd \,p)$. 
 \item $\sem{ex\_intro} = \lambda x:\N.\lambda f:\sem{P}.<x,f>$
-\item $\sem{fst} = fst$
-\item $\sem{snd} = snd$
+\item $\sem{fst} = \pi_1$
+\item $\sem{snd} = \pi_2$
 \item $\sem{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.<x,y>$
 \item $\sem{false\_ind} = \bot_{\sem{Q}}$
-\item $\sem{discriminate} = \lambda \_:\N.\lambda \_:1.*$
-\item $\sem{injS}= \lambda \_:\N. \lambda \_:\N.\lambda \_:1.*$
-\item $\sem{plus\_O} = \sem{times\_O} = \lambda \_:\N.*$
-\item $\sem{plus\_S} = \sem{times_S} = \lambda \_:\N. \lambda \_:\N.*$
+\item $\sem{discriminate} = \lambda \_:\N.\lambda \_:1.\star$
+\item $\sem{injS}= \lambda \_:\N. \lambda \_:\N.\lambda \_:1.\star$
+\item $\sem{plus\_O} = \sem{times\_O} = \lambda \_:\N.\star$
+\item $\sem{plus\_S} = \sem{times_S} = \lambda \_:\N. \lambda \_:\N.\star$
 \end{itemize}
 
 In the case of structured proofs:
@@ -119,7 +122,7 @@ In the case of structured proofs:
 The realizability relation is a relation $f \R P$ where $f: \sem{P}$.
 In particular:
 \begin{itemize}
-\item $\neg (* \R \bot)$
+\item $\neg (\star \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$
@@ -152,7 +155,9 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$.
   $p~\R~\exists~x:(P~x)$, then $\underline{ex\_ind}~f~p \R Q$.\\ 
   $p$ is a couple $<n_p,g_p>$ such that $g_p \R P[\underline{n_p}/x]$, while
   $f$ is a function such that forall $n$ and for all $m \R P[\underline{n}/x]$
-  then $f~n~m \R Q$.  Exapanding the definition of $\underline{ex\_ind}$, $fst$
+  then $f~n~m \R Q$ (note that $x$ is not free in $Q$ so $[\underline{n}/x]$
+  affects only $P$).\\
+  Exapanding the definition of $\underline{ex\_ind}$, $fst$
   and $snd$ we obtain $f~n_p~g_p$ that we know is in relation $\R$ with $Q$
   since $g_p \R P[\underline{n_p}/x]$.
 
@@ -168,6 +173,25 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$.
   Expanding the definition of $\underline{ex\_intro}$ we have
   $<n,m> \R \exists x.P(x)$ that is true since $m \R P[\underline{n}/x]$.
 
+\item $fst$.
+  Wehave to prove that $\pi_1 \R P \land Q \to P$, that is equal to proving
+  that for each $m \R P \land Q$ then $\pi_1~m \R P$ .
+  $m$ must be a couple $<f_m,g_m>$ such that $f_m \R P$ and $g_m \R Q$.
+  So we conclude that $\pi_1~m$ reduces to $f_m$ that is in relation $\R$
+  with $P$.
+
+\item $snd$. The same for $fst$.
+
+\item $conj$. 
+  We have to prove that 
+  $$\lambda x:\sem{P}. \lambda y:\sem{Q}.<x,y> \R P \to Q \to P \land Q$$
+  Following the definition of $\R$ we have to show that 
+  foreach $m \R P$ and foreach $n \R Q$ then 
+  $(\lambda x:\sem{P}. \lambda y:\sem{Q}.<x,y>)~m~n \R P \land Q$.\\
+  This is the same of $<m,n> \R P \land Q$ that is verified since 
+  $m \R P$ and $n \R Q$.
+
+
 \item $false\_ind$. 
   We have to prove that $\bot_{\sem{Q}} \R \bot \to Q$. 
   Trivial, since there is no $m \R \bot$.
@@ -180,8 +204,30 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$.
   We have to prove that for each $n_1$ and $n_2$\\
   $\lambda \_:\N. \lambda \_:\N.\lambda \_:1.*~n_1~n_2 \R 
   (S(x)=S(y)\to x=y)[n_1/x][n_2/y]$.\\
-  Assuming $m \R S(n_1)=S(n_2)$ we have to prove
-
+  We assume that $m \R S(n_1)=S(n_2)$ and we have to show that 
+  $\lambda \_:\N. \lambda \_:\N.\lambda \_:1.*~n_1~n_2~m$ that reduces to
+  $*$ is in relation $\R$ with $n_1=n_2$. Since in the standard model of 
+  natural numbers  $S(n_1)=S(n_2)$ implies $n_1=n_2$ we have that 
+  $* \R n_1=n_2$.
+
+\item $plus\_O$. 
+  Since in the standard model for natural numbers $0$ is the neutral element
+  for addition $\lambda \_:\N.\star \R \forall x.x + 0 = x$.
+
+\item $plus\_S$.
+  In the standard model of natural numbers the addition of two numbers is the 
+  operation of counting the second starting from the first. So
+  $$\lambda \_:\N. \lambda \_:\N. \star \R \forall x,y.x+S(y)=S(x+y)$$.
+
+\item $times\_O$.
+  Since in the standard model for natural numbers $0$ is the absorbing element
+  for multiplication $\lambda \_:\N.\star \R \forall x.x \times 0 = x$.
+  
+\item $times\_S$.
+  In the standard model of natural numbers the multiplications of two 
+  numbers is the operation of adding the first to himself a number of times
+  equal to the second number. So
+  $$\lambda \_:\N. \lambda \_:\N. \star \R \forall x,y.x+S(y)=S(x+y)$$.
   
 
 \end{itemize}