\documentclass[a4paper]{article}
\pagestyle{headings}
%\usepackage{graphicx}
\usepackage{amssymb,amsmath,mathrsfs}
%\usepackage{hyperref}
%\usepackage{picins}

\newcommand{\sem}[1]{[\![ #1 ]\!]}
\newcommand{\R}{\;\mathscr{R}\;}
\newcommand{\N}{\,\mathbb{N}\,}
\newcommand{\NT}{\,\mathbb{N}\,}
\newcommand{\NH}{\,\mathbb{N}\,}
\title{...}
\author{...}


\begin{document}
\maketitle

\begin{abstract}
...
\end{abstract}

\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 $times\_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 natural number $n$ $(f n) \R P[\underline{n}/x]$
\item $<n,g> \R (\exists x.P)$ iff $g \R P[\underline{n}/x]$
\end{itemize}

\noindent
We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$.

\begin{itemize}
\item $nat\_ind$. 
  We must prove that the recursion schema $R$ realizes the induction principle.
  To this aim we must prove that for any $a$ and $f$ such that $a \R P(0)$ and
  $f \R \forall x.(P(x) \to P(S(x)))$, and any natural number $n$, $(R \,a \,f
  \,n) \R P(\underline{n})$.\\ 
  We proceed by induction on n.\\ 
  If $n=O$, $(R \,a \,f \,O) = a$ and by hypothesis $a \R P(0)$.\\ 
  Suppose by induction that
  $(R \,a \,f \,n) \R P(\underline{n})$, and let us prove that the relation
  still holds for $n+1$.  By definition 
  $(R \,a \,f \,(n+1)) = f \,n \,(R \,a \,f \,n)$, 
  and since $f \R \forall x.(P(x) \to P(S(x)))$,  
  $(f n (R a f n)) \R P(S(\underline{n}))=P(\underline{n+1})$.

\item $ex\_ind$. 
  We must prove that $$\underline{ex\_ind} \R (\forall x:(P x)
  \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
  $f$ is a function such that forall $n$ and for all $m \R P[\underline{n}/x]$
  then $f~n~m \R Q$.  Exapanding the definition of $\underline{ex\_ind}$, $fst$
  and $snd$ we obtain $f~n_p~g_p$ that we know is in relation $\R$ with $Q$
  since $g_p \R P[\underline{n_p}/x]$.

\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)$$
  that leads to prove that foreach n
  $\underline{ex\_into}~n \R (P\to\exists x.P(x))[\underline{n}/x]$.\\
  Evaluating the substitution we have 
  $\underline{ex\_into}~n \R (P[\underline{n}/x]\to\exists x.P(x))$.\\
  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]$.

\item $false\_ind$. 
  We have to prove that $\bot_{\sem{Q}} \R \bot \to Q$. 
  Trivial, since there is no $m \R \bot$.

\item $discriminate$. 
  Since there is no $n$ such that $0 = S n$ is true... \\
  $\underline{discriminate}~n \R 0 = S~\underline{n} \to \bot$ for each n.

\item $injS$.
  We have to prove that for each $n_1$ and $n_2$\\
  $\lambda \_:\N. \lambda \_:\N.\lambda \_:1.*~n_1~n_2 \R 
  (S(x)=S(y)\to x=y)[n_1/x][n_2/y]$.\\
  Assuming $m \R S(n_1)=S(n_2)$ we have to prove

  

\end{itemize}

\begin{thebibliography}{}


\end{thebibliography}

\end{document}

