From: Andrea Asperti Date: Tue, 8 Nov 2005 10:43:36 +0000 (+0000) Subject: Typos. X-Git-Tag: V_0_7_2_3~105 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e0da1fa24baa53163808f2be1b523c548949ce30;p=helm.git Typos. --- diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex index 9a1f4ec25..a65402911 100644 --- a/helm/papers/system_T/t.tex +++ b/helm/papers/system_T/t.tex @@ -28,7 +28,7 @@ \section{Introduction} The characterization of the provable recursive functions of Peano Arithmetic as the terms of system T is a well known -result of G\"odel \cite{Godel58,Godel90}. Although many authors acknowledge +result of G\"odel \cite{Godel58,Godel90}. Although several authors acknowledge that the functional interpretation of the Dialectica paper is not among the major achievements of the author (see e.g. \cite{Girard87}), the result has been extensively investigated and there is a wide @@ -62,7 +62,7 @@ prefer to focus on higher order arithmetics and its relation with Girard's System $F$ \cite{Girard86}, but the technical complexity and the didactical value of the two proofs is not comparable: when you prove that the Induction Principle is realized by the recursor $R$ -of system $T$ you catch a sudden gleam of intelligence in the +of system $T$ you catch a sudden gleam of understanding in the students eyes; usually, the same does not happen when you show, say, that the ``forgetful'' intrepretation of the higher order predicate defining the natural numbers is the system $F$ encoding