From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 10 Oct 2005 13:57:38 +0000 (+0000)
Subject: First draft.
X-Git-Tag: V_0_7_2_3~226
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=890385fa69623abbcfbfe758218c080b7c80903e;p=helm.git

First draft.
---

diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex
index c9bf726c8..30cbd5732 100644
--- a/helm/papers/system_T/t.tex
+++ b/helm/papers/system_T/t.tex
@@ -5,7 +5,7 @@
 %\usepackage{hyperref}
 %\usepackage{picins}
 
-
+\newcommand{\sem}[1]{[\![ #1 ]\!]}
 \title{...}
 \author{...}
 
@@ -17,10 +17,111 @@
 ...
 \end{abstract}
 
-\section{Introduction}
+\section{Heyting's arithmetics}
+
+{\bf Axioms}
+
+\begin{itemize}
+
+\item $nat\_ind: P(0) \to (\forall x.P(x) \to P(S(x))) \to \forall x.P(x)$ 
+\item $ex\_ind: (\forall x.P(x) \to Q) \to \exists x.P(x) \to Q$
+\item $ex\_intro: \forall x.(P \to \exists x.P)$
+\item $fst: P \land Q \to P$
+\item $snd: P \land Q \to Q$
+\item $conj: P \to Q \to P \land Q$
+\item $false\_ind: \bot \to Q$
+\item $discriminate:\forall x.0 = S(x) \to \bot$
+\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 $timies\_S:\forall x,y.x*S(y)=x+(x*y)$ 
+\end{itemize}
+
+\noindent
+{\bf Inference Rules}
+
+\[ 
+   (\to_i)\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q} \hspace{2cm}
+   (\to_e)\frac{\Gamma \vdash M: A \to Q \hspace{1cm}\Gamma \vdash N: A}
+    {\Gamma \vdash M N: Q} 
+\]
+
+%\[ 
+%   (\land_i)\frac{\Gamma \vdash M:A \hspace{1cm}\Gamma \vdash N:B}
+%   {\Gamma \vdash <M,N> : A \land B} 
+%\hspace{2cm}
+%   (\land_{el})\frac{\Gamma \vdash A \land B}{\Gamma \vdash A}
+%\hspace{2cm}
+%   (\land_{er})\frac{\Gamma \vdash A \land B}{\Gamma \vdash B}  
+%\]
+
+\[ 
+   (\forall_i)\frac{\Gamma \vdash M:P}{\Gamma \vdash 
+   \lambda x:N.M: \forall x.P}(*) \hspace{2cm}
+   (\forall_e)\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]} 
+\]
+
+
+%\[ 
+%   (\exists_i)\frac{\Gamma \vdash P[t/x]}{\Gamma \vdash \exists x.P}\hspace{2cm}
+%   (\exists_e)\frac{\Gamma \vdash \exists x.P\hspace{1cm}\Gamma \vdash \forall x.P \to Q}
+%{\Gamma \vdash Q} 
+%\]
+
+\section{Extraction}
+
+\begin{itemize}
+\item $\sem{A} = 1$ if A is atomic
+\item $\sem{A \land B} = \sem{A}\times \sem{B}$
+\item $\sem{A \to B} = \sem{A}\to \sem{B}$
+\item $\sem{\forall x.P} = N \to \sem{P}$
+\item $\sem{\exists x.P} = N \times \sem{P}$
+\end{itemize}
+
+definition.
+For any type T of system T $\bot_T: 1 \to T$  is inuctively defined as follows:
+\begin{enumerate}
+\item $\bot_1 = \lambda x:1.x$
+\item $\bot_N = \lambda x:1.0$
+\item $\bot_{U\times V} = \lambda x:1.<\bot_{U} x,\bot_{V} x>$
+\item $\bot_{U\to V} = \lambda x:1.\lambda \_:U. \bot_{V} x$
+\end{enumerate}
 
+\begin{itemize}
+\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{fst} = fst$
+\item $\sem{snd} = snd$
+\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.*$
+\end{itemize}
 
+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}
+\end{itemize}
 
+\section{Realizability}
+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]$
+\end{itemize}
 
 \begin{thebibliography}{}