## What's the complexity of "proving a given theorem?"

A place to discuss the science of computers and programs, from algorithms to computability.

Formal proofs preferred.

Moderators: phlip, Moderators General, Prelates

Robert'); DROP TABLE *;
Posts: 730
Joined: Mon Sep 08, 2008 6:46 pm UTC
Location: in ur fieldz

### What's the complexity of "proving a given theorem?"

That is, given some formal system/language, and a sentence in tha language that can be assumed to be a valid theorem of the system, what is the time/space complexity of actually finding a proof of the sentence?

Obviously, the problem is somewhere within EXPTIME/EXPSPACE, since doing a brute-force search through the exponentially growing tree will eventually find the theorem. (Although since the tree is infinitely deep, this search has to be breadth-first, so it takes up an exponential amount of space as well, AFAIK) However, AFAIK this is also not an NP problem, because while verifying a provided proof is polynomial in length of the proof, the length of the proof doesn't scale in any readily definable way with the length of the proven theorem, i.e. verification can be exponential (or worse?) in the length of the theorem.

My intuition is that verifying a provided proof is easier than finding one from scratch, so whatever category this is in, it should have the NP-esque property of being easy to verify while hard to solve, which general EXPTIME problems don't have. However, it's not actually NP as mentioned. Any ideas where it actually falls?

(Another thought I had was that this is somehow a problem that resembles NP, but allows time polynomial in the length of the certificiate, rather than the final answer, but I couldn't work out how to formulate that without allowing "Ignore the certificate entirely and do a brute-force search" as a valid "verification" strategy.)
...And that is how we know the Earth to be banana-shaped.

jareds
Posts: 436
Joined: Wed Jan 03, 2007 3:56 pm UTC

### Re: What's the complexity of "proving a given theorem?"

For a given formal system S, call problem AS: given a provable sentence of length n, find a proof.

The time complexity of AS is not bounded by any computable function of n (unless S is very weak or inconsistent). Suppose the time complexity were bounded by a computable function f. Then there would exist an algorithm to decide whether or not a sentence of S was provable: Let the length of the sentence be n and check all proofs of length less than or equal to f(n). (The time complexity gives an upper bound on proof length because you can't output a proof of length m in less than m steps.) Therefore, if provability in S is undecidable, which it is for reasonably strong and consistent systems, the time complexity of AS is not bounded by any computable function.

In particular, since 2^2^n is computable, it is not in 2-EXPTIME and therefore not in EXPSPACE. As a side note, note that it is possible to create relatively short statements with very long proofs in strong and consistent systems.

You might be confusing the problem you posed with a different problem (or you might be assuming that proof lengths are bounded by an exponential function of the length of the statement proved). For a given formal system S, call problem BS: given a sentence with a proof of length n, find a proof. This is in NP: you guess and check the proof. (Or, for pedants, it's in FNP if proofs in S are checkable in P.)