+\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
+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
+literature on the
+topic (see e.g. \cite{Howard68,Troelstra,Girard87}.
+
+A different, more neglected, but for many respects much more
+direct relation between Peano (or Heyting) Arithmetics and
+G\"odel System T is provided
+by the so called {\em modified realizability}. Modified realizability
+was first introduced by Kreisel in \cite{Kreisel59} - although it will take you
+a bit of effort to recognize it in the few lines of paragraph 3.52 -
+and later in \cite{Kreisel62} under the name of generalized realizability.
+The name of modified realizability seems to be due to Troelstra
+\cite{Troelstra}
+- who contested Kreisel's name but unfortunately failed in proposing
+a valid alternative; we shall reluctantly adopt this latter name
+to avoid further confusion. Modified realizability is a typed variant of
+realizability, essentially providing interpretations
+of $HA^{\omega}$ into itself: each theorem is realized by a typed function
+of system T, that also gives the actual computational content extracted
+from the proof.
+In spite of the simplicity and the elegance of the proof, it is extremely
+difficult to find a modern discussion of this result; the most recent
+exposition we are aware of is in the encyclopedic (typewritten!) work by
+Troelstra \cite{Troelstra} (pp.213-229). Even modern introductory books
+to Type Theory and Proof Theory devoting much space to system T
+such as \cite{GLT} and \cite{TS} surprisingly leave out this simple and
+illuminating result. Both \cite{GLT} and \cite{TS}
+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
+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
+$\forall X.(X\to X) \to X \to X$ of $\N$.
+Moreover, after a first period of enthusiasm, the impredicative
+encoding of inductive types in Logical Frameworks has shown several
+problems and limitations (see e.g. \cite{Werner} pp.24-25) mostly
+solved by assuming inductive types as a primitive logical notion
+(leading e.g. form the Calculus of Constructions to the Calculus
+of Inductive Constructions - CIC). Even the extraction algorithm of
+CIC, strictly based on realizability principles, and in a first time
+still oriented towards System F \cite{Paulin87,Paulin89} has been
+recently rewritten \cite{Letouzey04}
+to take advantage of concrete types and pattern matching of ML-like
+languages. Unfortunately, systems like the Calculus of Inductive
+Constructions are so complex, from the logical point of view, to
+substantially prevent a really neat theoretical exposition (at present,
+it does not
+even exists a truly complete consistency proofs covering all aspects
+of such systems); moreover, not eveybody may be interested in all the features
+offered by these frameworks, from polymorphism to types depending on
+proofs. Our program is to restart the analysis of logical systems with
+primitive inductive types in a smooth way, starting form first order
+logic and adding little by little small bits of logical power.
+This paper is the first step in this direction.
+
+
+
+
+
+
+
+