Clarification of Gödel's second incompleteness theorem

Question

I am sorry for the following question, because the actual answer to this question is in the beautiful works of Feferman and Jeroslow, but, unfortunately, I havn't any time to go into that specific field right now and maybe some of you is aware of the answer.

The situation with Gödel's second incompleteness theorem is quite delicate. Let Pf(a, b) means that a is the Gödel number of proof of statement with Gödel number b and Neg(a, b) means that b is the Gödel number of negation of statement with Gödel number a. The main result of Gödel's work is representability of predicates Pf and Neg in formal arithmetic. Knowing that, we can define the Consistency of formal arithmetic in formal arithmetic as follows:

" it is not the case that there exist a statement A such that A and (not) A are provable in formal arithmetic " or in the language of formal arithmetic:

$$\forall x_1, x_2, x_3, x_4 [\neg (\operatorname{Pf}(x_1, x_3) \wedge \operatorname{Pf}(x_2, x_4) \wedge \operatorname{Neg}(x_3, x_4))].$$

Let's denote last proposition by W. Gödel's second incompleteness theorem says that W is not provable in formal arithmetic, i. e. the consistency of formal arithmetic is not provable in formal arithmetic. But Solomon Feferman in his remarkable paper of 1960 "Arithmetization of metamathematics in general setting" have found other formalization of consistency of formal arithmetic W' that is provable in formal arithmetic (see notes by E. Mendelson to the second theorem in formal arithmetic chapter of his "Intoduction to Mathematical logic"). Jeroslow ("Consistency statements in formal theories"), thereafter, studied consistency statements in a broader way.

Can someone explain the nature of W'? (obviously, $W\Leftrightarrow W'$ can not be proven in PA).

Can we interpret the provability of W' as the proof of consistency of formal arithmetic in formal arithmetic?

How well are various consistency statements grasped today?

Thanks in advance.

Answer 1

The key idea Feferman is exploiting is that there can be two different enumerations of the axioms of a theory, so that the theory does not prove that the two enumerations give the same theory.

Here is an example. Let $A$ be a set of the axioms defined by some formula $\phi(n)$ (that is, $\phi(x)$ holds for exactly those $x$ that are in $A$). Define a new formula $\psi(n)$ like so:

$\psi(n) \equiv \phi(n) \land \text{Con}( \langle x \leq n : \phi(x)\rangle)$

Where Con(σ) is a formula which says that no contradiction is provable from the axioms listed in the sequence σ.

In the case where $A$ is the set of axioms for a suitable consistent theory $T$ that satisfies the second incompleteness theorem, the following hold:

(1) In the standard model, we have $\phi(n) \Leftrightarrow \psi(n)$ for all $n$, because $T$ really is consistent.

(2) T does not prove that $\phi(n) \Leftrightarrow \psi(n)$ for all $n$, because this equivalence implies that T is consistent.

(3) If we use $\psi$ to define a formula Con_ψ(T), then T will prove (under the assumption that the empty theory is consistent, if this is not provable in T) that the theory defined by ψ is consistent. However, T will not prove Con_φ(T), which is the usual consistency sentence for T.

This kind of example is presented in a more precise way in Feferman's 1960 paper that you mentioned, along with precise hypotheses on the theory and sharper results.

My opinion is that we cannot regard a proof of Con_ψ(T) as a proof of the consistency of T, because although φ and ψ are extensionally identical, they do not intensionally represent the same theory. Feferman expresses a similar idea on his p. 69. Of course, this is a matter of philosophy or interpretation rather than a formal mathematical question.

---

Addendum

The difference between extensional and intensional equality is easiest to explain by example. Let A be the empty set and let B be the set of integers larger than 1 that do not have a unique prime factorization. Then we know B is also the empty set: so A and B are extensionally equal. But the definition of B is much different than the definition of A: so A and B are intensionally different.

This distinction is often important in contexts like computability and formal logic where the things that you work with are actually definitions (also called codes, indices, Gödel numbers, or notations) rather than the objects being defined. In many cases, extensional equality is problematic, because of computability or effectiveness problems. For example, in my answer above, we know that φ and ψ define the same set in the real world, but this fact requires proof, and that proof may be impossible in the object theory we are dealing with. On the other hand, intensional equality is easy to decide, provided you are working directly with definitions.

Answer 2

Reading between the lines, I think your question may be answered in David Auerbach's article "How to Say Things With Formalisms." Regarding whether these exotic "consistency" statements may be interpreted as "expressing" consistency, I would say that the answer is no. The crux of the matter may be put more simply. Let's suppose we want to express "$x$ is even" in the first-order language of arithmetic. A natural attempt is $\exists y: y+y=x$. However, you could be sneaky and try something like $\exists y: [y+y=x \wedge \neg G(y,"1=0")]$ where $G(a,b)$ says "$a$ is not the Goedel number of a proof of $b$." If the theory in question is consistent then your exotic evenness predicate will be true of precisely the even integers. However, it's pretty clear that there's something fishy about this predicate. It doesn't really say only that $x$ is even; it says that $x$ is even and $x/2$ doesn't witness a proof of a contradiction. Similarly, the exotic consistency predicates don't just say that the theory is consistent.

The issue is necessarily somewhat philosophical and not strictly mathematical, because when deciding whether $\exists y: y+y=x$ correctly "expresses" the statement that $x$ is even, we have to resort to our informal understanding of what it really means for $x$ to be even. But any reasonable person would agree that $\exists y: y+y=x$ is the right way to express "$x$ is even" and not the exotic alternative above. Similarly, when deciding whether a consistency predicate correctly expresses what we really mean by consistency, we have to look at each step of the construction and check that all the formalizations are "reasonable." If someone digs in their heels and insists that the exotic predicate is the reasonable one then it's impossible to prove them wrong; however, any reasonable person can see that the standard consistency predicate is the right one.