Formally expressing, and subsequently interpreting quantification constructively

[Bhupinder Singh Anand]

Apropos formally expressing, and subsequently interpreting quantification constructively, please permit me to share the following Abstract from my just published book (where I have cited some of your work as detailed in the Index):

The Significance of Evidence-based Reasoning in Mathematics, Mathematics Education, Philosophy, and the Natural Sciences

where I seek to distinguish between what is believed to be true, what can be evidenced as true, and what ought not to be believed as true.

ABSTRACT
In this recently concluded, multi-disciplinary, investigation, I address the 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 objectively evidencing such acceptance.

I then show how an evidence-based perspective of quantification in terms of:

• algorithmic verifiability, and
• algorithmic computability

admits evidence-based definitions of:

• well-definedness, and
• effective computability.

I further show how such a perspective yields two, unarguably constructive, interpretations of the first-order Peano Arithmetic PA—over the structure N of the natural numbers—that are complementary, not contradictory:

• The first yields the familiar, standard, weak interpretation I_PA(N, SV) of PA over N:

– which is well-defined with respect to assignments of algorithmically verifiable Tarskian truth values to the formulas of PA under I_PA(N, SV);

– and thus constitutes a constructively weak proof of consistency for PA.

• The second yields the hitherto unsuspected, finitary, strong interpretation I_PA(N, SC) of PA over N:

– which is well-defined with respect to assignments of algorithmically computable Tarskian truth values to the formulas of PA under I_PA(N, SC);

– and so constitutes a constructively strong proof of consistency for PA (as sought by Hilbert in his second ICM-1900 problem).

I situate my investigation within a broad analysis of quantification vis à vis:

• Hilbert’s ε-calculus
• Gödel’s ω-consistency
• The Law of the Excluded Middle
• Hilbert’s ω-Rule
• An Algorithmic ω-Rule
• Gentzen’s Rule of Infinite Induction
• Rosser’s Rule C
• Markov’s Principle
• The Church-Turing Thesis
• Aristotle’s particularisation
• Wittgenstein’s constructive mathematics
• Evidence-based quantification

By showing how these are formally inter-related, I highlight the fragility of both:

• the persisting, theistic, classical/Platonic interpretation of quantification grounded in Hilbert’s ε-calculus;

• the persisting, atheistic, constructive/Intuitionistic interpretation of quantification rooted in Brouwer’s mistaken belief that the Law of the Excluded Middle is non-finitary.

Sincerely,

Bhupinder Singh Anand