Timeline for Inconsistent theory with long contradiction
Current License: CC BY-SA 2.5
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 5, 2016 at 7:13 | answer | added | Joseph Van Name | timeline score: 3 | |
| Jun 8, 2011 at 17:39 | answer | added | Mirco A. Mannucci | timeline score: 2 | |
| Jun 8, 2011 at 16:47 | answer | added | Emil Jeřábek | timeline score: 8 | |
| Jan 15, 2011 at 12:00 | comment | added | Thomas Riepe | Voevodsky mentioned that issue in his recent popular IAS video talk, perhaps it is interesting to look at his program for reformulating the foundations of mathematics (with homotopy as basis, circumventing with the means of some programming language the use of set theory, if I understood his remarks correctly). | |
| Jan 14, 2011 at 23:50 | history | edited | David Harris | CC BY-SA 2.5 |
added 213 characters in body
|
| Jan 14, 2011 at 23:42 | comment | added | Andrés E. Caicedo | @Michael: This is a good point. But there are companion results (by Goedel, and more recently by Buss) that indicate how assuming the consistency of a theory leads to serious speed-up of proofs. Anyway, I cannot currently imagine a reasonable scenario where we could turn this into a method to anticipate a contradiction akin to what Sebastian R. is suggesting. It is worth giving it some thought, though. | |
| Jan 14, 2011 at 23:27 | comment | added | Sebastian Reichelt | What if the contradiction is too long to be written down explicitly, but there is a systematic way of constructing it? (In the same way that for every given Goodstein sequence, there is a proof in PA that it terminates. Even though it can become arbitrarily large, we can still construct it, in a sense.) | |
| Jan 14, 2011 at 23:11 | comment | added | Michael Hardy | ......just systematically search for a proof until one has exhausted those shorter than the bound. Gödel tells us that if the formula is universally valid, then there's a proof.) Hence, just take any theorem whose shortest proof is long. Deriving a contradiction from its negation will take a long time. | |
| Jan 14, 2011 at 23:11 | comment | added | Michael Hardy | I posted the following as an answer and then deleted it after it appeared that I misunderstood the question. But maybe it's worth bearing in mind here: It is a corollary of some theorems of logic discovered in the 1930s that the ratio of lengths of proofs to lengths of theorems is unbounded. (If it were bounded, then there would be an algorithm for deciding which formulas of first-order logic are universally valid, contradicting the conjunction of Church's theorem with Gödel's completeness theorem:...... | |
| Jan 14, 2011 at 21:02 | comment | added | David Harris | Alec, the example you give is very nice. I am not so sure that this example should be ruled out though. It seems plausible to me that you can still work with this theory as long as you stay "local enough". | |
| Jan 14, 2011 at 20:04 | comment | added | Alec Edgington | I guess you need to somehow say that $n$ should be large in relation to the size of the 'specification' of the theory? Otherwise, you could construct such a theory artificially: for example, $T$ could contain statements $P_0, P_1, \ldots, P_n$, with $P_0$ as the single axiom, and rules of deduction $P_m \Rightarrow P_{m+1}$ and $P_n \Rightarrow \neg P_0$. (Similarly, any inconsistent theory could be turned into one satisfying your criterion, by 'stretching' the rules sufficiently.) | |
| Jan 14, 2011 at 16:54 | answer | added | Andrés E. Caicedo | timeline score: 24 | |
| Jan 14, 2011 at 15:43 | comment | added | gowers | I'm not the person to explain this in detail, but if a theory has only very long contradictions, then I would have thought it might well have a structure that is in some sense "locally" a model (a bit like the surface of the Earth being locally a model for an infinite plane). | |
| Jan 14, 2011 at 13:56 | comment | added | Qfwfq | +1 . I once thought to ask exactly the same question on MO! | |
| Jan 14, 2011 at 13:19 | history | asked | David Harris | CC BY-SA 2.5 |