- first order logic
- Turing machine
- ordinal analysis
- bounded Zermelo / MacLane set theory
- EFA / PRA / PA
- convention: ZFC / NBG
- reverse mathematics and ontological commitments
- de res / de dicto axioms
Those words are written on a 9 cm x 9 cm note in front of me. They encapsulate the different ways I could think of (at the moment I wrote them down) to justify belief in the consistency of (rather weak) formal systems. I wrote them down after reading Timothy Chow's expository article The Consistency of Arithmetic, which tries to address the problem of Convincing Edward Nelson that PA is consistent.
The typical ZFC justifications (like those from Maddy's Believing the Axioms) are absent above, but they had been already mentioned in a previous exchange with Chow:
In addition to the consistency line of defence related to Turing
machines, also the von Neumann cumulative hierarchy justification can be
Chow had challenged FOM researchers with Kripkenstein doubting rule-following. Part of my defence was:
If it would really show that, than it would indeed be a major
achievement. But then it should be clarified how it is different from
the skeptic denying any possibility to communicate meaning at all.
Bill Taylor's reaction that Kripkenstein
is no more convincing than Goodman's "paradox" about grue and bleen clarifies this, if we are willing to admit that Goodman is right. Goodman's "Fact, Fiction, and Forecast" was published shortly after Wittgenstein's "Philosophical Investigations," and successfully clarifies the part of rule-following doubt which resists refutation, at least refutation by pointing out that Turing machines nail down the meaning of rules. (Note that Conifold's answer also mentions rule-following doubt.)
Chow's article offers Gentzen's consistency proof (=ordinal analysis), Friedman's reversal from Bolzano–Weierstrass for ℚ (=reverse mathematics), and a trivial argument that can be formalized in ZFC (=convention: ZFC) as main proofs for consistency of PA, and a finite approximation to the consistency of PA as an alternative justification for the supposed arch formalist. (Nelson withdrew his claim that primitive recursive arithmetic is inconsistent, but the introduction by Sarah Jones Nelson and afterword by Sam Buss and Terence Tao to his two posthumously published works tell us that this was not the end of the story, and that he continued his project to show the inconsistency of arithmetic the very next day.)
Back to my words on that 9 cm x 9 cm note. Chow's trivial argument had confused me with respect to his own position, and I wrote them down while composing an email to him. I didn't use those words in the end, but we had a nice discussion. Using ZFC to formalize his trivial argument felt like a cheap opt-out to me. However, Chow pointed out that as long as he doesn't know anything about my "belief system", the best he can do is to rely on standard assumptions (which in math means ZFC). The dubious part of his trivial argument is:
Now let me ask if a first-order formula in the language of arithmetic (e.g., ∃y:y+y=x) defines a mathematical property of the integers. Again, the answer is so obviously yes that you must wonder if it's a trick question. But it's not a trick question. The answer is yes.
But is the answer obviously yes, because first-order formulas always define mathematical properties (i.e. also in set theory), or because the integers are somehow special? Chow answered that at least historically
a mathematical concept is legitimate provided that the language that we use to define the object is sufficiently precise. Before answering, he queried my beliefs with questions like
Do you believe that "halting" is a mathematical property of a Turing machine? My answer was yes.
However, I also indicated I am more critical about the same statement for oracle Turing machines. At least one would have to clarify which property going beyond computability is shared by the sets used as oracles. Maybe they are somehow "absolutely definable"? Those types of questions are investigated by recursion theory. The computable sets are Δ01, the limit computable sets are Δ02, the hyperarithmetic sets are Δ11. The hyperarithmetic sets are closely related to the Church-Kleene ordinal ω1CK, but Arithmetical transfinite recursion ATR0 proves Δ11-comprehension, even so its proof-theoretic ordinal is the Feferman–Schütte ordinal Γ0, which is smaller than ω1CK.
Determining the proof-theoretic ordinal of an axiom system is the subject of ordinal analysis. Dmytro Taranovsky talks on FOM about ordinal analysis, and recommends The Art of Ordinal Analysis as a base reference. Personal opinion: Ordinal analysis provides real justifications for mathematics, and it would be nice to understand why it can do that (philosophically speaking). Probably what it does is to boil down the implications of consistency of an axiomatic system to the bare bones on a level where it becomes possible to understand it intuitively. (And this intuition can still be wrong, thereby resolving the paradox how we can know anything nontrivial for certain.)
The words "bounded Zermelo / MacLane set theory", "EFA / PRA / PA", and "de res / de dicto axioms" were not discussed above. Even (full) second order arithmetic is still out of reach for ordinal analysis. Now "bounded Zermelo / MacLane set theory" correspond to (full) higher order logic in a certain sense (as well as many other independent axiom systems for mathematics), and has been defended in the early days: Frank P. Ramsey and Rudolf Carnap accepted the ban on explicit circularity, but argued against the ban on circular quantification. "EFA / PRA / PA" are related to the fact that if we use mathematics to justify mathematics, then it is a good idea to have base-systems allowing us to do mathematics in the first place. "de res / de dicto axioms" is about the difference between asserting the existence of a concrete object fully specified (de res), and the mere claim of existence (de dicto) without specifying any particular object (like the axiom of choice).