patternModerate
What is the complexity of theorem proving?
Viewed 0 times
provingthewhattheoremcomplexity
Problem
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.
Let me know if my question is wrong. Regards.
Solution
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).
-
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).
Context
StackExchange Computer Science Q#160164, answer score: 16
Revisions (0)
No revisions yet.