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 at 3:11
  • $\begingroup$ @ice1000 if you could write down the string defining it $\endgroup$
    – jlft
    Jun 13 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
$\endgroup$
2
  • $\begingroup$ Are all examples necessarily of your form? $\endgroup$
    – jlft
    Jun 12 at 18:40
  • $\begingroup$ Let $A$ be one of my examples, then take $A \lor \lnot A$ for your $T$. $\endgroup$ Jun 12 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.