\documentclass{article}
%\renewcommand{\baselinestretch}{2}
\usepackage{amsthm}
\newtheorem{definition}{Definition}
\newtheorem{theorem}{Metatheorem}
\theoremstyle{remark}
\newtheorem{remark}{Remark}

\begin{document}
\title{Platonism in classical logic versus formalism in the
proposed non-Aristotelian finitary logic}
\author{Radhakrishnan Srinivasan\thanks{R \& D Group -- Exports services,
IBM Global Services India Pvt.\ Ltd., 5th floor, Golden Enclave,
Airport road, Bangalore~560017, India.
E-Mail:~\texttt{sradhakr@in.ibm.com}}}
\date{}
\maketitle

\begin{abstract}
The main thesis of this paper is that Platonism is inherent in classical
infinitary reasoning and that strict formalism inevitably
leads one to the author's non-Aristotelian finitary logic (NAFL)
proposed in the Philsci preprint ID Code~635. This claim
is established by an elementary analysis of Peano Arithmetic and its
weak fragments (especially Successor Arithmetic). Hence it is argued
that Hilbert's program is decisively settled negatively --
classical infinitary reasoning stands refuted
from the finitary and formalistic standpoints. The philosophical
basis for NAFL is discussed thoroughly and motivated via consideration
of several examples, including the Schr\"odinger cat and four-mirror
experiments of quantum mechanics. Particular attention is paid to
the delicate interplay between syntax and semantics in NAFL, and the
differences in this regard between NAFL and
classical/intuitionistic/constructive logics. The meaning of `existence'
of mathematical objects and the concept of negation
in NAFL are discussed. NAFL also
correctly handles time-dependent truth values for propositions involving
future contingencies; this is illustrated with examples, such as,
Aristotle's `There will be a sea battle tomorrow'.
That NAFL justifies quantum superposition on
the one hand, while emphatically rejecting much of classical infinitary
reasoning and the continuum-based relativity theories
(see also the PhilSci preprint ID Code~666) on the other, means that the
incompatibility between quantum mechanics and the theory of
relativity is clearly established in NAFL. Another important implication
for quantum mechanics is that NAFL requires the concept of `measurement'
to be confined to the metatheory, i.e., it is not formalizable.
\end{abstract}

\section{Platonism in classical first-order predicate logic}\label{sec1}
We begin by quoting Stephen Simpson\cite{SGS} on the current status
of the philosophy of mathematics:
\begin{quote}
We have mentioned three competing 20th century doctrines: formalism,
constructivism, set-theoretical Platonism. None of these doctrines
are philosophically satisfactory, and they do not provide much guidance
for mathematically oriented scientists and other users of mathematics.
As a result, late 20th century mathematicians have developed a split
view, a kind of Kantian schizophrenia, which is usually described as
``Platonism on weekdays, formalism on weekends''. In other words,
they accept the existence of infinite sets as a working hypothesis
in their mathematical research, but when it comes to philosophical
speculation, they retreat to a formalist stance. Thus they have given
up hope of an integrated view which accounts for both mathematical
knowledge and the applicability of mathematics to physical reality.
In this respect, the philosophy of mathematics is in a sorry state.
\end{quote}
In this section, we demonstrate that the ``retreat to a formalist
stance'' in the above quote is not really a viable option in
classical first-order predicate logic with equality~(FOPL);
i.e., Platonism is inherent in classical infinitary reasoning.

The existence of nonstandard models of Peano Arithmetic~(PA)
in FOPL follows from any one of the completeness, compactness and
incompleteness theorems due to G\"odel~\cite{Gd} in 1930 and 1931;
Skolem~\cite{Sk} first demonstrated the existence of these
nonstandard models in the 1930's. The proofs of the
(in)completeness and compactness theorems may
be formalized in a theory~T of intermediate strength between
PA and Zermelo-Fraenkel set theory with axiom of choice~(ZFC).
The proof of the existence of nonstandard integers therefore tacitly assumes
the consistency of T; for if T were inconsistent, the (in)completeness
and compactness theorems would carry no conviction from the formalistic
standpoint, since proof is the ultimate criterion for formalists.
The consistency of T in turn requires nonstandard models of T to exist,
by G\"odel's incompleteness theorems, and so tacitly presumes the
existence of nonstandard integers. It is clear that from a formalistic
standpoint, one does not have a convincing non-circular
proof of either the existence of
nonstandard integers or of the consistency of PA. In what follows, we
demonstrate that a strict interpretation of formalism requires one
to \emph{deny} the existence of nonstandard integers, and hence to deny
the consistency of PA and the validity of the proofs of the
(in)completeness and compactness theorems. This would leave Platonism
as the only viable philosophy for classical infinitary reasoning.
In Section~\ref{sec2}, we demonstrate that the non-Aristotelian
finitary logic (NAFL) developed by the author~\cite{SR} is the
appropriate logic which embodies formalism.

\subsection{Definition of formalism}
Traditionally, formalism has been defined as the formal manipulation
of symbols according to certain well-defined rules. Thus mathematics
consists solely of syntax; semantics will be acceptable to
formalists only when the concept of truth itself is formalized, as
in model theory. In other words, the axioms of mathematics do
not reflect any higher reality; the Platonic world of mathematical
objects and the corresponding Platonic truths about these objects
do not exist. This leads to the following definition of formalism.
\begin{definition}[Formalism]\label{def1}
According to formalism, the only legitimate `truths' regarding
formal propositions in the language of a theory are the theorems
provable in that theory and the truths in models for that theory,
when suitably formalized in a stronger theory (i.e., the metatheory).
The theorems of a given theory do not reflect any metamathematical (Platonic)
`reality'. Equivalently, no such metamathematical truths ought to be
deducible from the theorems of a given theory; for that would mean that
such informal/metamathematical/Platonic truths have been used in
formulating the axioms of that theory.
\end{definition}
To understand the implications of the above definition,
consider first the theory PA in FOPL and let GC stand for Goldbach's
conjecture. Let P be a suitable formalization, in ZFC, of
the proposition ``GC is undecidable in PA''. Suppose that
ZFC proves P (although we do not know whether this is the case).
From this proof, we can certainly deduce that PA is consistent
and that GC is true in the standard model of PA. From
Definition~\ref{def1}, it follows that these additional facts
must also be formalizable and provable in ZFC; in fact the proof
of P is also a proof in ZFC: (a) of the existence of the
standard model of PA (suitably formalized), (b) of GC in the
standard model of PA and (c) of con(PA) (which formalizes ``PA is
consistent''). If any of (a), (b) and (c) above were to be either
not formalizable in the language of ZFC or not provable in ZFC
despite the assumed provability of P, then one would have to conclude
that ZFC is an illegitimately defined theory according to the
formalistic philosophy outlined in Definition~\ref{def1}.
Of course, this is not the case in this specific instance.
But in what follows, we demonstrate that Definition~\ref{def1}
implies the inconsistency and/or illegitimacy of PA and in
fact, PRA (Primitive Recursive Arithmetic), as formulated in FOPL.

\subsection{The failure of formalism in FOPL}
In this subsection, whenever we mention PA, it is to be understood
that our comments apply equally well to PRA.
To get to the root of the problem in classical infinitary reasoning,
we begin by considering the most elementary theory postulating
infinitely many entities, namely, Successor Arithmetic~(SA). The two axioms
of SA are:
\begin{eqnarray}\label{SA}
&& \forall x \; \neg(S(x)=0), \nonumber  \\
&& \\
&& \forall x \forall y (S(x)=S(y) \Rightarrow x=y). \nonumber
\end{eqnarray}
Here $S$ is the successor function.
The induction axiom scheme (not included in SA) is defined by
\begin{equation}\label{Ind}
P(0) \; \& \; \forall x(P(x) \Rightarrow P(S(x)))
\Rightarrow \forall x P(x),
\end{equation}
where $P$ represents any property of the natural numbers expressible
in the language of SA. We will later consider (\ref{Ind}) as a
proposition in SA and comment on the fact that classical logic
requires (\ref{Ind}) to be undecidable in SA.

Consider the number-theoretic proposition Con(SA), which formalizes
``SA is consistent''. It is known that
\begin{equation}\label{PAConSA}
\mbox{PA} \vdash \mbox{Con(SA)},
\end{equation}
which should be read as ``PA proves Con(SA)''. Indeed, PA proves
the consistency of every finite subset of its axioms and this
includes SA. Keeping in mind Definition~\ref{def1},
let us carefully examine the consequences of (\ref{PAConSA}).

Let $N$ denote the infinite class of all natural numbers in classical
arithmetic, i.e., $N=\{0,S(0),S(S(0)),...\}$. Note that $N$ is the
standard model for SA. In the terminology of nonstandard arithmetic,
every natural number is \emph{standard finite} by definition
(as opposed to \emph{nonstandard finite}); we reserve the word
`integer' for numbers that may possibly be nonstandard finite.
We state the main result of this subsection in the following metatheorem:
\begin{theorem}\label{mt1}
Let $Q$ be the proposition that formalizes the existence of
$N$ as an infinite class. Definition~\ref{def1} and
equation~(\ref{PAConSA}) imply that $\emph{PA} \vdash Q$. Consequently,
nonstandard models for \emph{PA} cannot exist and by G\"odel's
incompleteness theorems, \emph{PA} is inconsistent.
\end{theorem}
The question of how $Q$ can be a legitimate
proposition of PA is addressed in Remark~\ref{rm1}.
The simplest proof of metatheorem~\ref{mt1} is as follows.
\begin{proof}
The consistency of SA (i.e., Con(SA)) is equivalent in FOPL to
the existence of a model for SA, which must either be a standard
model ($N$) or a nonstandard one. To prove the metatheorem, one only
needs to demonstrate that the existence of a nonstandard model
for SA implies $Q$ (as is done in the ensuing paragraph); this would make
\begin{equation}\label{SAequivQ}
\mbox{Con(SA)} \Leftrightarrow Q.
\end{equation}
From (\ref{SAequivQ}), (\ref{PAConSA}) and Definition~\ref{def1}
it would then follow that
\begin{equation}\label{PAQ}
\mbox{PA} \vdash Q.
\end{equation}
To see why (\ref{PAQ}) must follow, note the example for GC discussed below
Definition~\ref{def1}. For (\ref{SAequivQ}) makes the truth of $Q$
essential to formalize the very notion of a model for
SA, i.e., to formalize `SA is consistent' via Con(SA).
Definition~\ref{def1} then forces the
conclusion that PA must prove $Q$; in the absence of such a proof, we
would be able to draw the conclusion from (\ref{SAequivQ}) that $Q$ is
informally/metamathematically/Platonically true, in violation
of Definition~\ref{def1}. A proof in PA of $Q$ would amount
to a denial in PA of the existence of nonstandard integers
and the metatheorem would follow.

The proof that the existence of a nonstandard model for SA implies $Q$
is as follows. The very notion of a
nonstandard integer requires the existence of the class $N_s$ of
`all' standard non-negative integers; a nonstandard positive
integer, \emph{by definition}, is required to be greater than every
member of $N_s$. Of course, $N_s$ can only
be defined by putting it in one-to-one
correspondence with $N$; such a mapping would be called ``external''
in nonstandard analysis. So it is impossible to formalize the existence
of a nonstandard model for SA without first postulating $Q$, i.e., the
existence of $N$. It follows that the existence of
\emph{any} model for SA, or equivalently, con(SA),
is logically equivalent to $Q$, and (\ref{SAequivQ}) follows.
\end{proof}
\begin{remark}\label{rm1}
The reader's first reaction upon looking at (\ref{PAQ}) will
probably be ``PA supposedly does not even formalize the notion of
`standard finite' required to formulate the
proposition $Q$ and so cannot possibly prove $Q$''. But
this claim is true if and only if one already presumes
that PA is consistent and that therefore nonstandard models for PA
exist. Since metatheorem~\ref{mt1} falsifies this claim, one has to
re-examine it in that light. Our contention is that \emph{every}
universally quantified proposition, in particular, Con(SA), is
logically equivalent to $Q$. When PA proves that
something is true for `all' integers, Definition~\ref{def1} demands
that the notion of `all' \emph{must} also be formalized as the
existence of an infinite class of integers which \emph{must} be taken
as provable in PA. But the proof of metatheorem~\ref{mt1} shows
that the existence of \emph{any} such infinite class of integers
(i.e., \emph{any} model for SA) is in fact logically equivalent to $Q$. One
example of a universally quantified proposition provable in PA is
\[
\forall n \exists m \; (m > n).
\]
The truth of this proposition clearly allows us to draw the
inference (via a proof by contradiction) that infinitely many integers
of the form $\{0,1,2,...\}$ exist and therefore $Q$ must be `true'.
Definition~\ref{def1} would make PA an illegally defined theory if
such an inference were not formalizable and provable in PA;
taking $Q$ as `true-but-unprovable' is unacceptable in formalism.

In fact the following proposition,
provable in SA, is also logically equivalent to $Q$:
\[
\forall x \exists y \; (y=S(x)).
\]
This means that SA proves its own consistency; this is not surprising,
because as we will argue below in Remark~\ref{rm3}, the very notion of
SA as a theory can only be formalized with the unavoidable assumption
that $Q$ is `metamathematically true'. Definition~\ref{def1} then
demands that $Q$ be provable in SA. Of course, this does not make SA
inconsistent because SA is too weak for G\"odel's theorems to apply.
It follows that nonstandard integers do not exist, period. So in fact
even G\"odel's incompleteness theorems and the
completeness/compactness theorems of FOPL
do not go through, because, as noted earlier, they require theories at
least as strong or even stronger than PRA to formulate and
metatheorem~\ref{mt1} shows that PA (PRA) is inconsistent.
There is clearly a problem of circularity here; the inconsistency
of PA (PRA) is deduced from G\"odel's theorems, which however, are
unreliable because of said inconsistency. In Section~\ref{sec2}, we
observe that a new logic~\cite{SR} which accepts the requirement
of metatheorem~\ref{mt1} that $\mbox{PA} \vdash Q$,
but rejects the validity of G\"odel's theorems
because of their self-referential nature, will be needed to justify
the axioms of PA from the point of view of formalism.
\end{remark}
\begin{remark}
Another way of looking at Definition~\ref{def1} is as follows. If
a proposition were to be undecidable or cannot
even be formalized in a theory, then the metatheory that formulates
such a theory should in principle be able to either affirm or deny
that proposition via a proof/refutation, or not even decide/formalize
such a proposition. Thus formalism requires that
the truth or falsity of such a proposition
should not be essential in specifying that theory. In the case
of $Q$, one finds that it is essential to assume it as `true' in
formulating \emph{any} infinitary axiomatic theory of FOPL
(see Remark~\ref{rm3} below), in particular, SA. So $Q$ cannot be
denied in the metatheory that formalizes SA, i.e., $Q$ must be `really'
true in every model for SA. Definition~\ref{def1} then requires
$\mbox{SA} \vdash Q$. An important consequence of this fact
is that the induction axiom scheme~(\ref{Ind}) must be taken
as provable in SA as explained below.
It is the assumed undecidability of (\ref{Ind})
in SA that leads to the existence of nonstandard models for SA,
denied herein. To see why, consider the theory SA*, defined as
SA with an additional predicate $St$ and the following additional
axiom:
\begin{equation}\label{St}
St(0) \; \& \; \forall x(St(x) \Rightarrow St(S(x))).
\end{equation}
Clearly, every natural number $n$ will satisfy $St(n)$. But the
assumed undecidability of (\ref{Ind}) implies  $\forall x St(x)$
is not provable in SA* and so there must exist a nonstandard model
for SA* in which $\exists x \: \neg \: St(x)$ is true; such an $x$ would
be a nonstandard integer. Definition~\ref{def1} shows that (\ref{Ind})
must in fact be provable in SA and hence SA*; this means
that nonstandard integers do not exist and $St$
becomes a superfluous predicate that may be thought of as defining
`standard finite'. Observe that the undecidability of (\ref{Ind}) in
SA is established in FOPL only by circular reasoning; the theory
that establishes such undecidability \emph{presumes} the existence
of nonstandard integers (via its own consistency, which is a tacit
assumption); so what such a theory really establishes is the
tautology `If (\ref{Ind}) is undecidable in SA,
then (\ref{Ind}) is undecidable in SA'. 
\end{remark}
\begin{remark}\label{rm3}
The proposition Con(SA) literally denotes
``There does not exist a proof of `0=S(0)' in SA''. Of course,
this raises the question of what ``There does not
exist'', ``proof'' and ``SA'' denote. It is clear that the
theory~SA can only be defined, in particular, by identifying its
infinite class of well-formed formulae~(wff's), each of which is
a string of \emph{standard finite} (as opposed to
\emph{nonstandard finite}) length, and its infinite class
of proofs each of which must contain a standard finite number
of wff's. Therefore what Con(SA) `really' denotes is:
``The infinite class of SA-proofs does not contain within it a proof
of `0=S(0)', or equivalently, does not contain within it a pair of
SA-proofs which come to contradictory conclusions''. It is absolutely
essential to note that the ``infinite class'' of SA-proofs (or wff's)
referred to above can only be formally defined by mapping the SA-proofs
(wff's) to the class $N$ of all natural numbers.
If such a mapping is not done, the notion of
``all SA-proofs'' or ``all wff's of SA'' cannot be said to have been
formalized. The requirement that $N$ contain `all' and \emph{only} standard
finite (natural) numbers is also absolutely essential; it is easy to
show that if one permits nonstandardly long proofs/wff's, then SA
will be inconsistent. One concludes that to even formulate SA as a
theory one has to assume the truth of $Q$.
Even within a nonstandard model for SA, `all' SA-proofs and
wff's must necessarily be identified to be of standard finite length,
i.e., mapped to $N$; it is only with such identification that one can
meaningfully assert that `all' theorems of SA are true within such a
nonstandard model. As noted earlier, the nonstandardly long candidates
for `wff' or `proof' must be rejected in order to prove that a given
(nonstandard) structure is in fact a model for SA. This fact augments
the assertion in the proof of metatheorem~\ref{mt1} that the very
existence of nonstandard integers requires $Q$ to be true.
The main point of this remark is that it is impossible to
formalize the notion of SA as a theory and its consistency via Con(SA)
without first formally postulating the existence of $N$. 
\end{remark}
\begin{remark}
Note that Con(SA) is a purely number-theoretic (universally
quantified) proposition. To interpret it as meaning
`SA is consistent' (or equivalently, `There exists a model for SA')
requires formulating this latter proposition
in a stronger theory than PA and translating it into the
PA-proposition Con(SA) using the techniques developed by
G\"odel~\cite{Gd}. That such an infinitary proposition can
even be translated into PA clearly demonstrates that PA `really'
proves the existence of an infinite class. Metatheorem~\ref{mt1}
forces us to conclude (\ref{SAequivQ}) and (\ref{PAQ}). Hence
Definition~\ref{def1} implies that G\"odel really
translated the proposition $Q$ (i.e., `There exists the standard
model $N$ of SA') into Con(SA). The claim that `There exists a
model for SA' can be translated into Con(SA) without at
the same time translating $Q$ is a matter of Platonic belief. But
this (Platonic) leap of faith is unacceptable in formalism because
any metatheory that formalizes ``There exists a model for SA''
must necessarily \emph{prove} its equivalence to $Q$; to translate
one into Con(SA) is to translate the other.
\end{remark}
\begin{remark}
As noted in Remark~\ref{rm1},
the objection that PA does not even contain the predicate
`standard' and so cannot possibly formulate $Q$ is met by the fact
that if nonstandard integers do not even exist, such a predicate is
unnecessary. As observed earlier, in nonstandard arithmetic,
the class of `all' standard integers $N_s$ is first defined by putting
it into one-to-one correspondence with $N$. But \emph{by fiat}, such
a mapping, required to define a nonstandard integer, is deemed
`external'; only `internal' propositions are legitimate in nonstandard
arithmetic. Hence the class $N_a$ of `all' nonnegative integers and the
class $N_s$ in nonstandard arithmetic do not coincide, even though
their definitions are \emph{identical} except for the word `standard'.
The definition of $N_a$ is given by
\[
0 \in N_a \; \& \; \forall x \; (x \in N_a \Rightarrow S(x) \in N_a).
\]
To define $N_s$, one merely introduces the predicate `standard' as
follows:
\[
0 \in N_s \; \& \; \forall^{st} x \; (x \in N_s \Rightarrow S(x) \in N_s),
\]
where `$\forall^{st} x$' should be read as `for all standard $x$'.
Thus merely by introducing the word `standard', the meanings of
`all' in `all integers' and `all standard integers' do not coincide
in these two otherwise identical definitions of $N_a$ and $N_s$.
Defnition~\ref{def1} essentially tells us that formalism will not
permit such obfuscation of the meaning of the world `all'; Platonism
is inherent in such obfuscation (which would make nonstandard integers
`internally nonstandard finite', but `externally infinite').
In other words, formalism requires `all' to have a unique meaning
in the two definitions given above.
\end{remark}
\begin{remark}\label{rm6}
Let $Con(n)$ be the arithmetical proposition equivalent to the
consistency of the first $n$ axioms of PA (suitably enumerated),
where $n$ is a natural number (i.e., $n \in N$; for convenience,
we take $n=0$ to denote the null set of axioms). By the compactness
theorem,
\begin{equation}\label{compactness}
\mbox{Con(PA)} \Leftrightarrow \forall n \: \mbox{Con}(n).
\end{equation}
It is also known that for each \emph{given} natural number m
(here `m' is a constant symbol),
\begin{equation}\label{PAConm}
\mbox{PA} \vdash \mbox{Con(m)}, \quad  \mbox{m} \in N.
\end{equation}
Note that according to conventional wisdom,
(\ref{PAConm}) is \emph{not} to be interpreted as
\begin{equation}\label{PAConn}
\mbox{PA} \vdash \mbox{Con}(n),
\end{equation}
which is the same as `PA proves the \emph{open} formula Con($n$)',
where $n$ is a free variable ranging over all non-negative integers.
Such an interpretation is illegal in FOPL
because by universal generalization and
(\ref{compactness}), (\ref{PAConn}) would amount to
$\mbox{PA} \vdash \mbox{Con(PA)}$ and make PA inconsistent
by G\"odel's second incompleteness theorem. Metatheorem~\ref{mt1}
shows, however, that (\ref{PAConm}) and (\ref{PAConn}) are
in fact equivalent, since nonstandard integers do not exist;
from either of these formulae, one can infer the existence of
$N$ and by Definition~\ref{def1}, $\mbox{PA} \vdash Q$.
Formalism requires that an `arbitrary constant' like m in (\ref{PAConm})
is exactly the same as the free variable $n$, since both range over
`all' nonnegative integers. To give a different meaning to `all' in these
two contexts when it is clear that the axioms of PA do not imply
any such difference is illegal according to formalism.
\end{remark}
\begin{remark}
One may also conclude that Turing's halting problem ought not to be
undecidable, for the same reason that G\"odel's theorems do not
apply: nonstandard integers cannot exist, by metatheorem~\ref{mt1}.
It follows that Cantor's diagonalization procedure, used by G\"odel
and Turing to deduce their incompleteness results, must be illegal. 
Similarly, the axioms for addition and multiplication and (\ref{Ind})
(as noted earlier) cannot be undecidable in SA since these axioms can
only fail in nonstandard models. In Section~\ref{sec2}, we
demonstrate that the author's proposed
non-Aristotelian finitary logic~(NAFL)~\cite{SR}
is consistent with and justifies all these restrictions.
\end{remark}
\begin{remark}
Nevertheless, if one insists that PA does not formalize the notion of
``standard finite'' and hence does not prove $Q$
despite (\ref{PAConSA}), then one concludes that PA is illegitimately
defined from the strictly formalistic standpoint of
Definition~\ref{def1}. One option would be to abandon
formalism as a valid philosophy of classical mathematics and resort to
Platonic existence of $N$. The argument here would be that since
$N$ ``really'' exists (in a Platonic world), notions such as ``all''
theorems/proofs/wff's of SA do not have to be formalized by PA,
eventhough such notions are required to interpret the PA-proof
of Con(SA) as meaning ``SA is consistent''. The proposition $Q$
is therefore being taken as Platonically `true', eventhough unprovable
in PA. Of course ZFC would prove $Q$, but then one is
taking the axioms of ZFC as Platonically true, i.e., one is assuming
the Platonic existence of the ``universe of ZFC sets''. Hence Platonism
is inherent in classical infinitary reasoning.
\end{remark}
\begin{remark}
The arguments of this subsection lead to the strong
conclusion that Hilbert's Program is decisively
settled \emph{negatively} from the finitary and formalistic
standpoints; classical PA~(PRA), and hence classical infinitary
reasoning, would be \emph{inconsistent} if one insists on
Definition~\ref{def1}. From the finitary standpoint, 
one must also deny the legitimacy of ZFC in formalizing the
`truth' of the existence of $N$. The second option is to accept this
conclusion, i.e., to reject Platonism and insist on Definition~\ref{def1}
as valid. Since this would make PA~(PRA) inconsistent, a new logic would
be required to implement formalism as a philosophy of infinitary
reasoning in mathematics. In Section~\ref{sec2}, we demonstrate that
Definition~\ref{def1} is consistent with the truth definition
given in the Main Postulate of the logic~(NAFL)
proposed by the author~\cite{SR}; in other words, strict formalism
inevitably leads one away from classical logic and into NAFL.
\end{remark}

\section{Formalism in non-Aristotelian finitary logic}\label{sec2}
In Section~\ref{sec1}, we saw that a
consistent (non-circular) interpretation of
formalism is not possible within classical logic; formalism
requires one to reject G\"odel's and Turing's incompleteness
results and hence the Cantor diagonalization argument as
self-referential; nonstandard integers also cannot exist. In
NAFL~\cite{SR}, these restrictions are justified rigorously
by demonstrating that infinite sets cannot exist, and so $N$ (the
class of all natural numbers) must be a proper class. Diagonalization
will then be seen to fail because of the restriction that one cannot
quantify over infinitely many infinite (proper) classes, as explained
later. Other important implications for quantum mechanics, the relativity
theories and non-Euclidean geometries are also discussed.

\subsection{The Main Postulate of NAFL}
Definition~\ref{def1} seemingly provides an intuitively correct
definition for formalism; yet it is not sustainable within classical
logic. The flaw is in the requirement of classical logic that
the law of the excluded middle~(LEM) must necessarily apply to an
undecidable proposition in a consistent theory. It is this particular
requirement that makes Platonism inherent in classical logic.
NAFL does away with LEM and also the law of non-contradiction~(LNC)
via the truth definition given by its Main Postulate
(see Sec.~2 of \cite{SR}), which provides the appropriate
generalization of Definition~\ref{def1}. This makes formalism
sustainable in NAFL, but with severe restrictions on classical
infinitary reasoning.

The fundamental assumption of NAFL is that the \emph{only}
metamathematical objects that exist are axiomatic theories
(which have the same rules of inference as classical FOPL theories)
and their \emph{models}, which are structures in which all the axioms
of these theories and their logical consequences are assigned `true';
propositions undecidable in an axiomatic theory may be assigned `true',
`false' or `neither true nor false'. This last option makes
NAFL models different from classical models as will become clear
from the explanations below. Formal mathematical objects do not
have any existence outside of the theories
in which they are postulated. There are
no `truths' outside of these axiomatic theories for formal propositions
of NAFL; this is in keeping with Definition~\ref{def1}. Platonic truths
do exist in NAFL, but these are regarding propositions \emph{about}
axiomatic theories which \emph{cannot} be formalized in consistent
NAFL theories, because of their self-referential nature (and also
because the theories themselves are not formal objects); examples of
such non-formalizable propositions are
provability/refutability/undecidability of
formal propositions with respect to the theories in which they are
formulated, and the consistency of NAFL theories. In NAFL, a theory
is consistent if and only if it has a model; this definition
also holds in FOPL, but the NAFL notion of consistency is a
metamathematical one and is not quite the same as that of
classical logic, for reasons that will be
explained later. It immediately follows that in NAFL,
truths for formal propositions can
only exist with respect to axiomatic theories; there cannot exist
any absolute truths in just the \emph{language} of a theory.

This raises the question of what it means
for a proposition $\Psi$ to be true or false in a consistent NAFL
theory T. If $\Psi$ is provable/refutable in T, then it is certainly
true/false in T, i.e., a model for T will assign $\Psi$ to be true/false.
If $\Psi$ is undecidable in T, i.e., neither
$\Psi$ nor its negation $\neg \Psi$ is provable in T, then
the Main Postulate of NAFL provides the appropriate truth definition as
follows: $\Psi$ is true/false in T if and only if $\Psi$ is
provable/refutable in an \emph{interpretation} T* of T. Here
`interpretation' is defined as an axiomatic theory T* that resides
in the human mind and acts as the `truth-maker' for
(a model of) T; it immediately follows that T*
must prove all the axioms and theorems of T. Thus far it appears
that NAFL is not much different from classical logic and that the
NAFL truth definition coincides with Definition~\ref{def1}. The crucial
difference occurs when $\Psi$ is undecidable in T*; in this case
NAFL interprets $\Psi$ as neither true nor false in T, and
metatheorems~1~and~2 of \cite{SR} show that both LEM and LNC fail for
$\Psi$, in a non-classical model for T in which $\Psi \& \neg \Psi$ is the
case. This non-classical model is essentially a superposition of
two or more classical models. Here we are using
the words `classical model' and `non-classical model' only with
respect to the truth values for $\Psi$. Since the NAFL model for T
will, in general, contain some proposition undecided in T*, it will
always be non-classical with respect to this proposition.

The essence of the Main Postulate is that an undecidable proposition
$\Psi$ in a consistent NAFL theory T is true/false in T if and only
if it has been \emph{axiomatically asserted} as true/false by virtue of its
provability/refutability in the interpretation T* of T. This essentially
means that $\Psi$ is true/false in T if and only if
$\mbox{T*}=\mbox{T}+\Psi/\mbox{T}+\neg \Psi$; this notation is
used in \cite{SR} to emphasize the fact that $\Psi$ ($\neg \Psi$)
is an \emph{axiomatic declaration} with respect to T, regardless of its
status as an axiom or otherwise in the theory T*. Note in
particular that axiomatic assertions are made by human beings, and that
T* resides in the human mind. In the absence of any axiomatic assertions
regarding $\Psi$, (i.e., if $\Psi$ is undecidable in T*),
consistency of T demands that there must
exist a non-classical model for T in which $\Psi$ is neither true
nor false, i.e., $\Psi \& \neg \Psi$ is the case. The (non-classical)
interpretation of $\Psi \& \neg \Psi$ is explained in the ensuing
subsection.

\subsection{The philosophical basis for NAFL}
The first question that one may ask is \emph{why} the truth
for undecidable propositions in a consistent theory~T
is axiomatic in NAFL. Here there are two important points
to be understood. Firstly, in NAFL there is no
Platonic world in which formal propositions are either true or false,
independent of an axiomatic declaration (in the interpretation T*
of T). Secondly, NAFL interprets LEM for a T-undecidable proposition
$\Psi$ to mean `$\Psi$ is either true or false'; since there is
no Platonic world in which such truth/falsity occurs independent of
the human mind, the axiomatic nature of truth in NAFL follows and
LEM holds if and only if an axiomatic declaration of truth/falsity of
$\Psi$ is made (via provability) in T*. In the absence of
such an axiomatic declaration, the failure of LEM and LNC follows
for the reasons explained in metatheorems~1~and~2 of \cite{SR}.
In particular, the classical refutation of $\Psi \& \neg \Psi$
in T proceeds as follows: ``If $\Psi$~($\neg \Psi$) is true,
then $\neg \Psi$~($\Psi$) must be false''. This classical argument
appeals to \emph{Platonic} truths of $\Psi$ and
$\neg \Psi$ in ``pre-existing'' models of T; i.e., these classical
models have to be assumed to ``exist'' prior to and independent
of any axiomatic declarations of truth made in T. In NAFL, on the other
hand, there are no such Platonic truths and no ``pre-existing'' models.
The NAFL model of T is generated by its interpretation T*, which
is also an axiomatic NAFL theory. Hence the NAFL model of T has only a
temporary existence in the human mind and the `truths' in this model
are axiomatic declarations generated \emph{after} T  has been specified.
In summary, the attempted (classical) refutation of
$\Psi \& \neg \Psi$ in T fails in NAFL because such a refutation must
necessarily appeal to \emph{axiomatic} (as opposed to the classically
Platonic) truths of $\Psi$ and $\neg \Psi$ and so the refutation
is valid only in the NAFL theories T+$\Psi$ and T+$\neg \Psi$.
Note that this failure of LNC makes LNC equivalent to LEM in NAFL,
unlike intuitionistic logic (where LEM fails, but LNC holds for
undecidable propositions in a theory).

We first list some results explained in
detail in Remarks~1--7 of \cite{SR}. The failure of LNC in a
non-classical model for T is a unique NAFL phenomenon, and has the
following explanation: `$\Psi$' in $\Psi \& \neg \Psi$ asserts
that `$\neg \Psi$ has not been axiomatically
asserted as true~(provable) in T*',
while `$\neg \Psi$' in $\Psi \& \neg \Psi$ asserts that `$\Psi$
has not been axiomatically asserted as
true~(provable) in T*'; as in classical
logic (and unlike intuitionistic/constructive logics) there is no difference
between $\Psi$ and $\neg \neg \Psi$ in NAFL (see below under the
heading `The concept of negation in NAFL'). An important consequence
of the failure of LNC is that the classical assertion `From
$\Psi \& \neg \Psi$, any proposition can be deduced' fails in NAFL.
LEM and its negation are not legitimate propositions in NAFL theories.
A more general result (as noted in Remark~5 of \cite{SR})
is that if $\psi$ and $\phi$ are undecidable
propositions in a theory T, then $\psi \Rightarrow \phi$ is a
legitimate proposition of T if and only if $\phi$ ($\neg \psi$) is
\emph{not} a theorem of T+$\psi$ (T+$\neg \phi$) (or equivalently,
if and only if $\psi \Rightarrow \phi$ is \emph{not}
classically deducible in T). At this stage
the reader might wonder how $\psi \Rightarrow \phi$ can be classically
deducible in T and yet be an illegitimate proposition of an NAFL theory T,
which has, after all, the same rules of inference as classical FOPL
theories. This is explained in detail under the ensuing heading,
where the syntax and semantics of NAFL theories are considered.

As noted earlier, consistency of an NAFL theory T and the
provability (or undecidability) of a formal
NAFL proposition in a theory T are propositions that cannot be
formalized in NAFL theories. All these `informal' propositions are
in fact valid propositions of the metatheory, which is NAFL itself;
as will be explained below, LEM does apply to these Platonic
(informal) notions, i.e., they are either true or false,
independent of the human mind. For this reason, the notion of
`consistency' is not the same in NAFL and FOPL; in NAFL (unlike
FOPL), a proposition can be undecidable in an inconsistent theory
(which is rendered inconsistent by the fact that the required
non-classical model for that theory cannot exist).
So in NAFL (unlike classical/intuitionistic/constructive logics),
the assertion that `any proposition can be deduced in an
inconsistent theory' fails.

\subsubsection*{Syntax of an NAFL theory, syntax of
its proofs and the metatheory}
We now discuss a very important issue of syntax versus semantics
not clearly addressed in \cite{SR}. In NAFL, the \emph{syntax of
a theory}, which we will henceforth refer to as `t-syntax',
consists essentially of all its legitimate
propositions, including the axioms, theorems and undecidable propositions;
in particular, the t-syntax will not admit certain (classically acceptable)
propositions deemed `illegitimate' or `not formalizable' in NAFL, such as,
LEM~(LNC) or its negation for propositions undecidable in that theory.
More generally, as noted earlier, the proposition
$\psi \Rightarrow \phi$ is illegitimate in the t-syntax if $\psi$
and $\phi$ are undecidable in T and $\psi \Rightarrow \phi$ is
classically provable in T. The notion of provability/undecidability
is fixed by a second level of syntax in NAFL, namely,
the \emph{syntax of proofs in a theory}, which we will henceforth
refer to as `p-syntax'. The p-syntax of a theory T will include
all the rules of inference of FOPL, in
addition to \emph{all} the (classically legitimate)
propositions in the language of the theory. In particular, the p-syntax
is purely classical and will admit some propositions, such as
LEM~(LNC) or its negation, or the more general example noted above,
which are deemed illegitimate in the t-syntax. Thus
LEM~(LNC) is assumed true in the p-syntax and may occur in
\emph{proofs} of legitimate propositions in the t-syntax; but LEM~(LNC)
and its negation by themselves cannot occur
in the t-syntax. An example of this
situation is a deduction $\psi \Rightarrow \phi \& \neg \phi$
in the p-syntax of T for a proposition $\phi$ that
is undecidable in a theory T. Such a deduction is a legitimate proof
by contradiction (in the p-syntax) of
$\neg \psi$ in T \emph{despite} the fact that
$\phi \& \neg \phi$ and its negation are illegitimate in the t-syntax
and also despite the fact that in the \emph{metatheory} there does exist a
non-classical model for T in which $\phi \& \neg \phi$ is the case.
This metatheory, of course, is NAFL itself, which provides the semantics
for the t-syntax. The notions of consistency of T and those of
provability/refutability/undecidability of propositions in T
are purely metamathematical notions (permitted only in the metatheory)
and cannot even be expressed in the language of T in NAFL (note that
G\"odel's translation of these notions into number-theoretic
propositions is not valid in NAFL essentially because of their
self-referential nature). Another reason why the notion of provability
or undecidability of propositions is not formalizable in NAFL theories
is clearly the fact that the p-syntax admits classical inference rules
including propositions illegitimate in the t-syntax; this feature
of the p-syntax makes it Platonistic in intent, while the t-syntax
is formalistic.

The  p-syntax is Platonistic (i.e., admits
classical inference rules) because this is the only non-circular
way in which the concept of undecidability of propositions
or that of consistency of a theory can even be defined. As an example,
consider the example of the assumption $\psi$ leading to the
conclusion $\neg \psi$ in an NAFL theory T;
in the p-syntax of T this is a proof by contradiction
of $\neg \psi$. Clearly LNC, i.e., $\neg (\psi \& \neg \psi)$, has been
assumed in this proof; the objection that LNC need not hold by the
Main Postulate if $\psi$ is undecidable in T will not make sense
in the p-syntax because the notion of undecidability of $\psi$ is valid
in the first place only \emph{after all proofs} of T are available
(note that the undecidability of $\psi$ in T means that the class of
all proofs in T does not include within it either a proof of $\psi$
or a proof of $\neg \psi$). This argument also explains why a deduction
of $\psi \Rightarrow \phi \& \neg \phi$ in the p-syntax of T is a
proof of $\neg \psi$ in T despite the possible undecidability of
$\phi$ in T.

The author believes that intuitionism fails to provide a non-circular
definition of the concept of undecidability of propositions in theories
because intuitionism does not distinguish between the p-syntax and the
t-syntax. As an example, let $\mbox{T}_0$
be the null set of axioms. In NAFL, every legitimate proposition
of $\mbox{T}_0$ is undecidable in $\mbox{T}_0$; this assertion
is made in the metatheory and there is no `proof' for it because
the p-syntax of $\mbox{T}_0$ does not admit the concept of undecidability.
In fact it is self-evident that this this assertion cannot be proved
in $\mbox{T}_0$ for precisely the same reason that it is true -- nothing is
provable in $\mbox{T}_0$. Thus the attempt to formalize the notion of
undecidability in $\mbox{T}_0$ in NAFL will violate the Main Postulate.
Intuitionism, on the other hand, insists on a proof for this assertion,
which is non-existent, and as a result comes to the conclusion
that it is not even valid to assert that every proposition is either
provable or refutable or undecidable in intuitionistic theories.
Classical logic accepts this last assertion
but insists that the concept of provability/undecidability
is formalizable. This results in self-reference
and Platonism for the truth of formal
propositions of a theory, not acceptable in NAFL.
Intuitionism also fails to get rid of Platonism because it insists
on LNC for undecidable propositions of a theory; this forces
intuitionists to look for formal `proofs' of undecidable propositions
outside of the theory (e.g., $\mbox{T}_0$). In summary,
NAFL requires the p-syntax to be Platonistic and the t-syntax to be
formalistic; intuitionism fails on both counts by rejecting LEM in
the p-syntax and by accepting LNC in the t-syntax.

Note that the failure of LNC~(LEM) for an undecidable
proposition of an NAFL theory T in a
non-classical model occurs in the metatheory, because models
are metamathematical objects. This does not contradict the t-syntax,
because LNC~(LEM) is not even a legitimate proposition of the t-syntax.
Thus no inconsistency is implied by the existence of such a non-classical
model. A second important point regarding the metatheory is, as noted
earlier, that LEM applies to all (informal) propositions occurring in
the metatheory. Thus the metatheory requires that
a theory is either consistent or inconsistent,
and a formal proposition (in the t-syntax) is either provable or
refutable or undecidable in a given theory, possibly independent of
the human mind. In summary, the metatheory
is scrupulously Platonistic in intent, in contrast to the (formal)
theory itself. This is so because NAFL insists that the propositions
in the metatheory \emph{must} make sense in the real world. Thus, in
the real world, one has either axiomatically
declared an undecidable proposition $\Psi$ in a consistent NAFL
theory T to be true or false or neither (the last disjunct
occurs by default; it is not legal to declare a
proposition $\Psi$ to be `neither true nor false' in T, for that
would amount to adding $\Psi \& \neg \Psi$ formally as
an axiom, which is not permitted by the t-syntax). It is not
legal in the real world for the human mind that interprets T to
assert that he/she does not know which of these is the case, or
to assert that none of these options hold. In this respect,
NAFL differs from both classical logic and intuitionism.

