03-01-InterpretationOfIntuitionisticLogicByMeansOfFunctionals.tex

\documentclass[12pt]{article}
\usepackage{pmmeta}
\pmcanonicalname{InterpretationOfIntuitionisticLogicByMeansOfFunctionals}
\pmcreated{2013-03-22 18:32:35}
\pmmodified{2013-03-22 18:32:35}
\pmowner{gribskoff}{21395}
\pmmodifier{gribskoff}{21395}
\pmtitle{interpretation of intuitionistic logic by  means of functionals}
\pmrecord{7}{41262}
\pmprivacy{1}
\pmauthor{gribskoff}{21395}
\pmtype{Topic}
\pmcomment{trigger rebuild}
\pmclassification{msc}{03-01}
\pmclassification{msc}{03A05}
\pmclassification{msc}{03B20}
\pmsynonym{Brouwer's logic}{InterpretationOfIntuitionisticLogicByMeansOfFunctionals}
\pmsynonym{intuitionistic foundations}{InterpretationOfIntuitionisticLogicByMeansOfFunctionals}
%\pmkeywords{constructive proof}
%\pmkeywords{Evidenz}
%\pmkeywords{Heyting's formal system}
%\pmkeywords{functionals}
\pmrelated{IntuitionisticLogic}
\pmrelated{AnOutlineOfHilbertsProgramme}
\pmrelated{FOUNDATIONSOFMATHEMATICSOVERVIEW}
\pmrelated{Logicism}
\pmdefines{intuitionistic proof}
\pmdefines{functionals}

\endmetadata

\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amsmath}
\usepackage{graphicx}
%%\usepackage{xypic}
\usepackage{psfrag}
\usepackage{amsthm}
\usepackage[T1]{fontenc}
\usepackage{yfonts}

% define commands here
\begin{document}
\title{Interpretation of intuitionistic logic by  means of functionals}\Large 
\maketitle

\begin{abstract}
The entry reports on the analysis of the concept of constructivity and in particular G\"{o}del's own \emph{stricto sensu} constructivity. A structural description of a \emph{stricto sensu} constructive system is provided and the concept of a computable functional of finite type is used to formulate a new interpretation of the intuitionistic logical operators. This material is propaedeutic to an understanding of the so called \emph{Dialectica interpretation}. A new proof of the consistency of classical number theory is available. In spite of the provided continuity between the sections one can read most of them in isolation.
\end{abstract}

\tableofcontents

\section{Background}\normalsize

Strict Constructivism (or G\"{o}del's \emph{stricto sensu} constructivism) was the first stage of the interpretation of intuitionistic logic by means of functionals, the maturity of which was reached in 1958 with the \textbf{Dialectica} essay "Ãber eine bisher noch nicht benüzte Erweiterung des finiten Standpunktes". This first stage took the form of a lecture at Yale on intuitionistic logic, delivered on April 15, 1941.

It is also one of several occasions in which G\"{o}del labels the intuitionistic position as an extended nominal change of classical logic. But the Yale lecture shows with remarkable simplicity above all how much can be achieved by using the method of conceptual analysis.

It is obvious that the interest and the value of the insight gained in this analysis will not be recognized if one has \emph{previously} adopted the intuitionistic position. But to ask that G\"{o}del's insight into the basic concepts of intuitionistic logic be evaluated by a partisan intuitionist is perhaps as futile as to ask Lénin to evaluate the Sermon on the Mountain.

\section{Mathematical philosophy in intuitionistic systems}\normalsize

Whereas in intuitionistic mathematical philosophy two main patterns of deduction are rejected, the impredicative definition and the use of the \emph{tertium non datur}, in semi-intuitionism only the use of impredicative definition is rejected.

It would seem, at first sight, that of both deduction patterns, the rejection of the \emph{tertium non datur} would have a more radical impact, since it affects the underlying logic. 

But this impression can be corrected if one gives up the standard intuitionistic definition of disjunction. To achieve it one reformulates:

\begin{center} 
$X \vee Y$
\end{center} 

as

\begin{center}  
$\neg (\neg X \wedge \neg Y).$
\end{center}

Accordingly the \emph{tertium non datur}:

\begin{center} 
$X \vee \neg X$
\end{center}
 
becomes

\begin{center}
$\neg (\neg X \wedge \neg \neg X).$
\end{center}

This formula is an intuitionistically valid version of the law of contradiction.

The same process of reformulation can be applied to non constructive proofs of existential propositions, if one is ready to abandon the intuitionistic interpretation of the existential quantifier in favour of:

\begin{center} 
$\neg (\forall x) \neg F (x).$
\end{center}
 
By this reformulation a proof in classical logic becomes an intuitionistic correct proof, if one excludes the use of impredicative definitions.

\section{Proof that Heyting's system is not \emph{stricto sensu} constructive}\normalsize

In order to examine what is usually meant by saying that intuitionistic logic is constructive, we have to carry out a rigorous analysis of the concepts used in intuitionistic mathematical philosophy. When we do it we become first aware of the incongruence between, on one side, not allowing negation to be prefixed to universal statements and, on the other, allowing the use of the concept of "contradiction" without restrictions, although this concept logically entails the concept of negation. In particular, the analysis of the \emph{axioms} postulated as evident about contradiction shows that they allow operations everywhere equivalent to those of classical negation.
 
If we now turn to the analysis of the primitive concepts of intuitionistic logic we are told that they are to be formulated in terms of expressions like "\emph{constructive} proof (or rule)" or "intuitionistically correct proof". The paradigm cases in the literature are negation and implication.

The negation of $X$ is understood as the possibility of proving a contradiction starting with $X$ as a premiss. The implication of $Y$ by $X$ is understood as the possibility of proving $Y$ from a proof of $X$. But one should notice that in both examples, however, the concept of proof does not occur in its usual meaning, i.e., it does not denote a sequence of formulas in an explicit formal system. In both examples a proof is a mental act, an \emph{immediate object} of intuition.

One is therefore justified in raising the question as to what extent is the intuitionistic concept of "\emph{constructive} proof" itself constructive.

Using as measure the concept of \emph{stricto sensu constructivity} (yet to be defined) G\"{o}del proves that the concept of "\emph{constructive} proof", used in the above mentioned formulations of intuitionistic mathematical philosophy, is itself not constructive. 

\section{Analysis of the concept \emph{stricto sensu} constructivity}\normalsize

\begin{enumerate}

\item \textbf{Categorical clauses:}

To carry out this analysis we want first to specify a number of categorical clauses, i.e., clauses that an axiom system $\mathfrak{G}$ \emph{has} to satisfy in order to be considered \emph{stricto sensu} constructive.

The clauses are:

\textbf{SS1:} \emph{For all arguments, the decidability of all primitive relations and the computability of all functions of $\mathfrak{G}$.}

\textbf{SS2:} \emph{The exclusion of the concept of Existence from the class of all primitive concepts of $\mathfrak{G}$.}

\textbf{SS3:} \emph{The functions of the propositional calculus can not have arguments of the form} $(\forall \mathfrak{x}) \mathfrak{F} (\mathfrak{x}).$

\item \textbf{Theory of meaning:}

The theory of meaning associated with a \emph{stricto sensu} constructive system $\mathfrak{G}$ is characterized by the following propositions:

\begin{itemize}

\item \textbf{i)} The meaning of an expression of the form $(\exists \mathfrak{x}) \mathfrak{F} (\mathfrak{x})$ is to be analyzed in terms of what Hilbert and Bernays call a \emph{partial assertion} or an abbreviation of an effective construction.

\item \textbf{ii)} The only possible meaning of $\neg (\forall \mathfrak{x}) \mathfrak{F} (\mathfrak{x})$ is that of an assertion intending to imply the existence (in the sense of \emph{i)}) of a counter-example.

