# Proof systems and their hierarchy

Why ZFC is placed in top of the proof system hierarchy? How it can p-simulate other systems?

-
I really would appreciate some definition links to "proof system hierarchy" and "p-simulation". – Hans Stricker Jul 23 '11 at 15:18
@Hans Stricker, check the Wikipedia pages for "proof complexity" (en.wikipedia.org/wiki/Proof_complexity) and "propositional proof system" (en.wikipedia.org/wiki/Propositional_proof_system). – Kaveh Aug 2 '11 at 6:19

ZFC as propositional proof system can p-simulate any propositional proof system whose soundness (if there is proof for a formula then the formula is true) as a propositional proof system is provable in ZFC. The trick (which I think is due to Steve Cook) is based on the fact that proofs are concrete finite objects, if there is a proof for a formula in a proof system, then ZFC can prove its existence (i.e. ZFC is $\Sigma_1$-complete), combining this with the provability of the soundness we derive the truth of the encoded formula in ZFC. The rest of the argument is translating this first order proof in ZFC to a propositional proof in ZFC as propositional proof system and proving the equivalence of a propositional formula with the formula itself in the proof system. This can be done in $\mathsf{TC^0}$-Frege and any system that contains it. See Logical Foundations of Proof Complexity, 2010 by Cook and Nguyen for the details.
Strictly speaking, it's the function $F$ that maps ZFC-proofs of $T$ to $T$ (where $T$ is a tautology) that is the propositional proof system, not ZFC itself. Note also that the assertion that $F$ is a propositional proof system isn't provable in ZFC itself; you need to assume the soundness of ZFC. This is why people put ZFC at the top; conceivably, there could be "stronger" propositional proof systems $F$ that ZFC can't prove are actually propositional proof systems. But if you think that ZFC represents the outer limit of mathematical knowledge, you might have qualms about such $F$. – Timothy Chow Jul 22 '11 at 22:24