\subsubsection*{Open formulas and the meaning of `existence' in NAFL}
An immediate consequence of metatheorem~2 of \cite{SR} (which asserts
the failure of LNC and the existence of a non-classical model for
a consistent theory in which a given proposition is undecidable)
is that open formulas (with free variables) and formulas with
`arbitrary constants' in them in a given theory are in fact
universally quantified formulas with respect to the free
variables/arbitrary constants. The reason is that the theory
in question clearly does not decide the values of the free
variables/arbitrary constants which must therefore be in
a superposed state of assuming all possible values.
It follows that the two formulae in (\ref{PAConm}) and
(\ref{PAConn}) are in fact equivalent in NAFL (to a universally
quantified formula) and this is in conformity with the
requirements of formalism as stated in Remark~\ref{rm6}.
It also follows that an NAFL theory which asserts the existence
of a \emph{unique} $x$ such that some property $P(x)$ holds, but
does not provide a construction (value) for that $x$, is an
inconsistent theory. This is so because the uniqueness requirement
precludes the existence of a non-classical model for that theory
with values of $x$ superposed; but such existence is required for
the consistency of an NAFL theory in which the supposedly
unique value of `$x$' in  $\exists x P(x)$ is undecidable.

In NAFL, the issue of the meaning of `existence' of entities within
a theory is resolved as follows. Clearly, NAFL rejects Platonic
existence of mathematical entities. In constructive/intuitionistic
logics, existence of an entity has the meaning that a
\emph{construction} must necessarily be available for that entity;
i.e., $\exists x P(x)$ can only be asserted by specifying such
a construction for $x$. NAFL is not quite as restrictive;
existence of an entity $X$ in an NAFL theory T is to be interpreted
as meaning ``$X$ is a legal entity of T'', i.e., it is legal to
speak of $X$ in propositions/theorems of T. A construction for
such an $X$ need not necessarily be available within T. But
in a proposition of an NAFL theory T such as $\exists x P(x)$,
whether a construction for such an $x$ is required or not depends
on whether metatheorem~2 of \cite{SR} will permit such a
proposition to be undecidable within T. As an example, let $x$
range over the natural numbers. It is known that each natural number
has a unique construction available (built up from the null set, for
example, in set theory); so in this case, $\exists x P(x)$ \emph{cannot}
be undecidable in T; the required non-classical model cannot exist
because LEM must unavoidably apply to this proposition by virtue
of the definition of `natural number'.

For an example of non-constructive existence in NAFL, let $G$
stand for a suitable formalization of ``God exists'' in the null
set of axioms $\mbox{T}_0$; further, let $GG$ formalize
``God is great''. Clearly, $\mbox{T}_0$ does not specify any
construction for the entity `God', and so a non-classical model
for $\mbox{T}_0$ in which $G \& \neg G$ is the case does exist.
Hence undecidability of $G$ in $\mbox{T}_0$ is not a contradiction
and non-constructive existence is permitted here. Given the
axiomatic nature of truth in NAFL, the superposition $G \& \neg G$
means that neither $G$ nor $\neg G$ has been asserted axiomatically
in the interpretation T* of $\mbox{T}_0$, which is therefore
non-classical. This non-classical model clearly corresponds to
agnosticism, for an agonostic refuses to acknowledge that God is
either a legitimate or an illegitimate entity. Next consider the
proposition $GG \Rightarrow G$. This is clearly a rule of inference;
Platonically one would argue that `If God is great, then surely God
does exist'; in NAFL, $GG \Rightarrow G$ should be interpreted as
``If `God is great' is true then it is certainly a
legitimate sentence; it follows that God has to be
a legitimate entity and so `God exists' is true''.
So $GG \Rightarrow G$ is in the p-syntax of $\mbox{T}_0$
as a rule of inference. But since $G$~($\neg GG$)
is provable in the theory $\mbox{T}_0 + GG$~($\mbox{T}_0 + \neg G$)
and both $G$ and $GG$ are undecidable
in $\mbox{T}_0$, it follows from Remark~5 of \cite{SR} that
$GG \Rightarrow G$ is not in the t-syntax of $\mbox{T}_0$
i.e., it is not a legitimate proposition of $\mbox{T}_0$.
Therefore there does exist a non-classical model for $\mbox{T}_0$
(in the metatheory) in which both $G \& \neg G$
and $GG \& \neg GG$ are the case, i.e., no axiomatic assertions
have been made in T* regarding the truth or falsity of either $G$ or $GG$
and so both are neither true nor false. As noted in Remark~5 of
\cite{SR}, in this non-classical model $GG \Rightarrow G$ is also
neither true nor false; this would not be permitted if
$GG \Rightarrow G$ were in the t-syntax of $\mbox{T}_0$, since
it would then immediately become provable by virtue of its presence
in the p-syntax (as a rule of inference);
but then the said non-classical model required by
NAFL cannot exist and $\mbox{T}_0$ would become inconsistent.
Intuitively, the non-classical model simply asserts that for the
agnostic, ``If God is great then God exists'' is as meaningless
as ``God exists'' and ``God is great'' and so is just as entitled
to have a non-classical truth value of `neither true nor false'.
Careful thought will show that this is the correct formalistic
position; it is Platonism that forces $GG \Rightarrow G$ to
be a theorem of $\mbox{T}_0$ when both $G$ and $GG$ are undecidable
in $\mbox{T}_0$. To conclude this subsection, note that the believer
and atheist have respectively made the \emph{axiomatic} assertions $G$ and
$\neg G$ with respect to $\mbox{T}_0$ from the
NAFL point of view, eventhough they may personally believe
that God `really' exists/does not exist. NAFL essentially states
that their Platonic beliefs are irrelevant and they have ultimately
made axiomatic declarations of truth in an interpretation
T* of $\mbox{T}_0$.

\subsubsection*{The concept of negation in NAFL}
As noted earlier, for any proposition $\psi$,
($\neg \neg \psi \Leftrightarrow \psi$) holds
in the p-syntax of NAFL theories (as in FOPL and unlike
intuitionistic/constructive logics). But there are a couple of
subtleties regarding NAFL negation that need to be noted.

Firstly, note that in a non-classical model of a consistent NAFL
theory~T in which $\psi \& \neg \psi$ is the case
under the interpretation T*, the (classical) logical equivalence
$\neg \neg \psi \Leftrightarrow \psi$ certainly fails.
In fact even $\psi \Rightarrow \psi$ fails
since its negation is seen to hold. To avoid confusion, we reserve
the notation $\psi \Rightarrow \phi$ to \emph{always} mean the
\emph{classical} disjunction $\neg \psi \vee \phi$, whose negation
is $\psi \& \neg \phi$. The equivalence between $\psi$ and
$\neg \neg \psi$ holds in the non-classical model under a non-classical
interpretation which we define as $\neg \neg \psi \leftrightarrow \psi$.
Here $\psi \rightarrow \phi$ is a non-classical disjunction given
by $\neg \psi \vee \phi \vee (\neg \psi \& \phi)$, i.e., all three
disjuncts are possible \emph{even when $\phi$ is replaced by
$\psi$}. In the non-classical model,
$\psi$ expresses that $\neg \psi$ has not been \emph{classically}
asserted as an axiom (is not provable) in T*,
$\neg \psi$ expresses that $\psi$ has not been
\emph{classically} asserted as an axiom (is not provable) in T*
and their conjunction $\psi \& \neg \psi$ also obviously holds under
this interpretation. Similarly, the equivalence
$\neg \neg \psi \leftrightarrow \psi$ also holds;  both
$\neg \neg \psi$ and $\psi$ express the same concept in the
non-classical model and one can be substituted for the other.

Secondly, let $\psi$ stand for the outcome `one' in the roll of a dice,
and let $\neg \psi$ stand for its negation, i.e., any one of the
outcomes `two', `three', `four', `five' or `six'. Consider the null set of
axioms $\mbox{T}_0$. Suppose we add the axiom $\psi$ to
$\mbox{T}_0$ to obtain an interpretation T*. Then $\neg \psi$ is
certainly a legitimate proposition of $\mbox{T}_0$
and T* that stands refuted in T*.
But suppose we wish to add $\neg \psi$ to $\mbox{T}_0$ instead to obtain
the interpretation T*; \emph{now} $\neg \psi$ is also a legitimate
proposition of $\mbox{T}_0$, but it can be a legitimate
axiom of T* if and only if T* proves one of the outcomes `two', `three',
`four', `five' or `six'. The bottom line is that a
disjunction can be asserted as an \emph{axiom} of a consistent
NAFL theory if and only if that theory proves at least one of
the disjuncts. On the other hand, the disjunction can still be a
\emph{legitimate proposition} in the t-syntax of a theory even
if none of the disjuncts are proved, provided the restriction given
in Remark~5 of \cite{SR} is satisfied. In this example, the
said restriction is satisfied and the disjunction $\neg \psi$ is a
legitimate proposition of $\mbox{T}_0$ (because $\neg \psi$ is of the form
$A \Rightarrow B$, where $A$ and $B$ are undecidable in $\mbox{T}_0$
and $A \Rightarrow B$ is not classically deducible in $\mbox{T}_0$).
Of course, if \emph{all} disjuncts are refuted
by the theory (as in the above example where
$\neg \psi$ is such a disjunction in the theory $\mbox{T}_0 + \psi$),
then the (refuted) disjunction itself is in the t-syntax of that theory.
This example illustrates the difference between NAFL negation and
its classical and intuitionistic counterparts.

\subsection{Implications for some classical theories}\label{impl}
It turns out that metatheorem~2 of \cite{SR} is a killer of classical
infinitary reasoning in all but its weakest forms. The theory of
finite sets F, described in detail in Sec.~3 of \cite{SR}, is
essentially G\"odel-Bernays set theory with classes and without the
axiom of infinity (see Cohen~\cite{Coh}, pp.\ 73--78). Note that
we have used boldface notation for F in \cite{SR}. Since F is
equivalent to PA, we will only consider F in this paper. In Sec.~3 of
\cite{SR}, it is shown in detail that the undecidability of existence
of infinite sets in F is a contradiction because the non-classical
model for F required by metatheorem~2 of \cite{SR} cannot exist.
It is argued in \cite{SR} that infinite sets are self-referential
objects and must therefore be banned if F is to be consistent; in
other words, NAFL requires that the p-syntax
of F must include additional inference rules that would ban such
self-referential objects. In particular, Zermelo-Fraenkel set
theory would be inconsistent in NAFL. It is easy to
show that by similar reasoning, the axioms of F themselves
cannot be undecidable in weaker theories and so must be declared
as tautologously true in the p-syntax of F (i.e., they cannot be
denied).

The most important consequence of metatheorem~2 of \cite{SR} is
that the consistency of F demands that undecidable
propositions cannot exist in F, i.e., all propositions
of F in the t-syntax must be either provable
or refutable in F. This result may be
derived from the fact that nonstandard models of F cannot exist,
if F is consistent; indeed, this is obvious from the fact that
infinite sets cannot exist in \emph{any}
form in F. Alternatively, non-existence of
nonstandard integers can be established by arguments similar to
that in Sec.~\ref{sec1}; the Main Postulate of NAFL requires that
the existence of class $N$ of all (\emph{standard finite})
natural numbers be provable in F because it cannot be denied
in any model for F and NAFL does not permit the existence of $N$
to be `true-but-undecidable' in F. Note that the existence of $N$
is a proposition (denoted by $Q$) about \emph{formal objects} of
F, i.e., the natural numbers; so by the Main Postulate, it is
not legal in NAFL to assert that $Q$ is not in the t-syntax of F,
but is `true' in the metatheory. This violates the axiomatic
nature of truth regarding propositions about formal objects required
in NAFL. The existence of an infinite class
(such as, N) in an NAFL theory must
be equated with the existence of all of its objects, since the
infinite class by itself is not an object of any NAFL theory.
Thus any universally quantified proposition that asserts the
existence of infinitely many natural numbers (such as, the example
given in Remark~\ref{rm1}) proves $Q$ in F.
It is extremely important to note that the consistency
of F (or equivalently, consistency of PA) is no longer equivalent
to $Q$, which is a \emph{formal proposition} of F in NAFL. The
NAFL notion of consistency is different from the classical one.

It follows that G\"odel's
and Turing's incompleteness theorems must be illegal in NAFL, for they
predict the existence of undecidable propositions in F. The culprit
is the Cantor diagonalization principle, used by G\"odel and Turing;
this principle must be banned in NAFL because it is illegal in NAFL
to quantify over infinitely many infinite (proper) classes. Indeed,
such quantification speaks of infinite classes as infinite sets, since
it tacitly presumes that the `super-class' of these infinitely
many infinite classes exists. Note that quantification over finitely
many infinite classes can always be eliminated and so is not a problem.
So the notions of consistency and undecidability cannot be formalized
in NAFL because of their self-referential nature. It is doubtful if
there exist any methods acceptable in NAFL that would establish the
existence of undecidable propositions in F (and hence the
inconsistency of F). An important corollary of this result is that
some of the famous propositions of arithmetic, such as Fermat's last
theorem, Goldbach's conjecture, the Twin prime conjecture, etc., must
all be decidable in F. Further, Turing's halting problem must also
be decidable.

It is easy to demonstrate that Euclid's fifth postulate cannot be
undecidable in NAFL with respect to the first four. The reason again is
that if the first four postulates are consistent, the non-classical
model for these postulates (required to exist by NAFL)
in which the fifth postulate is neither
true nor false cannot exist; such existence would violate the
requirement of the first four postulates that a \emph{unique}
straight line must pass through any two given distinct points.
Hence non-Euclidean geometries should be
banned as self-referential in NAFL, and
all five Euclid's postulates must be declared as tautologously
true in the p-syntax. It follows that general relativity theory
is inconsistent in NAFL. The inconsistency of special relativity
theory~(SR) in NAFL is argued briefly in \cite{SR} and in greater detail
in \cite{SRT}, where strong grounds are established to suspect
inconsistency of SR even within classical FOPL.

\subsection{Quantum superposition justified in NAFL}
We consider two examples, namely, the four mirrors and the
Schr\"odinger cat experiments of quantum mechanics. These experiments
are well known and we will assume that the reader is aware of how
they are set up. We will show how quantum superposition is justified
in NAFL and the discuss the role of `measurement' in quantum mechanics.

\subsubsection*{The four mirrors experiment}
The essential, surprising result of this experiment is that in the
absence of a `measurement', the photon seems to take \emph{both} available
paths (call these A and B) simultaneously; any attempt to directly
detect this phenomenon fails and the photon is observed to take one
of the two paths.

Let $\psi$ be the proposition `The photon took path~A',
with the negation $\neg \psi$ denoting `The photon took path~B'; let
QM represent an axiomatization of quantum mechanics. Clearly,
$\psi$ is undecidable in QM (as will be explained shortly,
`measurement' will have to be part of the metatheory in NAFL and
not of the formalism). So in NAFL, the Main Postulate takes over
and the truth/falsity of $\psi$ is \emph{axiomatic} in nature; i.e.,
$\psi$ is true/false if and only if so asserted axiomatically in an
interpretation QM* of QM. In the absence of any such axiomatic
assertions, consistency of QM in NAFL demands that there \emph{must}
exist a non-classical model for QM in which $\psi$ is neither true
nor false. Whether
such a non-classical model can exist in the present available
formulations of QM is another matter; we assume that QM can be
`fixed' such that this is possible. Note that the superposition
does \emph{not} mean that `The photon took path~A and the photon
took path~B'; it only means that the photon took \emph{neither}
path~A nor path~B in the sense that neither of these alternatives
have been asserted axiomatically (ie., can be proved) in the
interpretation QM*. So NAFL confirms the Copenhagen interpretation
of quantum mechanics, rather than the many-worlds interpretation.

