In type theory, proving a statement means to exhibit an instance/element of a type corresponding to the statement. But if the statement is undecidable, no element of the type A nor its negation A → ⊥ can be generated. How can be proven that the statement A is undecidable?
2
-
2$\begingroup$ The question seems to conflate unprovable with independent. A statement is unprovable in a theory, if it is not provable in that theory. The statement is independent of a theory, if neither the statement nor its negation is provable. $\endgroup$– Joel David HamkinsCommented Nov 20, 2022 at 0:10
-
2$\begingroup$ Changed "unprovable" into "undecidable" for clarification $\endgroup$– Daniel MurciaCommented Nov 20, 2022 at 1:45
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
3
"A is unprovable" is a shortcut of "A is unprovable in the theory T": provability is always relative to a specified theory.
The statement "A is unprovable in the theory T" cannot be a statement of the theory T itself, as the rules and axioms that define T are expressed in a meta-language "outside" T.
A standard way to prove that a statement is unprovable in a theory T, is to exhibit two different models of the theory T, one in which A is provable, and one in which $\neg$A is provable. The models themselves are defined as objects in another theory, such as set theory or category theory, so that they satisfy all rules and axioms of T, plus extra properties so that the statement A or $\neg$A is also satisfied.
This is not specific to type theory. Forcing is a famous technique for proving such statement independence results. It was first defined for set theory, but can be adapted to type theories.
-
1$\begingroup$ 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. $\endgroup$ Commented Nov 20, 2022 at 0:05
-
3$\begingroup$ 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!) $\endgroup$ Commented Nov 20, 2022 at 0:46
-
3$\begingroup$ (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! $\endgroup$ Commented Nov 20, 2022 at 0:48