Consider the language of PROOFS. This language is the language of all ordered pairs of ZFC propositions T and unary strings S of all 1’s s.t. there exists a ZFC proof of T of length |S| or less.

PROOF OUTLINE:

1 – ZFC is consistent –> PROOFS is NP-complete

2 – ZFC is inconsistent –> PROOFS is in P

3 – PROOFS is not in P –> ZFC is consistent

4 – ZFC is consistent –> (PROOFS is not in P) is unprovable

1 – ZFC is consistent –> PROOFS is NP-complete

First, we show that: If ZFC is consistent, then there exist both theorems and non-theorems of ZFC. Based on any given SAT instance, we can construct a proposition that is an existentially quantified boolean proposition, where each variable is itself intended to be a proposition. For example: “there exists x1 s.t. there exists x2 s.t. there exists x3 s.t. (x1 v x2 v !x3) ^ (x3 v !x2) ^ (!x1 v !x1 v x3 v !x2 v x1)”. For each variable x1, x2, … , x_n, let x_i be one of two propositions from ZFC: provable_prop or !provable_prop (i.e., the negation of provable_prop).

If the initial SAT instance that we are mapping to a ZFC proposition is satisfiable, then we need only select x1, x2, … , x_n so that each x_i is either provable_prop or !provable_prop and the proposition is satisfied. Once we’ve done this, we’ll find that the resulting proposition simplifies to provable_prop, which is itself a theorem, implying that there do indeed exist propositions x1, x2, … , x_n s.t. the main proposition is a theorem.

On the other hand, if the initial SAT instance is unsatisfiable, then the main ZFC proposition that we map to will have no possible assignments to the literals (x1, x2, … , x_n) that will yield a provable proposition. This is clear because the ZFC proposition simplifies to a contradiction, which cannot be proved if ZFC is consistent.

This argument establishes that ZFC is consistent –> PROOFS is NP-hard. PROOFS is clearly NP, because proofs are checkable in polynomial time and the length of the proof to be guessed is linear in the size of the unary string of 1’s. Thus ZFC is consistent –> PROOFS is NP-complete.

2 – ZFC is inconsistent –> PROOFS is in P

Given the language PROOFS as described above, assume that ZFC is inconsistent. Then we have that we can find a contradiction in ZFC in constant space and time. Further, every proposition in ZFC can be proved, and a proof can be found in polynomial time. (If not enough space is available to generate the full proof of the contradiction in ZFC, we can still guess all possible proofs of the theorem in constant time and see if one of them works, since the proof allocated for the theorem must be shorter than the proof of the contradiction.)

3 – PROOFS is not in P –> ZFC is consistent

This follows immediately from the contraposition of (2).

4 – ZFC is consistent –> (PROOFS is not in P) is unprovable

By Godel’s Second Incompleteness Theorem, we cannot establish that ZFC is consistent unless ZFC is inconsistent. As we see from (3), if we could prove that PROOFS is not in P, then we would be able to prove that ZFC is consistent; this implies that ZFC is inconsistent, so we see that (PROOFS is not in P) is provable –> ZFC is inconsistent. Thus, by contraposition, we get the statement we are seeking to establish.