Timeline for What if Current Foundations of Mathematics are Inconsistent?
Current License: CC BY-SA 2.5
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 7, 2010 at 14:10 | comment | added | Daniel Tausk | Unfortunately, there seems to be no trivial way of getting around Gödel's theorem (otherwise, people like Gödel and Hilbert would have already found a way to do it). Either we work with systems for which no strictly finitary proof of consistency (say, a proof in PRA or less) is possible or we work with systems that cannot handle the vast majority of what we today call "mathematics". | |
| Oct 7, 2010 at 14:05 | comment | added | Daniel Tausk | Ok, so maybe we would have "proofs", "reliable proofs" and "certifiably reliable proofs", i.e., those "reliable proofs" for which the algorithm halts in finite time and answers "yes, this is reliable" (actually, it would be semantically less messy to restrict the term "proof" just for the "certifiably reliable proofs"). Since a Gödel-like theorem would block finitary proofs of consistency of the theory in which only the "certifiably reliable proofs" are considered, it would, a fortiori, block finitary proofs of consistency of the theory in which all "reliable proofs" are considered. | |
| Oct 7, 2010 at 13:20 | comment | added | Dan Petersen | Probably I misused the word probabilistic algorithm -- I'm no computer scientist. What I meant is that he seems to leave open the possibility that there are reliable proofs for which this hypothetical algorithm would not halt, but that one should get a certificate for "most" reliable proofs. | |
| Oct 7, 2010 at 12:32 | comment | added | Daniel Tausk | Ok, so normally we have an algorithm that checks whether something is a proof (i.e., the set of all proofs is recursive), which implies that the set of all theorems is $\Sigma_1$ (i.e., recursively enumerable). The new proposal would be: let's have an algorithm that takes a proposed proof as input, sometimes it halts and answers "yes, that is a (reliable) proof" and sometimes it doesn't halt. This makes the set of all (reliable) proofs $\Sigma_1$ (instead of recursive), but this again implies that the set of all theorems is $\Sigma_1$, so I guess Gödel-like arguments would apply just as well. | |
| Oct 7, 2010 at 7:26 | comment | added | Dan Petersen | I think Voevodsky intends to get around your last argument by not actually assuming the existence of an algorithm that separates reliable and unreliable proofs. Rather, it seems that he describes a probabilistic algorithm that given a reliable proof will generically produce a certificate of its reliability in finite time, but given an unreliable proof it will simply not halt. So there would be no way of proving unreliability of a proof using this hypothetical algorithm, and he leaves open the possibility that there will exist reliable proofs whose reliability cannot be proven either. | |
| Oct 6, 2010 at 23:33 | history | answered | Daniel Tausk | CC BY-SA 2.5 |