Timeline for Incompleteness and nonstandard models of arithmetic
Current License: CC BY-SA 2.5
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 19, 2010 at 15:37 | comment | added | Daniel Mehkeri | ECT can be weakened too. The paper I cited uses a weaker form, and the fan theorem is consistent with that form, so your example doesn't quite work. But you probably were thinking of WKL. Classically WLK is equivalent to the fan theorem, but constructively WKL implies a restricted form of the law of the excluded middle called LLPO. So it might work. | |
| Jun 16, 2010 at 11:29 | comment | added | Carl Mummert | Mightn't it be enough just to add axioms that contradict ECT and also permit the desired construction? For example, the compactness theorem of logic might be provable from the fan theorem; I don't know if it is or not. But since ECT implies the negation of the fan theorem intuitionistically, and since the compactness theorem for countable theories is equivalent to the fan theorem classically, this is at least plausible. I know there is some existing work on intuitionistic model theory (e.g. jstor.org/pss/2271944) but I'm not familiar enough to skim for this result. | |
| Jun 15, 2010 at 22:48 | comment | added | Daniel Mehkeri | Yeah, it follows from ECT that there are no nonstandard models of HA, it does NOT follow from HA that there are no nonstandard models of ECT. But it does not follow that there are, either. It requires assuming classical logic in the meta-theory to show that. | |
| Jun 15, 2010 at 11:44 | comment | added | Carl Mummert | It's worth pointing out explicitly that this requires assuming ECT in the metatheory. There are certainly nonstandard models of ECT in usual first-order logic. | |
| Jun 15, 2010 at 4:20 | history | answered | Daniel Mehkeri | CC BY-SA 2.5 |