Timeline for Proof systems and their hierarchy
Current License: CC BY-SA 3.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 2, 2011 at 6:13 | comment | added | Kaveh | @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. | |
| Jul 22, 2011 at 22:24 | comment | added | Timothy Chow | 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$. | |
| Jul 22, 2011 at 15:24 | history | edited | Kaveh | CC BY-SA 3.0 |
added 177 characters in body
|
| Jul 22, 2011 at 15:17 | history | answered | Kaveh | CC BY-SA 3.0 |