# Are all theories able to embed a universal Turing machine equivalent to one another?

Both set theory and second-order arithmetic are general enough to embed any Turing machine including of course universal Turing machines (UTM). Since any theorem is provable via a UTM, why are the theories not equivalent?

Perhaps using an embedded UTM to prove a theorem outside the scope of set theory involves the use of the fantasy rule. Hence it can at best prove theorems as; assume $A$ then $A \to B$? Where $A$ is the program required to be run on the UTM to prove $B$.

• What is "the fantasy rule?" – Noah Schweber Jul 6 '17 at 14:22
• What do you mean when you say "any theorem is provable via a UTM"? – Alex Kruckman Jul 6 '17 at 14:32
• @Alex I mean this: A theorem is a well formed sentence of a theory that is provable using the axioms of the theory and its rules of inference by a effective method. Turing formalized the notion of an effective method to a Turing machine. Since a theorem is only provable via an effective method, it must be that the proof (if it exists) can be the output of an appropriately encoded Turing machine. – Alexandre H. Tremblay Jul 6 '17 at 14:42
• @Noah Fantasy Rule: If assuming $A$ to be a theorem leads to $B$ being a theorem, then $(A \to B)$ is a theorem. – Alexandre H. Tremblay Jul 6 '17 at 14:46
• @AlexandreH.Tremblay Do you just mean "if $T$ plus $A$ proves $B$, then $T$ proves $A\rightarrow B$ for any theory $T$ and sentences $A, B$"? If so, this isn't a "fantasy rule," it (and all reasonable variants I can think of) is the deduction theorem, and it has nothing to do with the problem you're having. – Noah Schweber Jul 6 '17 at 14:58

There are a few issues here. First of all, UTMs don't prove things. What a UTM can do is verify that a computable first-order theory proves something, and so theories capable of studying UTMs can prove instances of provability in other theories. So for instance, if $T$ is a computable first-order theory which proves a sentence $\varphi$, then ZFC proves "$T$ proves $\varphi$." Moreover, if we assume ZFC is "reasonably true" (= $\Sigma^0_1$-sound), then ZFC proves "$T$ proves $\varphi$" iff $T$ in fact proves $\varphi$.

(To see that the soundness assumption on ZFC is needed, think about the theory ZFC+$\neg$Con(ZFC) ...)

So we have to be careful in defining "equivalent" here. A reasonable choice here is to do two things. First, restrict attention to $\Sigma^0_1$-sound theories to avoid the issue above. Second, say that theories $T_1, T_2$ are equivalent if they each correctly simulate each other: when we code the expressions "$T_i$ proves $\varphi$" appropriately, we have that for each sentence $\varphi$, $T_i$ proves $\varphi$ iff $T_{3-i}$ proves "$T_i$ proves $\varphi$."

(Note that if we didn't restrict attention to $\Sigma^0_1$-sound theories, we'd have a counterexample to your guess: ZFC+$\neg$Con(ZFC) proves that ZFC proves everything, so doesn't correctly simulate ZFC.)

So your question can now be rephrased as:

Why can't ZFC prove "the second-order theory of arithmetic proves $\varphi$," whenever second-order arithmetic in fact proves $\varphi$?

The answer comes down to those all-important words "first-order" versus "second-order." First-order logic has a recursive and complete proof system: if $T$ is a computably enumerable theory, the set of first-order consequences of $T$ is also computably enumerable (and we can go from a computable enumeration of $T$ to a computable enumeration of its consequences uniformly). By a "first-order consequence" of $T$ I mean a first-order sentence true in every model of $T$. The fact that the consequence relation in first-order logic can be captured by looking at finite combinatorial objects in a computable way is usually what justifies our use of the word "proves:" it's not just that a sentence is a consequence of a theory, but we can even produce a thing convincing us that the sentence is a consequence of the theory.

By contrast, this fails wildly for second-order logic. Second-order logic isn't even compact, so the mere idea of a "proof" in the sense of a finite sequence of sentences verifying that a certain sentence is a consequence of a certain set of sentences breaks down. And as it happens, this difference extends into the computability-theoretic realm:

The set of second-order sentences true in every structure (= second-order consequences of the empty theory) is not recursively enumerable.

(In fact it's much worse: it's not even in the analytic hierarchy!)

As a special case of this:

The set of first-order sentences which are true in every model of the second-order theory of arithmetic (or rather, the unique-up-to-isomorphism model of the second-order theory of arithmetic) is not recursively enumerable.

(In fact, it isn't even in the arithmetic hierarchy!)

So the issue here is:

UTMs cannot capture the consequence relation in second-order logic, either in general or in the specific case of first-order consequences of the second-order theory of arithmetic.

Incidentally, there's a terminological subtlety here. The phrase "second-order arithmetic" is more commonly these days used to refer to the first-order theory Z$_2$, which consists of basic axioms about natural numbers and sets of natural numbers. The reason for this shift in terminology is that the second-order theory of arithmetic is so terrible, we almost never actually study it. But this does mean you might here contradictory statements - the resolution is that they mean different things by "second-order arithmetic, and explains why I've said "second-order theory of arithmetic" above.