\item \textbf{iii)} The restriction \textbf{SS3} results from the fact that the functions of the propositional calculus are defined by means of truth-tables, a method that can not be applied to universal statements.

\item \textbf{iv)} The introduction of new symbols by a definition is allowed if it is a contextual definition, i.e., the \emph{definiendum}-term can be eliminated in every context.

Under these conditions the system of intuitionistic logic in Heyting 1930 is not \emph{stricto sensu} constructive, since existence is a primitive concept of the system and the functions of the propositional calculus are applied without restrictions.

\end{itemize}

\end{enumerate}

\section{Structural description of the \emph{stricto sensu} constructive system G}\normalsize

Structural description of the stricto sensu constructive system $\mathfrak{G}$.

The structural description of $\mathfrak{G}$ is the following:

\begin{enumerate}

\item The formulas of the system are in Prenex Normal Form, in particular in \emph{Skolem Normal Form},

\begin{center}
$(\exists \mathfrak{x}) (\forall \mathfrak{y}) \mathfrak{F} (\mathfrak{x}, \mathfrak{y})$
\end{center}

so that the atomic formulas after the prefix are quantifier-free.

\item The \emph{atomic formulas} are built out:

\begin{itemize}
\item \textbf{i)} Relations, like $=$, $<$, etc.
\item \textbf{ii)} Functions, like $+$, $\times$, etc.
\item \textbf{iii)} Constants, like $1$, $2$,etc
\item \textbf{iv)} Variables like $\mathfrak{x}$, $\mathfrak{y}$, etc.
\end{itemize}

