(Notations, non-standard concepts, and definitions used commonly in these investigations are detailed in this post.)
It is, indeed, gratifying that, after over 50 years of pursuing a path which challenged the accepted textbook wisdom that mathematical truth (which is the basis for asserting that any scientific proposition may be treated as true) is not definable objectively, my contrary contention has been accepted by the editors of the journal ‘Cognitive Systems Research‘ for publication in the December 2016 issue of the Journal. In a sense, this gives closure to the most challenging part of a journey which I have been privileged to afford and endure so far only because of the blessings, indulgence, and support provided by a generation of late elders (my teachers C. B. Nix James and Professor Manohar S. Huzurbazar, parents and mentors), contemporaries, and countless others who gave me the encouragement and strength to continue on such a nebulous path at crucial moments of my life. Defending the thesis promises to be as challenging—albeit far shorter—a journey!
In a paper The Truth Assignments That Differentiate Human Reasoning From Mechanistic Reasoning: The Evidence-Based Argument for Lucas’ Gödelian Thesis, due to appear in the December 2016 issue of Cognitive Systems Research, we briefly consider (Anand ) a philosophical challenge that arises when an intelligence—whether human or mechanistic—accepts arithmetical propositions as true under an interpretation—either axiomatically or on the basis of subjective self-evidence—without any specified methodology for evidencing such acceptance (for a brief, relatively recent, review of such challenges, see Feferman , Feferman ).
The ambiguity in the standard interpretation of the Peano Arithmetic PA
For instance conventional wisdom, whilst accepting Tarski’s classical definitions of the satisfiability and truth of the formulas of a formal language under an interpretation (Anand , p.44), postulates that under the classical standard interpretation (we shall refer to this henceforth as ) of the first-order Peano Arithmetic PA (we take this to be the first-order theory defined in any standard text corresponding to the theory S in Mendelson , p.102) over the domain of the natural numbers:
(i) The satisfiability/truth of the atomic formulas of PA can be assumed as uniquely decidable under ;
(ii) The PA axioms can be assumed to uniquely interpret as satisfied/true under ;
(iii) The PA rules of inference—Generalisation and Modus Ponens—can be assumed to uniquely preserve such satisfaction/truth under ;
(iv) Aristotle’s particularisation can be assumed to hold under .
We define Aristotle’s particularisation as the non-finitary assumption that an assertion such as, `There exists an such that holds’—usually denoted symbolically by `‘—can always be validly inferred in the classical logic of predicates from the assertion, `It is not the case that: for any given , does not hold’—usually denoted symbolically by `‘ (see also Hilbert & Ackermann , pp.58-59).
We argue that the seemingly innocent and self-evident assumptions of uniqueness in (i) to (iii)—as also the seemingly innocent assumption in (iv) which, despite being obviously non-finitary, is unquestioningly accepted in classical literature as equally self-evident under any logically unexceptionable interpretation of the classical first-order logic FOL—conceal an ambiguity with far-reaching consequences.
The two, hitherto unsuspected and essentially different, interpretations of PA
The ambiguity is revealed if we note that Tarski’s classic definitions permit both human and mechanistic intelligences to admit finitary evidence-based definitions of the satisfaction and truth of the atomic formulas of PA over the domain of the natural numbers in two, hitherto unsuspected and essentially different, ways:
(1a) In terms of classical algorithmic verifiabilty; and
(1b) In terms of finitary algorithmic computability.
By ‘finitary’ we mean that (for a brief review of ‘finitism’ and ‘constructivity’ in the context of this paper see Feferman ):
“… there should be an algorithm for deciding the truth or falsity of any mathematical statement”
We show that:
(2a) The two definitions correspond to two distinctly different assignments of satisfaction and truth to the compound formulas of PA over —say and (we shall refer to these henceforth as and respectively); where
(2b) The PA axioms are true over , and the PA rules of inference preserve truth over , under both and .
A finitary proof of consistency for Arithmetic: The solution to Hilbert’s Second Millenium Problem
We then show that:
(3a) If we assume the satisfaction and truth of the compound formulas of PA are always non-finitarily decidable under the assignment , then this assignment defines a non-finitary interpretation of PA in which Aristotle’s particularisation always holds over ; and which corresponds to the classical non-finitary standard interpretation of PA over the domain —from which only a human intelligence may non-finitarily conclude (as Gentzen’s argument does) that PA is consistent; whilst
(3b) The satisfaction and truth of the compound formulas of PA are always finitarily decidable under the assignment , which thus defines a finitary interpretation of PA—from which both intelligences may finitarily conclude that PA is consistent (as sought by David Hilbert for the second of the twenty three problems that he highlighted at the International Congress of Mathematicians in Paris in 1900; see Hilbert ).
PA is categorical and has no non-standard models
We show further that both intelligences would logically conclude that:
(4a) The assignment defines a subset of PA formulas that are algorithmically computable as true under the standard interpretation if, and only if, the formulas are PA provable;
(4b) PA is categorical (and so has no non-standard model, as argued in Anand );
We note that the standard argument to the contrary—as detailed, for instance, in Kaye  (pp.10-11)—violates finitarity by adding a new constant to the language of PA that is not definable in and, ipso facto, by adding an atomic formula to PA whose satisfaction under any interpretation of PA is not algorithmically verifiable.
However, since the atomic formulas of PA are algorithmically verifiable under the standard interpretation (Theorem 5.1, p. 38, in Anand ), the above argument invalidly postulates precisely that which it seeks to prove (as also do arguments in: Boolos, Burgess & Jeffrey , p.306, Corollary 25.3; Luna , p.7)!
There are no ‘undecidable’ arithmetical propositions: Gödel’s Theorems hold vacuously
Both intelligences would also logically conclude that:
(4c) PA is not -consistent.
(5a) Since PA is not -consistent, Gödel’s argument in Gödel  (p.28(2))—that “ is not -PROVABLE”—does not yield a `formally undecidable proposition’ in PA;
The reason we prefer to consider Gödel’s original argument (rather than any of its subsequent avatars) is that, for a purist, Gödel’s remarkably self-contained 1931 paper—it neither contained, nor needed, any formal citations—remains unsurpassed in mathematical literature for thoroughness, clarity, transparency and soundness of exposition—from first principles (thus avoiding any implicit mathematical or philosophical assumptions)—of his notion of arithmetical `undecidability’ as based on his Theorems VI and XI and their logical consequences.
We also note that if PA is not -consistent, then Aristotle’s particularisation does not hold in any finitary interpretation of PA over .
Now, J. Barkeley Rosser’s ‘undecidable’ arithmetical proposition in Rosser  is of the form .
Thus his ‘extension’ of Gödel’s proof of undecidability too does not yield a ‘formally undecidable proposition’ in PA, since it implicitly presumes that Aristotle’s particularisation holds when interpreting under a finitary interpretation over (Rosser , Theorem II, pp.233-234; Kleene , Theorem 29, pp.208-209; Mendelson , Proposition 3.32, pp.145-146).
(5b) The appropriate conclusion to be drawn from Gödel’s argument (in Gödel , p.27(1))—that “ is not -PROVABLE”—is thus not that there is a ‘formally undecidable arithmetical proposition’ (see also Feferman  for an interesting perspective on how he—as well as, reportedly, both Gödel and Hilbert—informally viewed the concept of ‘formally undecidable arithmetical propositions’) but that any such putatively ‘undecidable arithmetical proposition’ is an instantiation of the argument (corresponding to Cantor’s diagonal argument and Turing’s halting argument) that we can define number-theoretic formulas which are algorithmically verifiable as always true, but not algorithmically computable as always true.
The argument for Lucas’ Gödelian Thesis
We conclude from this that Lucas’ Gödelian argument can validly claim:
Thesis: There can be no mechanist model of human reasoning if the assignment can be treated as circumscribing the ambit of human reasoning about ‘true’ arithmetical propositions, and the assignment can be treated as circumscribing the ambit of mechanistic reasoning about ‘true’ arithmetical propositions.
Although Lucas’ original 1961 thesis (Lucas ):
“… we cannot hope ever to produce a machine that will be able to do all that a mind can do: we can never not even in principle, have a mechanical model of the mind.”
deserves consideration that lies beyond the immediate scope of this investigation, we draw attention to his informal 1996 defence of it from a philosophical perspective in Lucas , where he concludes with the argument that:
“Thus, though the Gödelian formula is not a very interesting formula to enunciate, the Gödelian argument argues strongly for creativity, first in ruling out any reductionist account of the mind that would show us to be, au fond, necessarily unoriginal automata, and secondly by proving that the conceptual space exists in which it is intelligible to speak of someone’s being creative, without having to hold that he must be either acting at random or else in accordance with an antecedently specifiable rule”.
Argument: Gödel has shown how to construct an arithmetical formula with a single variable—say (Gödel refers to this formula only by its Gödel number (Gödel , p.25(12)))—such that is not PA-provable, but is instantiationally PA-provable for any given PA numeral .
Hence, for any given numeral , Gödel’s primitive recursive relation must hold for some natural number (where denotes Gödel’s primitive recursive relation ‘ is the Gödel-number of a proof sequence in PA whose last term is the PA formula with Gödel-number ‘ (Gödel , p.22(45)); and denotes the Gödel-number of the PA formula ).
If we assume that any mechanical witness can only reason finitarily then although, for any given numeral , a mechanical witness can give evidence under the assignment that the PA formula holds in , no mechanical witness can conclude finitarily under the assignment that, for any given numeral , the PA formula holds in .
However, if we assume that a human witness can also reason non-finitarily, then a human witness can conclude under the assignment that, for any given numeral , the PA formula holds in .
 Bhupinder Singh Anand. 2016. The Truth Assignments That Differentiate Human Reasoning From Mechanistic Reasoning: The Evidence-Based Argument for Lucas’ Gödelian Thesis. To appear in Cognitive Systems Research. Volume 40, December 2016, Pages 35-45, doi:10.1016/j.cogsys.2016.02.004.
 Solomon Feferman. 2006. Are There Absolutely Unsolvable Problems? Gödel’s Dichotomy. In Philosophia Mathematica (2006) 14 (2): 134-152.
 Solomon Feferman. 2008. Lieber Herr Bernays!, Lieber Herr Gödel! Gödel on finitism, constructivity and Hilbert’s program. In the Special Issue: Gödel’s dialectica Interpretation of Dialectica, Volume 62, Issue 2, June 2008, pp. 245-290.
 Elliott Mendelson. 1964. Introduction to Mathematical Logic. Van Norstrand, Princeton.
 David Hilbert & Wilhelm Ackermann. 1928. Principles of Mathematical Logic. Translation of the second edition of the Grundzüge Der Theoretischen Logik. 1928. Springer, Berlin. 1950. Chelsea Publishing Company, New York.
 David Hilbert. 1900. Mathematical Problems. An address delivered before the International Congress of Mathematicians at Paris in 1900. Dr. Maby Winton Newson translated this address into English with the author’s permission for the Bulletin of the American Mathematical Society, 8 (1902), 437-479. An HTML version is accessible at http://aleph0.clarku.edu/~djoyce/hilbert/problems.html.
 Bhupinder Singh Anand. 2008. Can we really falsify truth by dictat?. In The Reasoner, Vol(2)1 pp. 7-8.
 Richard Kaye. 1991. Models of Peano Arithmetic. Oxford Logic Guides, 15. Oxford Science Publications. The Clarendon Press, Oxford University Press, New York, 1991.
 George S. Boolos, John P. Burgess, & Richard C. Jeffrey. 2003. Computability and Logic (4th ed). Cambridge University Press, Cambridge.
 Laureano Luna. 2008. On non-standard models of Peano Arithmetic. In The Reasoner, Vol(2)2 p. 7.
 Kurt Gödel. 1931. On formally undecidable propositions of Principia Mathematica and related systems I. Translated by Elliott Mendelson. In M. Davis (ed.). 1965. The Undecidable. Raven Press, New York.
 J. Barkley Rosser. 1936. Extensions of some Theorems of Gödel and Church. In M. Davis (ed.). 1965. The Undecidable. Raven Press, New York. Reprinted from The Journal of Symbolic Logic, Vol.1, pp.87-91.
 Stephen Cole Kleene. 1952. Introduction to Metamathematics. North Holland Publishing Company, Amsterdam.
 J. R. Lucas. 1961. Minds, Machines and Gödel. In Philosophy, XXXVI, 1961, pp.112-127; reprinted in The Modeling of Mind, Kenneth M.Sayre and Frederick J.Crosson, eds., Notre Dame Press, 1963, pp.269-270; and in Minds and Machines, ed. Alan Ross Anderson, Prentice-Hall, 1954, pp.43-59.
 J. R. Lucas. 1996. The Gödelian Argument: Turn Over the Page. A paper read at a BSPS conference in Oxford. Reproduced in 2003 as Series/Report no.: Etica & Politica / Ethics & Politics V (2003) 1, EUT Edizioni Università di Trieste, URI: http://hdl.handle.net/10077/5477.