Aristotle’s particularisation: A grey area in our accepted foundational concepts
We shall now argue that what mathematics needs is not a new foundation, but a greater awareness of the nature of its existing foundations.
In particular, it is the thesis of these investigations that almost all of the unresolved philosophical issues in the foundations of mathematics reflect the fact that the nature and role of Aristotle’s particularisation is left implicit when it is postulated over infinite domains.
Perhaps that is the unintended consequence of ignoring Hilbert’s efforts to integrate the concept formally into first order logic by formally defining universal and existential quantification through the introduction of his -operator.
Semantic postulation of Aristotle’s particularisation
Aristotle’s particularisation (AP) is the postulation that from the negation of a universal we may always deduce the existence of a contrafactual.
(It is necessarily true over finite domains.)
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.
(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—or by the assumption that FOL is -consistent.)
Is the price of Aristotle’s particularisation too high?
If so, we shall argue that the price being asked for assuming AP implicitly—instead of explicitly as Hilbert had proposed—may be too high!
Partially because the assumption seems to effectively obscure the far-reaching consequences of the non-finitary nature of AP from immediate view in natural and formal deductive chains.
(And therefore of the first order logic FOL under the implicit assumption of Aristotle’s particularisation.)
For instance, as Carnap’s deduction of the Axiom of Choice in ZF illustrates, the non-finitary consequences of assuming AP over infinite domains becomes apparent when the underlying logic is taken as Hilbert’s -calculus instead of the classical first order logic FOL.
However, formal deductions apparently prefer to substitute—seemingly arbitrarily—the implicit assumption of AP in the underlying logic by the introduction of `contrived’ formal assumptions such as Gödel’s -consistency or Rosser’s Rule C.
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 .
Rosser’s Rule C
“Since the rule ‘If , then ‘ corresponds to a hypothetical act of choice, we shall call it the rule of choice, or more briefly, Rule C.”
… J. Barkley Rosser. Logic for Mathematicians. 1953. McGraw Hill Book Company Inc., New York.
Similarly natural deduction chains apparently prefer to substitute—again seemingly arbitrarily—the implicit assumption of AP in the underlying logic by admitting a Rule of Infinite Induction (transfinite induction).
More importantly, the price may be too high because the implicit assumption of Aristotle’s particularisation in the underlying logic has masked the fact that, without such assumption, FOL is finitarily consistent; and—as we note below—that mathematically significant finitary structures can be built upon it without assuming AP.
Evidence-Based Interpretations of PA
Some consequences of making the assumption of Aristotle’s particularisation explicit are highlighted in `Evidence-Based Interpretations of PA’ that was presented at the AISB/IACAP Turing 2012 conference in Birmingham last year.
We showed there that Tarski’s inductive definitions admit evidence-based interpretations of the first-order Peano Arithmetic PA which allow us to define the satisfaction and truth of the quantified formulas of PA constructively over the domain of the natural numbers in two essentially different ways:
In terms of algorithmic verifiabilty; and
In terms of algorithmic computability.
That there can be even one, let alone two, logically sound (one finitary and one non-finitary) assignments of satisfaction and truth certificates to both the atomic and compound formulas of PA had hitherto been unsuspected!
Definition: Algorithmically verifiable arithmetical truth
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 .
“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.
We show in the Birmingham paper (as we shall refer to it hereafter) 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.
Definition: Algorithmically computable arithmetical truth
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 .
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 show in the Birmingham paper 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.
We show in this paper that although every algorithmically computable relation is algorithmically verifiable, the converse is not true.
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 (as addressed in more detail in this paper) 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.
The finitarily sound algorithmic interpretation of PA over
We argued from the above distinction that the algorithmically computable PA-formulas can provide a finitarily sound algorithmic interpretation of PA over the domain of the natural numbers.
We showed, moreover, that this yields a finitary proof of consistency for PA—as demanded by the Second of Hilbert’s celebrated Twenty Three Problems.
The non-finitarily sound standard interpretation of PA over
On the other hand, the distinction also suggests that Gerhard Gentzen’s transfinite proof of consistency for PA corresponds to the argument that the algorithmically verifiable PA-formulas of PA provide a non-finitarily sound standard interpretation of PA over .
Moreover—as has been generally suspected (perhaps for the reason noted towards the end of this post)—the distinction also suggests why the standard interpretation cannot yield the finitary proof of consistency for PA as demanded by Hilbert.
The distinction between finitary and non-finitary arithmetical reasoning introduced in the Birmingham paper has far reaching consequences
In these pages we shall argue that the power of this simple distinction actually goes far beyond the immediate conclusions drawn in the Birmingham paper.
Reason: We can further constructively define an unambiguous distinction between finitary and non-finitary reasoning, at the level of first order logic itself, which shows that the two are both mutually inconsistent yet complementary!
As can be expected, such a distinction could have far-reaching consequences for the foundations of mathematics, logic and computabiity (which form the focus of the investigations in these pages).
We shall consider some of these in the next post.