From 6d6a2cceca53d661e478bfc6046845727e2049ce Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 10 Nov 2005 13:50:43 +0000 Subject: [PATCH] Several changes. --- helm/papers/system_T/t.tex | 56 ++++++++++++++++++++++++++++---------- 1 file changed, 42 insertions(+), 14 deletions(-) diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex index 1dba53d5b..a438e59a3 100644 --- a/helm/papers/system_T/t.tex +++ b/helm/papers/system_T/t.tex @@ -7,13 +7,15 @@ \newcommand{\semT}[1]{\ensuremath{\llbracket #1 \rrbracket}} \newcommand{\sem}[1]{\llbracket \ensuremath{#1} \rrbracket} +\newcommand{\pair}[2]{<\!#1,#2\!>} \newcommand{\R}{\;\mathscr{R}\;} \newcommand{\N}{\,\mathbb{N}\,} +\newcommand{\B}{\,\mathbb{B}\,} \newcommand{\NT}{\,\mathbb{N}\,} \newcommand{\NH}{\,\mathbb{N}\,} \renewcommand{\star}{\ast} \renewcommand{\vec}{\overrightarrow} -\newcommand{\one}{\mathscr{1}} +\newcommand{\one}{{\bf 1}} \newcommand{\mult}{\cdot} \newcommand{\ind}{Ind(X)} \newcommand{\Xind}{\ensuremath{X_{ind}}} @@ -103,6 +105,32 @@ logic and adding little by little small bits of logical power. This paper is the first step in this direction. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\section{G\"odel system T} +We shall use a variant of system T with three atomic types $\N$ (natural +numbers), $\B$ (booleans) and $\one$ (a terminal object), and two binary +type constructors $\times$ (product) and $\to$ (arrow type). + +The terms of the language comprise the usual simply typed lambda terms +with explicit pairs, plus the following additional constants: +\begin{itemize} +\item $*:\one$, +\item $true: \B$, $false:\B$, $D:A\to A \to \B \to A$ +\item $O:\N$, $S:\N \to \N$, $R:A \to (A \to \N \to A) \to \N \to A$, +\end{itemize} +Redexes comprise $\beta$-reduction +\[(\beta)\;\; \lambda x:U.M \; N \leadsto M[N/x]\] +projections + +\[(\pi_1)\;\;fst \pair{M}{N} \leadsto M\\ \hspace{.6cm} (\pi_2)\;\; snd \pair{M}{N} +\leadsto N \] +and the following type specific reductions: +\[(D_{true})\;\;\\D\;M\;N\; true \leadsto M \hspace{.6cm} + (D_{false})\;\; D\;M\;N\;false \leadsto N \] +\[(R_0)\;\;\\R\;M\;F\; 0 \leadsto M \hspace{.6cm} + (R_S)\;\; R\;M\;F\;(S\;n) \leadsto F\;n\;(R\;M\;F\;n) \] +\[(*)\;\; M \leadsto * \] +where (*) holds for any $M$ of type $\one$. + \section{Heyting's arithmetics} {\bf Axioms} @@ -142,7 +170,7 @@ say that ax:AX refers to the previous Axioms list... %\[ % (\land_i)\frac{\Gamma \vdash M:A \hspace{1cm}\Gamma \vdash N:B} -% {\Gamma \vdash : A \land B} +% {\Gamma \vdash \pair{M}{N} : A \land B} %\hspace{2cm} % (\land_{el})\frac{\Gamma \vdash A \land B}{\Gamma \vdash A} %\hspace{2cm} @@ -180,7 +208,7 @@ For any type T of system T $\bot_T: \one \to T$ is inductively defined as follo \begin{enumerate} \item $\bot_\one = \lambda x:\one.x$ \item $\bot_N = \lambda x:\one.0$ -\item $\bot_{U\times V} = \lambda x:\one.<\bot_{U} x,\bot_{V} x>$ +\item $\bot_{U\times V} = \lambda x:\one.\pair{\bot_{U} x}{\bot_{V} x}$ \item $\bot_{U\to V} = \lambda x:\one.\lambda \_:U. \bot_{V} x$ \end{enumerate} @@ -188,10 +216,10 @@ For any type T of system T $\bot_T: \one \to T$ is inductively defined as follo \item $\sem{nat\_ind} = R$ \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{ex\_intro} = \lambda x:\N.\lambda f:\sem{P}.\pair{x}{f}$ \item $\sem{fst} = \pi_1$ \item $\sem{snd} = \pi_2$ -\item $\sem{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.$ +\item $\sem{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.\pair{x}{y}$ \item $\sem{false\_ind} = \bot_{\sem{Q}}$ \item $\sem{discriminate} = \lambda \_:\N.\lambda \_:\one.\star$ \item $\sem{injS}= \lambda \_:\N. \lambda \_:\N.\lambda \_:\one.\star$ @@ -214,10 +242,10 @@ In particular: \begin{itemize} \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 $\pair{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 $ \R (\exists x.P)$ iff $g \R P[\underline{n}/x]$ +\item $\pair{n}{g}\R (\exists x.P)$ iff $g \R P[\underline{n}/x]$ \end{itemize} %We need to generalize the notion of realizability to sequents. %Given a sequent $B_1, \ldots, B_n \vdash A$ with free variables in @@ -261,7 +289,7 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$. \to Q) \to (\exists x:(P x)) \to Q$$ Following the definition of $\R$ we have to prove that given\\ $f~\R~\forall~x:((P~x)~\to~Q)$ and $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 + $p$ is a couple $\pair{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$ (note that $x$ is not free in $Q$ so $[\underline{n}/x]$ affects only $P$).\\ @@ -271,7 +299,7 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$. \item $ex\_intro$. We must prove that - $$\lambda x:\N.\lambda f:\sem{P}. \R \forall x.(P\to\exists x.P(x)$$ + $$\lambda x:\N.\lambda f:\sem{P}.\pair{x}{f} \R \forall x.(P\to\exists x.P(x)$$ that leads to prove that for each n $\underline{ex\_into}~n \R (P\to\exists x.P(x))[\underline{n}/x]$.\\ Evaluating the substitution we have @@ -279,12 +307,12 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$. Again by definition of $\R$ we have to prove that given a $m \R P[\underline{n}/x]$ then $\underline{ex\_into}~n~m \R \exists x.P(x)$. Expanding the definition of $\underline{ex\_intro}$ we have - $ \R \exists x.P(x)$ that is true since $m \R P[\underline{n}/x]$. + $\pair{n}{m} \R \exists x.P(x)$ that is true since $m \R P[\underline{n}/x]$. \item $fst$. We have 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$. + $m$ must be a couple $\pair{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$. @@ -292,11 +320,11 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$. \item $conj$. We have to prove that - $$\lambda x:\sem{P}. \lambda y:\sem{Q}. \R P \to Q \to P \land Q$$ + $$\lambda x:\sem{P}. \lambda y:\sem{Q}.\pair{x}{y}\R P \to Q \to P \land Q$$ Following the definition of $\R$ we have to show that for each $m \R P$ and for each $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 + $(\lambda x:\sem{P}. \lambda y:\sem{Q}.\pair{x}{y})~m~n \R P \land Q$.\\ + This is the same of $\pair{m}{n} \R P \land Q$ that is verified since $m \R P$ and $n \R Q$. -- 2.39.2