Is there an explicit type $T$ in Martin-Löf type theory such that $(T\to \mathbf{0})\to\mathbf{0}$ has an explicit closed term and $T$ can be shown externally to not have closed terms?
2
-
$\begingroup$ What do you mean by a type or a term to be 'explicit'? $\endgroup$– ice1000Jun 13, 2021 at 3:11
-
$\begingroup$ @ice1000 if you could write down the string defining it $\endgroup$– jlftJun 13, 2021 at 7:05
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
2
Sure. Take any $A$ type which cannot be proven or disproven in MLTT, necessarily by some external argument. Then $A \lor \lnot A$ is not provable but $\lnot (\lnot (A \lor \lnot A))$ is provable, because this is an intuitionistic tautology for all $A$. Reminder: $\lnot A$ is defined as $A \to \mathbf{0}$.
Some examples for types whose inhabitation is independent from basic intuitionistic MLTT:
- Function extensionality
- Uniqueness of identity proofs
- Parametricity (for given types)
- Law of excluded middle
-
-
$\begingroup$ Let $A$ be one of my examples, then take $A \lor \lnot A$ for your $T$. $\endgroup$ Jun 12, 2021 at 19:39