Basic facts about group morphisms.

[helm.git] / helm / papers / system_T / t.tex

diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex
index 42b937bf2a1e9223f4386cdd267dbf86457aabcc..20ec951492223efb55f63fa2aec8ddf9eb2329ee 100644 (file)
--- a/helm/papers/system_T/t.tex
+++ b/helm/papers/system_T/t.tex
@@ -43,7 +43,19 @@
 \thispagestyle{empty}
 
 \begin{abstract}
-...
+In 1959, Kreisel introduced a notion of ``modified'' realizability to
+provide an alternative technique to G\"odel functional (dialectica)
+interpretation for establishing the connection between Peano Arihtmetic
+and System T. While the dialectica interpretation has been widely
+studied in the literature, Kreisel's technique, although remarkably 
+simpler,has apparently been almost neglected (with the only exception
+of Troelstra). In this paper we give a modern presentation of the technique, 
+and generalize it to arbitrary inductive types in a first order setting.
+This is part of a larger program, advocating the study 
+of logical systems with primitive inductive types starting form
+weak, predicative logical frameworks and adding little by little small 
+bits of logical power.
+
 \end{abstract}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -179,23 +191,24 @@ informative part of the algorithms.
 {\bf Inference Rules}
 
 say that ax:AX refers to the previous Axioms list...
-\begin{table}[!h]
-\hrule\vspace{0.1cm}
-\begin{tabular}{p{0.34\textwidth}r}
-  $\Gamma, x:A, \Delta \vdash x:A$ & $(Proj)$\\
-  $\Gamma \vdash ax : AX$ & $(Const)$\\
-  $\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q}$ & 
-    $(\to_i)$\\
-  $\frac{\Gamma \vdash M: A \to Q \hspace{0.5cm}\Gamma \vdash N: A}
-        {\Gamma \vdash M N: Q}$ & $(\to_e)$\\
-  $\frac{\Gamma \vdash M:P}{\Gamma \vdash \lambda x:\N.M: \forall x.P}(*)$ &
-    $(\forall_i)$\\
-  $\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]}$ &
-    $(\forall_e)$
-\end{tabular}\vspace{0.1cm}
-\hrule
-\caption{\label{tab:HArules}Inference rules}
-\end{table}{lr}
+%\begin{table}[!h]
+%\hrule\vspace{0.1cm}
+%\begin{tabular}{p{0.34\textwidth}r}
+
+  $$\Gamma, x:A, \Delta \vdash x:A ~~~ (Proj)$$
+  $$ \Gamma \vdash ax : AX~~~ (Const)$$
+  $$\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q} ~~~ (\to_i)$$
+  $$\frac{\Gamma \vdash M: A \to Q \hspace{0.5cm}\Gamma \vdash N: A}
+        {\Gamma \vdash M N: Q} ~~~ (\to_e)$$
+  $$\frac{\Gamma \vdash M:P}{\Gamma \vdash \lambda x:\N.M: \forall x.P}(*) ~~~
+    (\forall_i)$$
+  $$\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]}
+     ~~~ (\forall_e)$$
+    
+%\end{tabular}\vspace{0.1cm}
+%\hrule
+%\caption{\label{tab:HArules}Inference rules}
+%\end{table}{lr}
 
 %\[ 
 %   (\land_i)\frac{\Gamma \vdash M:A \hspace{1cm}\Gamma \vdash N:B}