\item The \emph{terms} of $\mathfrak{G}$ are the constants, the variables and the result of one or more applications of functions to constants resp. variables.

\item Every atomic formula is decidable.

\item The functions of the propositional calculus, in the sense of the truth-table method, are a subset of the computable functions and their arguments and values are the truth-values 0, 1 (resp. false, true).

If one or several of these computable functions are applied using a fixed order to arbitrary objects $\mathfrak{x, y, z}$, $\ldots$, the result is always 1, regardless of the identity of the objects $\mathfrak{x, y, z}$, $\ldots$ 

\item \emph{Axioms} and \emph{rules of inference}:

\begin{itemize}
\item \textbf{i)} All axioms from the two-valued propositional calculus applied to atomic formulas;

\item \textbf{ii)} Other axioms which depend on the identity of the primitive objects;

\item \textbf{iii)} \emph{Existential generalization}:

If $\mathfrak{F} (\mathfrak{t})$ is a well formed formula of the system in which $\mathfrak{F}$ has a constant term $\mathfrak{t}$, then we are allowed to infer $(\exists \mathfrak{x}) \mathfrak{F} (\mathfrak{x}).$

[N.B.: \textbf{6.iii)} is not a definition, in which the \emph{definiendum} is the existential proposition. It rather explains how a proposition with an occurrence of $(\exists \mathfrak{x}) \mathfrak{F} (\mathfrak{x})$ acts in a proof, i.e., from which formulas it can be inferred. It satisfies the following eliminability clause:

\begin{center}
if a proposition $P$ in which the existential statement does not occur becomes provable as

$P \cup (\exists \mathfrak{x}) \mathfrak{F} (\mathfrak{x})$ 

then it also provable as P.]
\end{center}
\end{itemize}
\end{enumerate}

\section{Three models for G}\normalsize

If we leave the structural characterization of $\mathfrak{G}$ and proceed to specify primitive objects, relations and primitive functions, we obtain a series of \emph{stricto sensu} constructive models for $\mathfrak{G}$.

\begin{enumerate}
\item The first that suggests itself is \textbf{recursive number theory}:

\begin{itemize}  
\item \textbf{i)} \emph{Primitive objects}:  are the elements of $\mathbb{N}$;

\item \textbf{ii)} \emph{Relations} and \emph{functions}: are defined by recursion or by complete induction. 
\end{itemize}

\item Since at this level one can not prove the consistency of classical number theory, \textbf{Gentzen} proposed the following extension:

We substitute the usual (increasing) well-ordering of the integers by another well ordering $R^*$, in which one allows the recursive definition of a function $f (n)$ over $\mathbb{N}$ in terms of $f (\pi (n))$, in which $\pi (n)$ denotes the predecessor of $n$ in the well ordering. By definition of $R^*$ every subset has a $R^*$-first-element and therefore $f (n)$ is computable in a finite number of steps.

In terms of \emph{stricto sensu} constructivity this approach is not very attractive since in order to show that $R^*$ is a well ordering we may eventually have to fall back on set theoretical arguments.

\item \textbf{Computable functionals of finite type}.

The next approach is due to G\"odel and it mainly consists in an \emph{extension of the underlying ontology}, in the sense that other than the integers and functions of integers one introduces functions of functions of integers. Such functions, in the literature called functionals, are functions whose arguments and values are functions, i.efunctions 

\begin{center}
$F: \mathbb{N}^{\mathbb{N}} \to \mathbb{N}^{\mathbb{N}}.$ 
\end{center}

Thus if $f$ and $h$ are functions and $n \in \mathbb{N}$, a functional $F$ is a function:

\begin{center}
$F (f) = h$
\end{center}

defined as being the function $h$ whose value for an argument $x \in \mathbb{N}$ is computed by reiterating the computation of the function $f$. Therefore:

\begin{center}
$h (\mathfrak{x}) = f^n, \ldots, f^2 \circ f (\mathfrak{x})$
\end{center}

so that

\begin{center} 
$F (f) (\mathfrak{x}) = f^n, \ldots, f^2 \circ f (\mathfrak{x}).$
\end{center}

If $n = 2$ for example one then says that the functional $F$ squares $f$ and that $F$ is a function of the second type.
The functionals of 3. have to satisfy \textbf{SS1} and the types that they give rise to have to be in turn finite. Both features are captured in the expression \emph{computable functional of finite type}, the name by which G\"odel's proposal became to be known.

\end{enumerate}

\section{Definition schemata and axioms for G}\normalsize

Along with the introduction of functionals two rules from recursive number theory can be adapted:

\begin{enumerate}
\item \textbf{Explicit definition:}
 
A functional $F$ can be defined by the clause:

\begin{center}
$F (\mathfrak{x}_1), \ldots, (\mathfrak{x}_n)$
\end{center}

meaning that $F$ acts on $\mathfrak{x}_1$, the resulting \emph{function} acts on $\mathfrak{x}_2$, and in the end we have a term $\mathfrak{T}$, built out of the variables and the previously defined functions.

\item \textbf{Recursive definition:}

A function:

\begin{center}
$F : \mathbb{Z} \to \mathbb{N}^{\mathbb{N}}$
\end{center}

whose arguments are integers and whose values can be functions of any type can be defined by the equations:

\begin{center}
$\mathfrak{F} (0) = \mathfrak{T}_1$

$\mathfrak{F} (\mathfrak{x} + 1) = \mathfrak{T}_2 (\mathfrak{x}, \mathfrak{F} (\mathfrak{x})).$
\end{center}

\end{enumerate}

[N.B.:

As it was said above the ontology or the domain of objects has been expanded with the introduction of the computable functionals, like $\mathfrak{F}$ above. This entails that we have a \emph{new primitive operation not mentioned in section 5}, namely the application of a functional to an object of the appropriate type. Since it belongs to the meaning of the concept of computable functional that the computation can be always carried out, it follows that a term, which results from the application of a functional to an object of the appropriate type, is itself also computable.]

With both schemata and functions of any type the axioms for $\mathfrak{G}$ are the following:

\begin{itemize}
\item The axioms of the propositional calculus (provided \textbf{SS1} is satisfied).

\item Complete Induction.

\item Substituion I (Leibniz Law): rules the substitution \emph{salva veritate} of equal terms.

\item Substituion II (\emph{dictum de omni}): rules of insertion of objects in $(\forall \mathfrak{x}) \mathfrak{A} (\mathfrak{x}).$

\item Existential generalization, as described above.

Under these circumstances a proposition of $\mathfrak{G}$ is an assertion in prenex normal form according to which there are objects $\mathfrak{f}_i$ (of specified types) such that for all objects $\mathfrak{g}_i$ (of specified types) $F (\mathfrak{f}_i, \mathfrak{g}_i)$ is true, in other words:

\begin{center}
$(\exists \mathfrak{f}_i) (\forall \mathfrak{g}_i) \mathfrak{F} (\mathfrak{f}_i, \mathfrak{g}_i).$ 
\end{center}

\end{itemize}

\section{The functional interpretation of the propositional calculus}\normalsize

We return now to the point raised at the end of section 3 about the interpretation of the intuitionistic logic, and begin with the propositional calculus.

Assuming \textbf{SS1} the interpretation procedure aims at showing the following:

\begin{itemize}
\item \textbf{i)} That the \emph{meaning} of the operations of the propositional calculus can be captured in $\mathfrak{G}$ in such a way that the arguments and the values are propositions of $\mathfrak{G}$;

\item \textbf{ii)} That the axioms and the rules of intuitionistic logic are provable in $\mathfrak{G}$ as theorems.
\end{itemize}

We consider propositions with double quantification in Skolem Normal Form.

\begin{enumerate}
\item \textbf{Negation:}

