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.

Explanatory comments

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.

Evidence

“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.

Aristotle’s particularisation

This holds that from an assertion such as:

‘It is not the case that: For any given x,\ P^{*}(x) does not hold’

usually denoted symbolically by ‘\neg(\forall x)\neg P^{*}(x)‘, we may always validly infer in the classical, Aristotlean, logic of predicates [1] that:

‘There exists an unspecified x such that P^{*}(x) holds’

usually denoted symbolically by ‘(\exists x)P^{*}(x)‘.

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 [\neg (\forall x) \neg F(x)] of a first order language S interprets as true under a sound interpretation of S, then we may always conclude that there must be some object s in the domain D of the interpretation such that, if the formula [F(x)] interprets as the unary relation F^{*}(x) in D, then the proposition F^{*}(s) 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 ‘[(\exists x)P(x)]‘ is an abbreviation for the formula ‘[\neg(\forall x)\neg P(x)]‘.

The commonly accepted interpretation of this formula—and a fundamental tenet of classical logic unrestrictedly adopted as intuitively obvious by standard literature [2] 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 [3] 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 ‘[P(x)]‘ of a formal Arithmetical language interprets as an arithmetical relation denoted by ‘P^{*}(x)‘, and the formula ‘[\neg(\forall x)\neg P(x)]‘ as the arithmetical proposition denoted by ‘\neg(\forall x)\neg P^{*}(x)‘, the formula ‘[(\exists x)P(x)]‘ need not interpret as the arithmetical proposition denoted by the usual abbreviation ‘(\exists x)P^{*}(x)‘; and that such postulation is invalid as a general logical principle in the absence of a means for constructing some putative object a for which the proposition P^{*}(a) holds in the domain of the interpretation.

Hence we shall follow the convention that the assumption that ‘(\exists x)P^{*}(x)‘ is the intended interpretation of the formula ‘[(\exists x)P(x)]‘—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 \omega-consistency [4] as an explicit assumption in his formal reasoning in his seminal 1931 paper on formally undecidable arithmetical propositions [5].

Gödel explained at some length [6] that his reasons for introducing \omega-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 \omega-consistent if, and only if, Aristotle’s particularisation holds under the standard interpretation of PA [7].

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 \omega-consistent.

The structure \mathbb{N}

The structure of the natural numbers—namely:

N (the set of natural numbers);

= (equality);

S (the successor function);

+ (the addition function);

\ast (the product function);

0 (the null element).

The axioms of the first-order Peano Arithmetic PA

PA_{1}: [(x_{1} = x_{2}) \rightarrow ((x_{1} = x_{3}) \rightarrow (x_{2} = x_{3}))];

PA_{2}: [(x_{1} = x_{2}) \rightarrow (x_{1}^{\prime} = x_{2}^{\prime})];

PA_{3}: [0 \neq x_{1}^{\prime}];

PA_{4}: [(x_{1}^{\prime} = x_{2}^{\prime}) \rightarrow (x_{1} = x_{2})];

PA_{5}: [( x_{1} + 0) = x_{1}];

PA_{6}: [(x_{1} + x_{2}^{\prime}) = (x_{1} + x_{2})^{\prime}];

PA_{7}: [( x_{1} \star 0) = 0];

PA_{8}: [( x_{1} \star x_{2}^{\prime}) = ((x_{1} \star x_{2}) + x_{1})];

PA_{9}: For any well-formed formula [F(x)] of PA:

[F(0) \rightarrow (((\forall x)(F(x) \rightarrow F(x^{\prime}))) \rightarrow (\forall x)F(x))].

Generalisation in PA

If [A] is PA-provable, then so is [(\forall x)A].

Modus Ponens in PA

If [A] and [A \rightarrow B] are PA-provable, then so is [B].

The standard interpretation of PA

The standard interpretation \mathcal{I}_{PA(\mathbb{N},\ Standard)} of PA over the structure \mathbb{N} is the one in which the logical constants have their ‘usual’ interpretations [8] in Aristotle’s logic of predicates (which subsumes Aristotle’s particularisation), and [9]:

(a) the set of non-negative integers is the domain;

(b) the symbol [0] interprets as the integer 0;

(c) the symbol [S] interprets as the successor operation (addition of 1);

(d) the symbols [+] and [*] interpret as ordinary addition and multiplication;

(e) the symbol [=] interprets as the identity relation.

Simple consistency

A formal system S is simply consistent if, and only if, there is no S-formula [F(x)] for which both [(\forall x)F(x)] and [\neg(\forall x)F(x)] are S-provable.

\omega-consistency

A formal system S is \omega-consistent if, and only if, there is no S-formula [F(x)] for which first [\neg(\forall x)F(x)] is S-provable, and second [F(a)] is S-provable for any given S-term [a].

Soundness (formal system – non-standard)

A formal system S is sound under an interpretation \mathcal{I}_{S} with respect to a domain \mathbb{D} if, and only if, every theorem [T] of S translates as ‘[T] is true under \mathcal{I}_{S} in \mathbb{D}‘.

Soundness (interpretation – non-standard)

An interpretation \mathcal{I}_{S} of a formal system S is sound with respect to a domain \mathbb{D} if, and only if, S is sound under the interpretation \mathcal{I}_{S} over the domain \mathbb{D}.

Soundness in classical logic

In classical logic, a formal system S 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 [10] of the formal system.

This definition suffers, however, from an implicit circularity: the formal logic L underlying any interpretation of S 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 L_{1} and L_{2} are implicitly assumed to be sound, S+L_{1} is sound, but S+L_{2} is not.

Moreover, an interpretation of S is now a model for S if, and only if, it is sound.

Algorithmic verifiability

A number-theoretical relation F(x) is algorithmically verifiable if, and only if, for any given natural number n, there is an algorithm AL_{(F,\ n)} which can provide objective evidence for deciding the truth/falsity of each proposition in the finite sequence \{F(1), F(2), \ldots, F(n)\}.

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 \mathbb{N} if, and only if, they are algorithmically verifiable under the interpretation. [11]

Algorithmic computability

A number theoretical relation F(x) is algorithmically computable if, and only if, there is an algorithm AL_{F} that can provide objective evidence for deciding the truth/falsity of each proposition in the denumerable sequence \{F(1), F(2), \ldots\}.

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 \mathbb{N} if, and only if, they are algorithmically computable under the interpretation. [12]

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 [13], 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 [14]—and not only to a mathematically definable limit—if and only if such representation is definable by an algorithmically computable function. [15]

We note that although every algorithmically computable relation is algorithmically verifiable, the converse is not true. [16]

References

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 EPR 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.\

Notes

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 \omega-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 \mathbb{N}.

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 \mathbb{N}; 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?.

Author’s working archives & abstracts of investigations

Bhupinder Singh Anand