Timeline for Undecidable statements in type theory
Current License: CC BY-SA 4.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 20, 2022 at 0:48 | comment | added | Noah Schweber | (Alternatively, if as usual you want to keep the trusted background theory in the background, you could just drop all references to provability at all: "exhibit models $M$, $N$ of $T$ such that $A$ holds in $M$ and $\neg A$ holds in $N$.") These sorts of issues may seem like hair-splitting at first, but they're actually crucially important! | |
| Nov 20, 2022 at 0:46 | comment | added | Noah Schweber | Expanding on @JoelDavidHamkins' comment, this answer would be correct if it were written as "... exhibit two different models of the theory T, such that it is provable that A holds in one and A fails in the other" (emph. mine). That is, the right situation is the following: if we can build models $M$, $N$ such that our "trusted background theory" proves $M\models A$ and $N\models \neg A$, then that same trusted background theory will prove that $A$ is independent of $T$. (The issue Joel points out is that we don't want to ask the models themselves about what is and isn't provable!) | |
| Nov 20, 2022 at 0:05 | comment | added | Joel David Hamkins | This answer seems problematic. To show that a statement $A$ is unprovable in a theory $T$, one should exhibit a model in which $T$ is true, but $A$ is not. This shows that $A$ is not a valid consequence of $T$, so it cannot be proved from $T$. The method suggested in the answer, however, exhibiting models of $T$ in which $A$ is is provable and $\neg A$ is provable, wouldn't actually even show that $A$ is not provable. For example, there is a model of PA in which 0=0 is provable, and also a model of PA in which $\neg 0=0$ is provable---take any model of PA+$\neg$Con(PA). Bu 0=0 is provable. | |
| Nov 19, 2022 at 21:44 | vote | accept | Daniel Murcia | ||
| Nov 19, 2022 at 20:32 | history | answered | L. Garde | CC BY-SA 4.0 |