2
$\begingroup$

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?

Improve this question
$\endgroup$
2
  • $\begingroup$ What do you mean by a type or a term to be 'explicit'? $\endgroup$
    – ice1000
    Jun 13 '21 at 3:11
  • $\begingroup$ @ice1000 if you could write down the string defining it $\endgroup$
    – jlft
    Jun 13 '21 at 7:05
6
$\begingroup$

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
Improve this answer
$\endgroup$
2
  • $\begingroup$ Are all examples necessarily of your form? $\endgroup$
    – jlft
    Jun 12 '21 at 18:40
  • $\begingroup$ Let $A$ be one of my examples, then take $A \lor \lnot A$ for your $T$. $\endgroup$
    – András Kovács
    Jun 12 '21 at 19:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.