<p>Sure. Take any <span class="math-container">$A$</span> type which cannot be proven or disproven in MLTT, necessarily by some external argument. Then <span class="math-container">$A \lor \lnot A$</span> is not provable but <span class="math-container">$\lnot (\lnot (A \lor \lnot A))$</span> is provable, because this is an intuitionistic tautology for all <span class="math-container">$A$</span>. Reminder: <span class="math-container">$\lnot A$</span> is defined as <span class="math-container">$A \to \mathbf{0}$</span>.</p>
<p>Some examples for types whose inhabitation is independent from basic intuitionistic MLTT:</p>
<ul>
<li>Function extensionality</li>
<li>Uniqueness of identity proofs</li>
<li>Parametricity (for given types)</li>
<li>Law of excluded middle</li>
</ul>

CC BY-SA 4.0
2021-06-12T18:40:20.727Z
Are all examples necessarily of your form?
jlft
CC BY-SA 4.0
2021-06-12T19:39:48.797Z
Let $A$ be one of my examples, then take $A \lor \lnot A$ for your $T$.
András Kovács
CC BY-SA 4.0
2021-06-12T18:21:08.423Z
2021-06-12T19:41:31.030Z
2021-06-12T19:41:31.030Z
András Kovács
<p>Is there an explicit type <span class="math-container">$T$</span> in Martin-Löf type theory such that <span class="math-container">$(T\to \mathbf{0})\to\mathbf{0}$</span> has an explicit closed term and <span class="math-container">$T$</span> can be shown externally to not have closed terms?</p>

CC BY-SA 4.0
2021-06-13T03:11:49.077Z
What do you mean by a type or a term to be 'explicit'?
ice1000
CC BY-SA 4.0
2021-06-13T07:05:52.600Z
@ice1000 if you could write down the string defining it
jlft
<type-theory>
External failure of law of excluded middle in Martin-Löf type theory
jlft
# External failure of law of excluded middle in Martin-Löf type theory

(Asked by: username_0 on 2021-06-12)

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?

**Tags:** type-theory

> **Comments:**
> **username_1**: What do you mean by a type or a term to be 'explicit'?  
> **username_0**: @username_1 if you could write down the string defining it  

---

## 1 answers

### Answer by username_2 on 2021-06-12. Score: 6

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

> **Comments:**
> **username_0**: Are all examples necessarily of your form?  
> **username_2**: Let $A$ be one of my examples, then take $A \lor \lnot A$ for your $T$.  

---

