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.)

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

**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?"

...And that is how we know the Earth to be banana-shaped.

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

For a given formal system S, call problem A

The time complexity of A

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 B

_{S}: given a provable sentence of length n, find a proof.The time complexity of A

_{S}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 A_{S}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 B

_{S}: 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.)### Who is online

Users browsing this forum: No registered users and 7 guests