# External failure of law of excluded middle in Martin-Löf type theory

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?

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

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}$$.
• Let $A$ be one of my examples, then take $A \lor \lnot A$ for your $T$. Jun 12 at 19:39