Use of square brackets
Unless otherwise obvious from the context, we use square brackets to indicate that the contents represent a symbol or a formula—of a formal theory—generally assumed to be well-formed unless otherwise indicated by the context.
In other words, expressions inside the square brackets are to be only viewed syntactically as juxtaposition of symbols that are to be formed and manipulated upon strictly in accordance with specific rules for such formation and manipulation—in the manner of a mechanical or electronic device—without any regards to what the symbolism might represent semantically under an interpretation that gives them meaning.
Use of an asterisk
Unless otherwise obvious from the context, we use an asterisk to indicate that the associated expression is to be interpreted semantically with respect to some well-defined interpretation.
We have taken some liberty in emphasising standard definitions selectively, and interspersing our arguments liberally with comments and references, generally of a foundational nature.
These are intended to reflect our underlying thesis that essentially arithmetical problems appear more natural when expressed—and viewed—within an arithmetical perspective of an interpretation of PA that appeals to the evidence provided by a deterministic algorithm.
Since a deterministic algorithm has only one possible move from a given configuration such a perspective, by its very nature, cannot appeal implicitly to transfinite concepts.
“It is by now folklore … that one can view the values of a simple functional language as specifying evidence for propositions in a constructive logic …”
… Chetan R. Murthy. 1991. An Evaluation Semantics for Classical Proofs. Proceedings of Sixth IEEE Symposium on Logic in Computer Science, pp. 96-109, (also Cornell TR 91-1213), 1991.
This holds that from an assertion such as:
‘It is not the case that: For any given does not hold’
usually denoted symbolically by ‘‘, we may always validly infer in the classical, Aristotlean, logic of predicates  that:
‘There exists an unspecified such that holds’
usually denoted symbolically by ‘‘.
Aristotle’s particularisation (AP) is essentially the semantic postulation that from the negation of a universal we may always deduce the existence of a contrafactual. It is necessarily true over finite domains.
Expressed more formally:
Aristotle’s particularisation under an interpretation
If the formula of a first order language interprets as true under a sound interpretation of , then we may always conclude that there must be some object in the domain of the interpretation such that, if the formula interprets as the unary relation in , then the proposition is true under the interpretation.
The significance of Aristotle’s particularisation for the first-order predicate calculus
We note that in a formal language the formula ‘‘ is an abbreviation for the formula ‘‘.
The commonly accepted interpretation of this formula—and a fundamental tenet of classical logic unrestrictedly adopted as intuitively obvious by standard literature  that seeks to build upon the formal first-order predicate calculus—tacitly appeals to Aristotlean particularisation.
However, L. E. J. Brouwer had noted in his seminal 1908 paper on the unreliability of logical principles  that the commonly accepted interpretation of this formula is ambiguous if interpretation is intended over an infinite domain.
Brouwer essentially argued that, even supposing the formula ‘‘ of a formal Arithmetical language interprets as an arithmetical relation denoted by ‘‘, and the formula ‘‘ as the arithmetical proposition denoted by ‘‘, the formula ‘‘ need not interpret as the arithmetical proposition denoted by the usual abbreviation ‘‘; and that such postulation is invalid as a general logical principle in the absence of a means for constructing some putative object for which the proposition holds in the domain of the interpretation.
Hence we shall follow the convention that the assumption that ‘‘ is the intended interpretation of the formula ‘‘—which is essentially the assumption that Aristotle’s particularisation holds over the domain of the interpretation—must always be explicit.
The significance of Aristotle’s particularisation for PA
In order to avoid intuitionistic objections to his reasoning, Kurt Gödel introduced the syntactic property of -consistency  as an explicit assumption in his formal reasoning in his seminal 1931 paper on formally undecidable arithmetical propositions .
Gödel explained at some length  that his reasons for introducing -consistency explicitly was to avoid appealing to the semantic concept of classical arithmetical truth in Aristotle’s logic of predicates (which presumes Aristotle’s particularisation).
The two concepts are meta-mathematically equivalent in the sense that, if PA is consistent, then PA is -consistent if, and only if, Aristotle’s particularisation holds under the standard interpretation of PA .
We note that Aristotle’s particularisation is a non-constructive—and logically fragile—semantic deduction rule. It is reflected in classical first order deduction either by some similarly non-constructive syntactic rule of natural deduction—such as Rosser’s Rule C [7.1]—or by the assumption that FOL is -consistent.
The structure of the natural numbers—namely:
(the set of natural numbers);
(the successor function);
(the addition function);
(the product function);
(the null element).
The axioms of the first-order Peano Arithmetic PA
: For any well-formed formula of PA:
Generalisation in PA
If is PA-provable, then so is .
Modus Ponens in PA
If and are PA-provable, then so is .
The standard interpretation of PA
The standard interpretation of PA over the structure is the one in which the logical constants have their ‘usual’ interpretations  in Aristotle’s logic of predicates (which subsumes Aristotle’s particularisation), and :
(a) the set of non-negative integers is the domain;
(b) the symbol interprets as the integer ;
(c) the symbol interprets as the successor operation (addition of );
(d) the symbols and interpret as ordinary addition and multiplication;
(e) the symbol interprets as the identity relation.
A formal system S is simply consistent if, and only if, there is no S-formula for which both and are S-provable.
A formal system S is -consistent if, and only if, there is no S-formula for which first is S-provable, and second is S-provable for any given S-term .
Soundness (formal system – non-standard)
A formal system S is sound under an interpretation with respect to a domain if, and only if, every theorem of S translates as ‘ is true under in ‘.
Soundness (interpretation – non-standard)
An interpretation of a formal system S is sound with respect to a domain if, and only if, S is sound under the interpretation over the domain .
Soundness in classical logic
In classical logic, a formal system is sometimes defined as ‘sound’ if, and only if, it has an interpretation; and an interpretation is defined as the assignment of meanings to the symbols, and truth-values to the sentences, of the formal system. Moreover, any such interpretation is defined as a model  of the formal system.
This definition suffers, however, from an implicit circularity: the formal logic underlying any interpretation of is implicitly assumed to be ‘sound’.
The above definitions seek to avoid this implicit circularity by delinking the defined ‘soundness’ of a formal system under an interpretation from the implicit ‘soundness’ of the formal logic underlying the interpretation.
This admits the case where, even if and are implicitly assumed to be sound, is sound, but is not.
Moreover, an interpretation of is now a model for if, and only if, it is sound.
A number-theoretical relation is algorithmically verifiable if, and only if, for any given natural number , there is an algorithm which can provide objective evidence for deciding the truth/falsity of each proposition in the finite sequence .
Tarskian interpretation of an arithmetical language verifiably in terms of the computations of a simple functional language
We show in the Birmingham paper that the ‘algorithmic verifiability’ of the formulas of a formal language which contain logical constants can be inductively defined under an interpretation in terms of the ‘algorithmic verifiability’ of the interpretations of the atomic formulas of the language; further, that the PA-formulas are decidable under the standard interpretation of PA over if, and only if, they are algorithmically verifiable under the interpretation. 
A number theoretical relation is algorithmically computable if, and only if, there is an algorithm that can provide objective evidence for deciding the truth/falsity of each proposition in the denumerable sequence .
Tarskian interpretation of an arithmetical language algorithmically in terms of the computations of a simple functional language
We show in the Birmingham paper that the ‘algorithmic computability’ of the formulas of a formal language which contain logical constants can also be inductively defined under an interpretation in terms of the ‘algorithmic computability’ of the interpretations of the atomic formulas of the language; further, that the PA-formulas are decidable under an algorithmic interpretation of PA over if, and only if, they are algorithmically computable under the interpretation. 
Algorithmic verifiability vis à vis algorithmic computability
We note that algorithmic computability implies the existence of an algorithm that can decide the truth/falsity of each proposition in a well-defined denumerable sequence of propositions , whereas algorithmic verifiability does not imply the existence of an algorithm that can decide the truth/falsity of each proposition in a well-defined denumerable sequence of propositions.
From the point of view of a finitary mathematical philosophy—which is the constraint within which an applied science ought to ideally operate—the significant difference between the two concepts could be expressed by saying that we may treat the decimal representation of a real number as corresponding to a physically measurable limit —and not only to a mathematically definable limit—if and only if such representation is definable by an algorithmically computable function. 
We note that although every algorithmically computable relation is algorithmically verifiable, the converse is not true. 
Be59 Evert W. Beth. 1959. The Foundations of Mathematics. Studies in Logic and the Foundations of Mathematics. Edited by L. E. J. Brouwer, E. W. Beth, A. Heyting. 1959. North Holland Publishing Company, Amsterdam.
BBJ03 George S. Boolos, John P. Burgess, Richard C. Jeffrey. 2003. Computability and Logic. (4th ed). Cambridge University Press, Cambridge.
BF58 Paul Bernays and Abraham A. Fraenkel. 1958. Axiomatic Set Theory Studies in Logic and the Foundations of Mathematics. Edited by L. E. J. Brouwer, E. W. Beth, A. Heyting. 1959. North Holland Publishing Company, Amsterdam.
Br08 L. E. J. Brouwer. 1908. The Unreliability of the Logical Principles. English translation in A. Heyting, Ed. L. E. J. Brouwer: Collected Works 1: Philosophy and Foundations of Mathematics. Amsterdam: North Holland / New York: American Elsevier (1975): pp.107-111.
Co66 Paul J. Cohen. 1966. Set Theory and the Continuum Hypothesis. (Lecture notes given at Harvard University, Spring 1965) W. A. Benjamin, Inc., New York.
Da82 Martin Davis. 1958. Computability and Unsolvability. 1982 ed. Dover Publications, Inc., New York.
EC89 Richard L. Epstein, Walter A. Carnielli. 1989. Computability: Computable Functions, Logic, and the Foundations of Mathematics. Wadsworth & Brooks, California.
Go31 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. pp.5-38.
HA28 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.
Hi25 David Hilbert. 1925. On the Infinite. Text of an address delivered in Münster on 4th June 1925 at a meeting of the Westphalian Mathematical Society. In Jean van Heijenoort. 1967. Ed. From Frege to Gödel: A source book in Mathematical Logic, 1878 – 1931. Harvard University Press, Cambridge, Massachusetts.
Kl52 Stephen Cole Kleene. 1952. Introduction to Metamathematics. North Holland Publishing Company, Amsterdam.
Kn63 G. T. Kneebone. 1963. Mathematical Logic and the Foundations of Mathematics: An Introductory Survey. D. Van Norstrand Company Limited, London.
Li64 A. H. Lightstone. 1964. The Axiomatic Method. Prentice Hall, NJ.
Me64 Elliott Mendelson. 1964. Introduction to Mathematical Logic. Van Norstrand. pp.145-146.
Mu91 Chetan R. Murthy. 1991. An Evaluation Semantics for Classical Proofs. Proceedings of Sixth IEEE Symposium on Logic in Computer Science, pp. 96-109, (also Cornell TR 91-1213), 1991.
Nv64 P. S. Novikov. 1964. Elements of Mathematical Logic. Oliver & Boyd, Edinburgh and London.
Qu63 Willard Van Orman Quine. 1963. Set Theory and its Logic. Harvard University Press, Cambridge, Massachusette.
Rg87 Hartley Rogers Jr. 1987. Theory of Recursive Functions and Effective Computability. MIT Press, Cambridge, Massachusetts.
Ro53 J. Barkley Rosser. 1953. Logic for Mathematicians. McGraw Hill, New York.
Sh67 Joseph R. Shoenfield. 1967. Mathematical Logic. Reprinted 2001. A. K. Peters Ltd., Massachusetts.
Sk28 Thoralf Skolem. 1928. On Mathematical Logic. Text of a lecture delivered on 22nd October 1928 before the Norwegian Mathematical Association. In Jean van Heijenoort. 1967. Ed. From Frege to Gödel: A source book in Mathematical Logic, 1878 – 1931. Harvard University Press, Cambridge, Massachusetts.
Sm92 Raymond M. Smullyan. 1992. Gödel’s Incompleteness Theorems. Oxford University Press, Inc., New York.
Su60 Patrick Suppes. 1960. Axiomatic Set Theory. Van Norstrand, Princeton.
Tu36 Alan Turing. 1936. On computable numbers, with an application to the Entscheidungsproblem. In M. Davis (ed.). 1965. The Undecidable. Raven Press, New York. Reprinted from the Proceedings of the London Mathematical Society, ser. 2. vol. 42 (1936-7), pp.230-265; corrections, Ibid, vol 43 (1937) pp. 544-546.
Wa63 Hao Wang. 1963. A survey of Mathematical Logic. North Holland Publishing Company, Amsterdam.
An12 Bhupinder Singh Anand. 2012. Evidence-Based Interpretations of PA. In Proceedings of the Symposium on Computational Philosophy at the AISB/IACAP World Congress 2012-Alan Turing 2012, 2-6 July 2012, University of Birmingham, Birmingham, UK.
An13 … 2013. A suggested mathematical perspective for the argument. Presented on 7’th April at the workshop on `Logical Quantum Structures‘ at UNILOG’2013, 4’th World Congress and School on Universal Logic, 29’th March 2013 – 7’th April 2013, Rio de Janeiro, Brazil.\
Return to 1: HA28, pp.58-59.
Return to 2: Hi25, p.382; HA28, p.48; Sk28, p.515; Go31, p.32.; Kl52, p.169; Ro53, p.90; BF58, p.46; Be59, pp.178 & 218; Su60, p.3; Wa63, p.314-315; Qu63, pp.12-13; Kn63, p.60; Co66, p.4; Me64, p.52(ii); Nv64, p.92; Li64, p.33; Sh67, p.13; Da82, p.xxv; Rg87, p.xvii; EC89, p.174; Mu91; Sm92, p.18, Ex.3; BBJ03, p.102.
Return to 3: Br08.
Return to 4: The significance of -consistency for the formal system PA is highlighted in An12.
Return to 5: Go31, p.23 and p.28.
Return to 6: In his introduction on p.9 of Go31.
Return to 7: For details see An12.
Return to 7.1: See Ro53, pp.127-136.
Return to 8: See Me64, p.49.
Return to 9: See Me64, p.107.
Return to 10: We follow the definition in Me64, p.51.
Return to 11: We show in An12 that the concept of Algorithmic verifiability is also well-defined under the standard interpretation of PA over .
Return to 12: We show in An12 that the concepts of Algorithmic verifiability and Algorithmic computability are both well-defined under the standard interpretation of PA over ; moreover they identify distinctly different subsets of the well-defined PA formulas.
Return to 13: We note that the concept of ‘algorithmic computability’ is essentially an expression of the more rigorously defined concept of ‘realizability’ in Kl52, p.503.
Return to 14: In the sense of a physically ‘completable’ infinite sequence (as needed to resolve Zeno’s paradox).
Return to 15: This point is addressed in more detail in An13.
Return to 16: See Appendix B of this preprint Is Gödel’s undecidable proposition an ‘ad hoc’ anomaly?.