From 79a621a91ddda24398a804ff7677b5210b55f66f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 13 Oct 2005 11:37:46 +0000 Subject: [PATCH] added few proofs --- helm/papers/system_T/t.tex | 70 +++++++++++++++++++++++++++++++------- 1 file changed, 58 insertions(+), 12 deletions(-) diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex index 1e1b6c46c..db212276d 100644 --- 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}.$ -\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}.$ \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 $ \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 $$ 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 $ \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 $$ 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}. \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}.)~m~n \R P \land Q$.\\ + This is the same of $ \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} -- 2.39.2