It is clear from this description that NAFL treats `measurement' as
precisely equivalent to an \emph{axiomatic declaration}
of truth, in the interpretation QM* (which resides in the human
mind). Since the notions of `axiomatic declaration', `interpretation'
and `model' are all part of the metatheory in NAFL, it follows that
`measurement' must also be outside the formalism~(QM). In NAFL, when
the human being makes a measurement, he/she simultaneously `sees' the
outcome and makes an axiomatic declaration of the observed outcome
in QM*. If the observer chooses to keep the axiomatic declarations in
tune with the observed outcomes, then there is a perfect correspondence
between such axiomatic declarations and measurement in the real world.
The assertion that one cannot measure $\psi \& \neg \psi$ is in
correspondence with the NAFL requirement that $\psi \& \neg \psi$
is not in the t-syntax of QM and so can never be formally asserted
as an axiom (i.e., the notion of `undecidability' is not formalizable
in NAFL).

It is also clear that NAFL does not assign any objective reality to
the concept of a photon as a `particle'. Indeed, if the photon were
to be fixed as a particle in the sense that we denote this term, then
$\psi \vee \neg \psi$ must unavoidably be an axiom of QM and hence
the NAFL version of QM will be inconsistent (since the non-classical
model required by metatheorem~2 of \cite{SR} cannot exist and also,
$\psi \vee \neg \psi$ is not even in the t-syntax of QM). So the
photon must be treated as having a non-constructive existence in
NAFL. The superposition $\psi \& \neg \psi$ in the non-classical
model only means that the human mind that inteprets QM has not
declared either $\psi$ or $\neg \psi$ axiomatically as true
in QM* (which proves neither of these propositions). This is certainly
true in the real world, provided, as observed earlier, QM* is
kept in tune with real-world measurements.

Note that NAFL correctly handles the temporal aspect of truth
in this experiment. The superposition $\psi \& \neg \psi$ applies
\emph{until} the measurement is actually made (in the detectors),
at which point the observer switches to either $\psi$ or
$\neg \psi$ as axiomatic declarations in QM* in accordance with
the measured result. Thus QM* is `dynamic' and will change in time
to suit real-world measurements/observations. Of course, NAFL
does not insist in general that real-world obervations
should be available or that QM* should be kept in tune with such
observations even if available. Suppose the experiment is started
at time $t=0$ and the outcome $\psi$ is observed at time $t=T$.
Does this mean that the photon `really' took path~A for $0 < t <T$?
Not in NAFL; NAFL can only tell us the real-world truth that
the photon was not \emph{observed/measured} to take either path~A
or path~B during $0 < t <T$. \emph{However}, the aposteriori
conclusion `At time $t \geq T$, I conclude that the photon took path~A
for $0 < t <T$' can certainly be formalized in NAFL. There is no
contradiction here because this conclusion is valid only
for $t \geq T$.