We reduce the problem of the negation of $\mathfrak{A}$, expressed by $\neg \mathfrak{A}$, to the problem of the interpretation of implication, since we can define $\neg \mathfrak{A}$ by:

\begin{center}
$\neg \mathfrak{A} = [\mathfrak{A} \rightarrow (0 = 1)].$
\end{center}

\item \textbf{Implication:}

Let 

\begin{center}
$\mathfrak{A} = (\exists \mathfrak{x}) (\forall \mathfrak{y}) \mathfrak{R} (\mathfrak{x}, \mathfrak{y})$
\end{center}

and 

\begin{center}
$\mathfrak{B} = (\exists \mathfrak{m}) (\forall \mathfrak{n}) \mathfrak{S} (\mathfrak{m}, \mathfrak{n})$
\end{center}

If both formulas are well formed formulas of $\mathfrak{G}$ then our problem consists in finding an expression of $\mathfrak{G}$ which captures the meaning of the implication:

\begin{center} 
$(\Phi)$ \qquad \qquad $(\exists \mathfrak{x}) (\forall \mathfrak{y}) \mathfrak{R} (\mathfrak{x}, \mathfrak{y}) \rightarrow (\exists \mathfrak{m}) (\forall \mathfrak{n}) \mathfrak{S} (\mathfrak{m}, \mathfrak{n}).$
\end{center}

By sections 7 and 5 we have to find an expression of the pattern:

\begin{center}
$(\exists \mathfrak{f}_i) (\forall \mathfrak{g}_i) \mathfrak{F} (\mathfrak{f}_i, \mathfrak{g}_i)$
\end{center}

which is intensionally equivalent to the implication $(\Phi)$.
 
The analysis of the meaning of $(\Phi)$ shows that in the assertion of $(\Phi)$ the intended meaning is to formulate a condition according to which:

\begin{center}
\emph{If there is an example $x$ which satisfies a relation $R$,}

\emph{then there is also an example $m$ which satisfies a relation $S.$}
\end{center}

Now by section 4.i) the meaning of this condition is that we have a function $f$ which taking $x$ as argument allows the calculation of $m$, so that the intensional content of our implication is better expressed by a formula like:

\begin{center}
$(\Phi \Phi)$ \qquad \qquad $(\exists f) (\forall x) [(\forall y) R (x, y) \rightarrow (\forall n) S (f (x), n)].$
\end{center}

But by section 5.ii) the formula in square brackets is not a well formed formula of $\mathfrak{G}$. However if we analyze the meaning of this new implication:

\begin{center}
$(\Upsilon)$ \qquad \qquad $(\forall y) R (x, y) \rightarrow (\forall n) S [f (x), n)]$
\end{center}

we realize that a refutation of the implicatum by means of a counter-example allows the computation of a counter-example to refute the implicans.

And so if $g$ is the formula by means of which we compute the counter-example for $S$, then the meaning of the implication $(\Upsilon)$ can be expressed by:

\begin{center} 
$(\exists g) (\forall n) [\neg S (f (x), n) \rightarrow \neg R (x, g (n))].$
\end{center}

Since the formula inside the square brackets is quantifier-free, the implication is now a truth-function. This allows full use of contrapostion and double negation and we get the well formed formula of $\mathfrak{G}$:

\begin{center} 
$(\Upsilon \Upsilon)$ \qquad \qquad $(\exists \mathfrak{g}) (\forall \mathfrak{n}) [\mathfrak{R} (\mathfrak{x}, \mathfrak{g} (\mathfrak{n})) \rightarrow \mathfrak{S} (\mathfrak{f} (\mathfrak{x}), \mathfrak{n})]$
\end{center} 

If we join $(\Phi \Phi)$ with $(\Upsilon \Upsilon)$ we get the new formula:

\begin{center}
$(\exists \mathfrak{f}) (\forall \mathfrak{x}) (\exists \mathfrak{g}) (\forall \mathfrak{n}) [\mathfrak{R} (\mathfrak{x}, \mathfrak{g} (\mathfrak{n})) \rightarrow \mathfrak{S} (\mathfrak{f} (\mathfrak{x}), \mathfrak{n})].$
\end{center}

Since $n$ depends on $x$, $g$ is representable as $g (x, n)$ and the formula in $\mathfrak{G}$ is finally:

\begin{center}
$(\exists \mathfrak{f}) (\exists \mathfrak{g}) (\forall \mathfrak{x}) (\forall \mathfrak{n}) [\mathfrak{R} (\mathfrak{x}, \mathfrak{g} (\mathfrak{x}, \mathfrak{n})) \rightarrow \mathfrak{S} (\mathfrak{f} (\mathfrak{x}), \mathfrak{n})].$
\end{center}

N.B.: It important to notice that the type of the functional variables is higher relative to the type of the initial expressions, since the arguments and the values in $\mathfrak{f} (\mathfrak{x})$ and in $\mathfrak{g} (\mathfrak{x}, \mathfrak{n})$ have the type of the variables in $\mathfrak{R} (\mathfrak{x}, \mathfrak{n})$ and $\mathfrak{S} (\mathfrak{m}, \mathfrak{n})$. Therefore $\mathfrak{f}$ and $\mathfrak{g}$ have a higher type. 

\item \textbf{Conjunction:}

The interpretation of conjunction consists in bringing together the expressions $\mathfrak{R}$ and $\mathfrak{S}$ with the quantifiers in Skolem normal form. One then has:

\begin{center}
$(\exists \mathfrak{x}) (\exists \mathfrak{m}) (\forall \mathfrak{y}) [\mathfrak{R} (\mathfrak{x}, \mathfrak{y}) \wedge \mathfrak{S} (\mathfrak{m}, \mathfrak{n})].$
\end{center}

\item \textbf{Disjunction:}

In 1941 G\"odel thought that the same could be done for disjunction but in 1958 he restricted this possibility to the case in which the atomic formulas are quantifier-free. Otherwise if $\mathfrak{t}$ is a term type 0 one has:

\begin{center}
$(\exists \mathfrak{x}) (\exists \mathfrak{m}) (\exists \mathfrak{t}) (\forall \mathfrak{y}) (\forall \mathfrak{n}) {[ \mathfrak{t} = 0 \wedge \mathfrak{R} (\mathfrak{x}, \mathfrak{y})] \vee [ \mathfrak{t} = 1 \wedge \mathfrak{S} (\mathfrak{m}, \mathfrak{n})]}.$
\end{center}

\end{enumerate}

\section{Existence and generality}\normalsize

To interpret the quantifiers we can begin by considering an expression:

\begin{center} 
$(\exists \mathfrak{x}) (\forall \mathfrak{y}) \mathfrak{R} (\mathfrak{k}, \mathfrak{x}, \mathfrak{y})$
\end{center}

with a free accurrence of a constant $\mathfrak{k}$.

\begin{itemize}
\item \textbf{i)} To prefix the existential quantifier to $\mathfrak{R}$ results again in an expression of $\mathfrak{G}$,

\begin{center}
$(\exists \mathfrak{w}) (\exists \mathfrak{x}) (\forall \mathfrak{y}) \mathfrak{R} (\mathfrak{w}, \mathfrak{x}, \mathfrak{y}).$
\end{center}

\item \textbf{ii)} We can not apply the same treatment directly to the universal quantifier.
\end{itemize}

Assuming again that we have an expression:

\begin{center}
$(\exists \mathfrak{x}) (\forall \mathfrak{y}) \mathfrak{R} (\mathfrak{k}, \mathfrak{x}, \mathfrak{y}),$
\end{center}

prefixing the universal quantifier would produce the formula:

\begin{center}
$(\ast) \qquad \qquad (\forall \mathfrak{w}) (\exists \mathfrak{x}) (\forall \mathfrak{y}) \mathfrak{R} (\mathfrak{w}, \mathfrak{x}, \mathfrak{y})$
\end{center}

which is not in Skolem normal form.

However, as we have seen above, the meaning of a formula:

\begin{center}
$(\forall x) (\exists y) F (x, y)$
\end{center}

is intuitionistically better expressed by an assertion of the form:

\begin{center}
$(\exists f) (\forall x) F (x, f (x)).$
\end{center}

Thus our formula $(\ast)$ has the reformulation:

\begin{center}
$(\exists \mathfrak{f}) (\forall \mathfrak{w}) (\forall \mathfrak{y}) \mathfrak{R} (\mathfrak{w}, \mathfrak{f} (\mathfrak{w}), \mathfrak{y}),$
\end{center}

which is a formula of $\mathfrak{G}$ and is in Skolem normal form. 

\section{Axioms and \emph{modus ponens}}\normalsize

