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?

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

1 Answer 1

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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