\subsubsection*{The Schr\"odinger cat experiment}
Let $\psi$ denote `The cat is alive' and $\neg \psi$ denote
`The cat is dead'. Again, $\psi$ is undecidable in QM. If the
experiment is started at $t=0$ and at $t=T$, say, $\psi$ is
observed, then $\psi \& \neg \psi$ is the case (in a non-classical
model for QM) for $0 < t < T$ and neither $\psi$ nor $\neg \psi$ is
provable in QM* for these times. For $t \geq T$, the observer declares
the observed result ($\psi$ in this case) axiomatically in QM*.
Once again, the aposteriori conclusion that the cat was `really'
alive for $0 < t < T$ can be reached and formalized only for
$t \geq T$; during the interval $0 < t < T$, NAFL only tells us the
real-world truth that the cat has not been \emph{observed} to be either
alive or dead.

\subsection{Two further examples of the NAFL concept of truth}
We discuss here the coin toss experiment and Aristotle's example
of `There will be a sea-battle tomorrow'. Let the theory
$\mbox{T}_0$ denote the null set of axioms.

\subsubsection*{The coin toss experiment}
Let the observer toss a coin and before the outcome is observed,
cover the coin, say, under the palm of his/her hand. Let $\psi$
stand for `The outcome is heads' and $\neg \psi$ for the
`The outcome is tails'. Again in NAFL, the superposition
$\psi \& \neg \psi$ is the case in a non-classical model for
$\mbox{T}_0$ until the outcome is actually observed to be either
heads or tails (at which time the observer makes the appropriate
axiomatic declaration in the interpretation T* of $\mbox{T}_0$).
Let $\phi$ stand for `The coin has landed flat under the palm
of the observer's hand'. The important point of this experiment is
that the observer \emph{knows} that $\phi$ is `true' in the real world.
But in NAFL, $\phi$ is not part of the t-syntax of $\mbox{T}_0$,
for clearly $\phi \Leftrightarrow \psi \vee \neg \psi$. But $\phi$
is legitimate in the p-syntax and the metatheory of $\mbox{T}_0$.
No matter how `real' $\phi$ seems to the observer, it cannot be
formalized as a proposition of $\mbox{T}_0$ in NAFL. Indeed, $\phi$
represents the conclusion that the observer will observe either
$\psi$ or $\neg \psi$ if he/she lifts the palm of his/her hand;
but in NAFL, `measurement' or `observation' is equivalent to
an axiomatic declaration of truth and so is part of the metatheory
and not formalizable, as discussed earlier.

\subsubsection*{Aristotle's sea-battle example}
Finally, consider Aristotle's example `There is/was/will be a sea-battle
on a specified date and time between two specified nations at a
specified location', where the appropriate tense is to be used
depending on the time at which the proposition is considered;
let $\psi$ formalize this proposition in the NAFL theory $\mbox{T}_0$.
The superposition will once again apply until the specified date and
time when the observation is made by the observer. The details are
similar to the previous examples. The interest in this example is
for the case when say, a disaster takes place wiping out the two
specified nations or the specified location prior to the specified
time and date. The proposition will clearly become meaningless in
classical logic. But in NAFL, the proposition can still be formalized;
it no longer applies to the real world. The superposition will continue
to apply because the observer will not have the chance to make any
real-world observations. Of course, the observer may make fictitious
declarations of truth in the interpretation T* of $\mbox{T}_0$ at
any given time.

\section{Concluding remarks}
In this paper, we have critically examined the concept of formalism
and concluded that it is only NAFL, and not either classical or
intuitionistic logic, that correctly embodies this concept. The
result is that much of classical infinitary reasoning becomes
invalid in consistent NAFL theories. Anything `stronger' than
the theory of finite sets F (or equivalently, Peano arithmetic)
discussed in Sec.~\ref{impl} will become inconsistent in NAFL.
Hence Hilbert's program has been settled negatively -- much of
classical infinitary reasoning stands refuted from the finitary
and formalistic standpoints. However, it is important to note
that in inconsistent NAFL theories, it is still not possible to
deduce \emph{any} proposition; this is in contrast to inconsistent
theories in classical/intuitionistic/constructive logics.
It is still possible to permit infinite sets, say, in the p-syntax of
F, to \emph{prove} results, such as FLT, in the t-syntax. However,
such a `proof' is not rigorous by NAFL standards. So can the proof
be trusted, i.e., is it true that we will never ever find a
counter-example to FLT? In general, the answer must be in the
negative; but nevertheless such inconsistent (by NAFL standards)
infinitary reasoning may still be useful and convenient in real
life, such as, in the case of the relativity theories. But while
many of the predictions of such inconsistent theories are valid
in the sense that they have been confirmed by experiment, \emph{all}
such predictions cannot be trusted in the absence of experimental
data. For example, did the Big Bang occur? Do black holes exist?
Will the universe shrink to a point as predicted by General Relativity?
Is time travel possible as predicted by General Relativity? Can
the concept of quantum computing be trusted? These are all questions
that can only be answered empirically by experiments. A useful
line of further research will be to see how infinite sets can be
admitted into NAFL theories without sacrificing consistency;
infinite sets, and quantification over infinitely many such sets
are very useful in real analysis. A second line of research would
be to abandon the concept of the continuum and look for a (possibly
very complicated) finitary, discrete description of nature in a
consistent NAFL theory in which \emph{everything}, including
space, time and matter, is quantized. This line of research is
suggested by the fact that the very process by which quantum
superposition is justified in NAFL is also responsible for the
rejection of the relativity theories in NAFL via the
constraint of consistency. Thus the suspected incompatibility
between quantum mechanics and the relativity theories
is clearly established in NAFL.

\section*{Dedication}
This paper is dedicated to my son R.~Anand and my wife R.~Jayanti.

\begin{thebibliography}{9}
\bibitem{SGS}
Simpson, Stephen~G.~2000. Logic and mathematics, in \emph{The Examined Life:
Readings from Western Philosophy from Plato to Kant}, edited by S.~Rosen,
Book-of-the-Month~Club. See also \\
http://www.math.psu.edu/simpson/papers/philmath/node20.html
\bibitem{Gd}
G\"odel, Kurt~1986. \emph{Collected Works}, Vol.~1, ed.~Feferman
\emph{et al}., Oxford University Press.
\bibitem{Sk}
Skolem, Thoralf~1934. \emph{Fundamenta Mathematicae}, Vol.~23,
pp.~150--161. Reprinted as 1934~b, pp.~355--366, in
Skolem,~Thoralf,~1970. \emph{Selected Works in Logic},
ed.~Jens~E.~Fenstad, Universitetsforlaget, Oslo.
\bibitem{SR}
Srinivasan, Radhakrishnan~2002. Quantum superposition justified
in a new non-Aristotelian finitary logic. PhilSci Archive, \\
http://philsci-archive.pitt.edu, Preprint ID Code~635.
\bibitem{Coh}
Cohen, Paul~J.~1966. \emph{Set theory and the continuum hypothesis}.
W.~A.~Benjamin, Inc., New York.
\bibitem{SRT}
Srinivasan, Radhakrishnan~2002. Inertial frames, special realativity
and consistency. PhilSci Archive, \\
http://philsci-archive.pitt.edu, Preprint ID Code~666.
\end{thebibliography}
\end{document}

