2

1

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

flag
2 
 I really would appreciate some definition links to "proof system hierarchy" and "p-simulation". – Hans Stricker Jul 23 2011 at 15:18
2 
 @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 2011 at 6:19

2 Answers

-9

Iam really sorry for this delayed reply...I just digged up a bit on this topic. Here are 'my views' , Iam novice in this area, if I am wrong correct me.

Frege systems ( also hilbert systems) is a better proof system than Gentzen systems as it captures "Human thinking" also. Now, if we add some rules which , say act as lemmas, they readily help us in proving a problem in the proof system. This lemma need not be proved in this problem again , we can just quote it.The Frege + rules = EXTENDED FREGE system.

There is strong parallelism between Proof system and Circuit complexity proof system wherein we can simulate one problem into other.The circuit complexity class heirarchy is like Ac , NC , P/poy , TC . We concentrate on P\Poly what it means. P\poly solves the problem in polynomial time given "some polynomial time advice function".

If we closely observe these advice functions, they are similar to 'lemmas' or 'rules' in extended frege system. Thus P\poly is equivalent to Extended Frege system.Is this the best proof system ? I think no because if we want to compare two outputs produced by applying different lemmas in this system we don;t have any parameter to compare. So we have Zorn's Lemma in our hand where it says that if we have upper bound in every chain, then we have maximal element in that set. This for us nothing but the "Axiom Of Choice". The proof system with the axoim of choice is ZFC. IS THIS THE ULTIMATUM ? No one knows......

link|flag
2 
 As a non-expert in this particular area, I much prefer to read answers of experts than to write my own attempts. – Andrej Bauer Aug 26 2011 at 9:45
I am unable to see how this addresses the question (which, according to Kaveh's answer, seems to be based on false premises). – S. Carnahan♦ Aug 29 2011 at 2:10
6

It is an open problem if there is an optimal propositional proof system. Therefore we don't know if ZFC as a propositional proof system is optimal either.

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.

link|flag
1 
 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 2011 at 22:24
@Timothy, there are two equivalent definitions for a pps, one is what you described, the other one is a proof checker program (which the one I found more natural). Yes, strictly speaking, but I didn't want to go into too much details. One can add axioms to obtains a possibly stronger pps, e.g. large cardinal axioms. Note that we don't need the full soundness, we only need a very restricted form of it. In fact, as you know :), some proof complexity theorist conjecture that EF is a plausible candidate for the optimal proof system, in which case ZFC will be just equal to it. – Kaveh Aug 2 2011 at 6:13

Your Answer

Get an OpenID
or

Not the answer you're looking for? Browse other questions tagged or ask your own question.