\documentclass{amsart}
\usepackage[latin2]{inputenc}
\usepackage[magyar]{babel}
\usepackage{amsthm}
\usepackage{amsmath}
\usepackage{amssymb}

\begin{document}
\begin{center}
\vspace {2cm}

{\bf \Large Extending nonstandard Heyting Arithmetic with
\\ Church's Thesis}

\vspace{0.5cm}

\bf{Abstract}

\end{center}
\vspace {0.5cm}

    Our investigations are concerned with nonstandard Heyting Arithmetic ($HA^{c}$), which is the usual
theory of arithmetic taking intuitionistic logic as background
extended with the axioms $\underline{n}<c$ for all natural numbers
$n$.

    As early as 1934 Skolem proved the existence of models of
nonstandard classical, that is Peano, arithmetic ($PA$).

Intuitionistic logic has a different flavour to classical logic,
for example- making use of the method of realizability devised by
Kleene- it can be shown that Heyting Arithmetic ($HA$) can be
extended with an axiom scheme expressing constructivity, which is
usually termed as Church's Thesis
\begin{center}
$(CT)$\hspace{1cm}$\forall x\exists yA(x,y)\supset \exists
e\forall x\exists y(T(e,x,y)\wedge A(x,Uy)),$
\end{center}
such that the resulting theory remains consistent just in case
$HA$ is consistent. It should be remarked that $PA$ is
inconsistent with $CT$.

The question raises naturally, whether $HA^{c}$ could be extended
with $CT$ preserving consistency relative to the original theory.
In our exposition it is proved with a slightly modified version of
the realizability method invented by Kleene that $HA^{c}+CT$ is
consistent at the same time, when $HA^{c}$ is.

Furthermore, a relative consistency result is obtained with
respect to a stronger version of $CT$- an axiom scheme denoted by
$ECT$. A formula is almost negative, if it does not contain
disjunction and existential quantification occurs in it in front
of atomic subformulas, only. $ECT$ is an implicative form of $CT$
with an almost negative formula in the antecedent:
\begin{center}
$(ECT)$\hspace{1cm}$\forall x(B(x)\supset \exists yA(x,y))\supset
\exists e\forall x(B(x)\supset \exists y(T(e,x,y)\wedge
A(x,Uy))),$
\end{center}
where $B$ is almost negative.

Our claim is that if $HA^{c}$ is consistent, then $HA^{c}+ECT$ is
also consistent.



\end{document}
