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, 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

Reset to default
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, 2021 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, 2021 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.