Sergei Artemov --- On the Provability of Consistency.

Talk given on Wednesday May 15, 2019 at The Graduate Center.

Abstract: We revisit the foundational question concerning Peano arithmetic PA:

(1) can consistency of PA be established by means expressible in PA?

The usual answer to (1) is “No, by Gödel’s Second Incompleteness Theorem.” In that theorem (G2), Gödel used an arithmetization of contentual mathematical reasoning and established that the arithmetical formula representing PA-consistency is not derivable in PA. Applying G2 to (1), one makes use of the formalization thesis (FT):

FT: any proof by means expressible in PA admits Gödel’s arithmetization.
Historically, there has been no consensus on FT; Gödel (1931) and Hilbert (1934) argued against an even weaker version of FT with respect to finitary proofs, whereas von Neumann accepted it.

Note that the aforementioned negative answer to (1) is unwarranted: here is a counter-example to FT. Let Ind(F) denote the induction statement for an arithmetical formula F. The claim C, “for each formula F, Ind(F),” is directly provable by means of PA: given any F, argue by induction to establish Ind(F). However, C is not supported by any arithmetization as a single formula since PA is not finitely axiomatizable.

We provide a positive answer to (1). We offer a mathematical proof of PA-consistency,

No finite sequence of formulas is a PA-proof of 0=1,
by means expressible in PA, namely, by partial truth definitions. Naturally, this proof does not admit Gödel’s arithmetization either.

[LaureanoLuna]

55:30 His concern wrt the meaning of Con(PA) in nonstandard models is hard to make sense of; when we say PA does not prove its own consistency, we mean PA under its standard interpretation hence under such an interpretation of PA. Uninterpreted formulas don't state whatever they would state under every possible interpretation; they state nothing.

[LaureanoLuna]

See slide at 31:50. Artemov contradicts himself. He says that by Compactness (4) reduces to (5), which is true. He then states that (5) is stronger than (4); obviously, by that same Compactness he invokes they are equivalent. Certainly, he states the former as true on the assumption that proving something in PA is proving a formula but this assumption is obviously true since PA only proves formulas.

[LaureanoLuna]

However, he may have a point when he says that proving something in PA and proving something by means of PA are two different things and that finitary proof may coincide with the latter.