+\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}