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?



Undecidable statements in type theory
"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.


