# What is the complexity of theorem proving?

I'm learning some computer science and mathematics by myself. I know that proving theorems in ZFC is undecidable in general, but, is there a formal way to express how complex it is? Is it as complex as the Halting Problem, i.e., knowing if a TM halts? Where can I learn more of this (subjects, books, articles)?

Let me know if my question is wrong. Regards.

• Only computable tasks have a complexity. If a statement is a theorem, finding a proof of it takes time at most exponential in the shortest proof's length, using the recursive enumeration @CalebStanford's answer mentions. Sec. 3.1 here discusses the potential implications of a polynomial-time solution.
– J.G.
Commented May 15, 2023 at 14:17

In general, the complexity of theorem proving in a particular logical system (such as ZFC) is recursively enumerable (RE), and is complete for this class -- that is, equally as hard as solving the halting problem. To see this, we can show a reduction both ways:

• First, to show that theorem proving is RE: the statements provable in any known logical system can be listed out recursively, by enumerating all the axioms and all the possible proofs from those axioms. (This applies to any theory where the axioms are recursively enumerable, which includes ZFC, Peano arithmetic (PA), first-order logic, and any other familiar logical system). Therefore, theorem proving reduces to the halting problem and is RE.

• Second, to show theorem proving is complete for the class RE, we can reduce the halting problem to theorem proving. For this, it requires that the logical system is sufficiently expressive to state and prove properties about Turing machines; for example, this is true for ZFC and PA. Additionally, the encoding of properties has to be faithful (doesn't prove anything false about natural numbers); technically, it should be either omega-consistent or arithmetically sound. These properties most likely hold for ZFC if it is consistent, and certainly hold for PA.

Then the way the reduction work is, given a Turing machine $$M$$, encode the property "$$M$$ halts" as a formula in ZFC. The formula says, roughly, "there exists a finite sequence of configurations of the tape and sequence of states of $$M$$ such that each pair of adjacent states are a valid transition of the Turing machine and the last state in the sequence is halting." It turns out we can express all of that in ZFC (or indeed, in PA). If $$M$$ halts, the formula is provable; and if $$M$$ does not halt, arithmetical soundness (or $$\omega$$-consistency) implies the formula is not provable. So this reduction shows that theorem proving is at least as hard as the halting problem.

It may be interesting to note that the facts we used in the above two reductions are exactly the requirements about a logic that are necessary for Gödel's incompleteness theorems to apply to that logic: i.e. (i) the logic's axioms must be recursively enumerable, and (ii) the logic must be strong enough to (faithfully) encode properties about arithmetic and Turing machines.

Finally, I will note that if either of (i) or (ii) does not hold, then we get a different situation. Typically, (i) holds in any reasonable logic; no one studies logics that are not recursively enumerable. But many researchers look at logics that are weaker than ZFC and PA, for which (ii) does not hold; for example, satisfiability in linear arithmetic, or satisfiability of Boolean formulas. For these, we get much weaker complexity than RE that is often not just decidable, but in PSPACE, or NP, or a similar complexity class. For more on this topic, you can read about automated theorem proving and satisfiability modulo theories (SMT).

• Thanks a lot! So, if I understood correctly, we can say that when Gödel's theorems apply to some logic, that logic can express "M halts". Also, I'm assuming that the sequence of valid states that "M halts" talks about is finite. Again, thanks a lot. I'll be researching about the RE complexity class. Commented May 14, 2023 at 0:53
• @OtakarMolnárLópez That's correct for both! Commented May 14, 2023 at 1:50
• Btw, the class RE (recursively enumerable) is just problems that can be reduced to the halting problem, i.e. are "easier than" or equally hard as the halting problem. Commented May 14, 2023 at 1:51
• I think it's interesting to consider the possibility that ZFC is inconsistent, or that it is consistent but arithmetically unsound. If it's inconsistent, then provability is, of course, decidable, because every statement is provable. If it's consistent but arithmetically unsound, then it may prove statements of the form "the Turing machine $M$ halts" for Turing machines $M$ that actually do not halt. In that case, can we still prove that the halting problem reduces to provability in ZFC? Commented May 15, 2023 at 10:36
• @TannerSwett Good catch, thanks!! Right, I'm assuming consistency of ZFC there -- actually slightly stronger, I'm assuming $\omega$-consistency or arithmetical soundness (roughly, doesn't prove anything false about natural numbers). I've updated the answer. Commented May 15, 2023 at 15:46