\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}}}
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}
%\[
% (\land_i)\frac{\Gamma \vdash M:A \hspace{1cm}\Gamma \vdash N:B}
-% {\Gamma \vdash <M,N> : 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}
\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}
\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}.<x,f>$
+\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}.<x,y>$
+\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$
\begin{itemize}
\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 $\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 $<n,g> \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
\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 $<n_p,g_p>$ 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$).\\
\item $ex\_intro$.
We must prove that
- $$\lambda x:\N.\lambda f:\sem{P}.<x,f> \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
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
- $<n,m> \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 $<f_m,g_m>$ 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$.
\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$$
+ $$\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}.<x,y>)~m~n \R P \land Q$.\\
- This is the same of $<m,n> \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$.
projects / helm.git / commitdiff