Two examples show how to formulate in $\mathfrak{G}$ a well known axiom and of the Rule of \emph{modus ponens}.

\begin{enumerate}

\item \textbf{Reflexivity of implication}

Our hypothesis are:

\begin{itemize}
\item \textbf{i)} That $\mathfrak{A}$ is a well formed formula of $\mathfrak{G}$ and

\item \textbf{ii)} That an implication $\mathfrak{A} \rightarrow \mathfrak{B}$ is defined as in section 8 by:

\begin{center}
$(\exists \mathfrak{f}) (\exists \mathfrak{g}) (\forall \mathfrak{x}) (\forall \mathfrak{n}) [\mathfrak{R} (\mathfrak{x}, \mathfrak{g} (\mathfrak{x}, \mathfrak{n})) \rightarrow \mathfrak{S} (\mathfrak{f} (\mathfrak{x}), \mathfrak{n})].$
\end{center}

\end{itemize}

To prove $\mathfrak{A} \rightarrow \mathfrak{A}$ as a theorem of $\mathfrak{G}$ we notice that $\mathfrak{A} = \mathfrak{B}$ implies $\mathfrak{R} = \mathfrak{S}.$

Since the functions $\mathfrak{f}$ and $\mathfrak{g}$ are computable by section 7.1 their values are accordingly:

\begin{center}
$\mathfrak{f} (\mathfrak{x}) = \mathfrak{x} \text{and} \mathfrak{g} (\mathfrak{x}, \mathfrak{n}) = \mathfrak{n}$
\end{center}

so that the antecedent equals the consequent.

\item \textbf{Modus ponens}

The hypothesis are:

\begin{itemize}
\item \textbf{i)} $\mathfrak{G} \vdash (\exists \mathfrak{g}) (\forall \mathfrak{x}) (\forall \mathfrak{n}) \mathfrak{R} (\mathfrak{x}, \mathfrak{g} (\mathfrak{x}, \mathfrak{n})$

\item \textbf{ii)} $\mathfrak{G} \vdash (\exists \mathfrak{f}) (\exists \mathfrak{g}) (\forall \mathfrak{x}) (\forall \mathfrak{y}) [\mathfrak{R} (\mathfrak{x}, \mathfrak{g} (\mathfrak{x}, \mathfrak{n}) \rightarrow \mathfrak{S} (\mathfrak{f} (\mathfrak{x}), \mathfrak{n})]$ 

and we want to infer:

\begin{center}
$(\exists \mathfrak{m}) (\forall \mathfrak{n}) \mathfrak{S} (\mathfrak{m}, \mathfrak{n}).$
\end{center}

\begin{itemize}
\item \textbf{1.} By the discussion of quantification and the introduction of functional symbols we can define an object $\mathfrak{k}$ such that:

\begin{center}
$(\diamond) \qquad \qquad (\forall \mathfrak{y}) \mathfrak{R} (\mathfrak{k}, \mathfrak{y})$
\end{center}

and define functions such that:

\begin{center}
$(\diamond \diamond) \qquad \qquad (\forall \mathfrak{x}) (\forall \mathfrak{n}) [\mathfrak{R} (\mathfrak{x}, \mathfrak{f}_2 (\mathfrak{x}, \mathfrak{n})) \rightarrow \mathfrak{S} (\mathfrak{f}_1 (\mathfrak{x}), \mathfrak{n})].$
\end{center}

\item \textbf{2.} By \emph{dictum de omni} over $(\diamond \diamond)$ we have:

\begin{center}
$(\forall \mathfrak{n}) [\mathfrak{R} (\mathfrak{k}, \mathfrak{f}_2 (\mathfrak{k}, \mathfrak{n})) \rightarrow \mathfrak{S} (\mathfrak{f}_1 (\mathfrak{k}), \mathfrak{n})].$
\end{center}

\item \textbf{3.} Now we insert in $(\diamond)$ $\mathfrak{f}_2 (\mathfrak{k}, \mathfrak{n})$ for $\mathfrak{y}$ and get:

\begin{center}
$(\forall \mathfrak{n}) [\mathfrak{R} (\mathfrak{k}, \mathfrak{f}_2 (\mathfrak{k}, \mathfrak{n}))].$
\end{center}

\item \textbf{4.} Steps 2, 3 and two-valued \emph{modus ponens} gives:

\begin{center}
$(\forall \mathfrak{n}) \mathfrak{S} (\mathfrak{f}_1 (\mathfrak{k}), \mathfrak{n}).$
\end{center}

\item \textbf{5.} Existential Generalization on 4. leads to

\begin{center}
$(\exists \mathfrak{m}) (\forall \mathfrak{n}) \mathfrak{S} (\mathfrak{m}, \mathfrak{n}).$
\end{center}
\end{itemize}

\end{itemize}

\end{enumerate}

\section{The consistency of classical number theory}\normalsize

If $E$ is a complex expression composed by formulas of $\mathfrak{G}$ by means of the already defined logical operations, then the \emph{meaning} of $E$ is to be identified with a formula $\mathfrak{E}$ of $\mathfrak{G}$ so that if $E$ is intuitionistically provable then $\mathfrak{E}$ has a proof in $\mathfrak{G}$. \emph{We can then say that the intuitionistic proof of E is stricto sensu constructive.}

In particular if one has an intuitionistic proof of an existential statement $(\exists x) F (x)$ then the corresponding formula of $\mathfrak{G}$, $(\exists \mathfrak{x}) \mathfrak{F} (\mathfrak{x})$ is a theorem of $\mathfrak{G}$. As it was discussed above, the interpretation of existence in $\mathfrak{G}$ allows that from a proof of $(\exists \mathfrak{x}) \mathfrak{F} (\mathfrak{x})$ we can find an explicit term $\mathfrak{k}$ such that $\mathfrak{F} (\mathfrak{k})$. This means that \emph{via functional interpretation} the intuitionistic proof gives the term.

As we have seen, apart from the use of impredicative definitions, classical logic is included in intuitionistic logic and since there is no use of impredicative definitions in classical number theory, the consistency of this theory can be reduced to that of $\mathfrak{G}$. By the argument in section 2, if disjunction and existential quantification are eliminated, every classically correct proof is also intuitionistically correct.

Under these circumstances a contradiction obtained by means of a classical argument would then imply a contradiction in the intuitionistic system and in turn the inconsistency of $\mathfrak{G}$.

Finally if we have a classical proof of $(\exists x) F (x)$ in which $F$ is quantifier-free, then we have an intuitionistic proof of $\neg \neg (\exists x) F (x)$. But by section 4 an intuitionistic existence proof gives in $\mathfrak{G}$ a corresponding construction and we will then have in $\mathfrak{G}$ a variant of Markov's rule.

\section{Complementary material}\normalsize

See \PMlinkname{"the inclusion of classical into intuitionistic logic"}{InclusionOfClassicalIntoIntuitionisticLogic}. See also parent entry \PMlinkname{"intuitionistic logic"}{IntuitionisticLogic}.

\begin{thebibliography} {99}
\bibitem{LEB1} Brouwer, L., \emph{Collected works: vol. 1}, North Holland, Amsterdam, 1975.
\bibitem{LEB2} Brouwer, L., "Mathematik, Wissenschaft und Sprache", \emph{Monatshefte für Mathematik und Physik}, Leipzig, 1929.
\bibitem{LEB3} Brouwer, L., "Consciousness, philosophy and mathematics", ed. W. Beth, \emph{Library of the tenth international congress of philosophy}, Amsterdam, 1948.
\bibitem{MD} Dummett, M., \emph{Elements of intuitionism}, Clarendon Press, Oxford, 1977.
\bibitem{KG} G\"{o}del, K., \emph{Collected works}, ed. S. Feferman, Oxford, 1987-2003.
\bibitem{AH} Heyting, A. \emph{Intuitionism: An introduction}, 3. ed., North-Holland, Amsterdam, 1971.
\bibitem{DHPB} Hilbert, D., and, Ackermann, \emph{Grundzüge der theoretischen Logik}, Berlin, 1949.
\bibitem{SK} Kleene, S., \emph{Introduction to metamathematics}, North-Holland, Amsterdam, 1964.
\bibitem{RS} Rasiowa, H., and, Sikorski, R., \emph{The mathematics of metamathematics}, Warsaw, 1963.
\bibitem{AT} Tarski, A., "Der Aussagenkalkül und die Topologie", \emph{Fundamenta Mathematicae}, 31, 1938.
\end{thebibliography}

\end{document}
%%%%%
%%%%%
\end{document}