# How do you derive a type $∃e(e)$ in terms of universally quantified types, without invoking Void initially?

I wrote a "proof" for this, and though it was enough to convince myself, there are a few things that bother me about it. Primarily I'm not sure about the loose way in which I'm swapping between first-order logic and the Curry-Howard correspondence, and some ancient and brief exposure to first-order logic as an undergraduate. I'm looking to keep the proof fairly intuitive, and avoid any overly clever invocations if possible (though I don't mind hearing about them).

I'm using a possibly non-standard convention that the syntax $$∃e(e)$$ means $$∃e(P(e))$$ where $$P(e)$$ means there exist a value of type $$e$$. Let $$\texttt{Void}$$ denote a type devoid of any values, and assume it can be expressed as $$∀a(a)$$ in the type system, which seems a legitimate take on affairs as it would be seemingly impossible to construct a value simultaneously inhabiting every type. Then a function from $$T → \texttt{Void}$$ is equivalent to $$¬T$$ by Curry-Howard, I believe.

Rather than going about it the hard way and trying to find a universal-only sentence that is implied by $$∃e(e)$$, then proving a logical equivalence, I'll start with a universally quantified type I've been given by an oracle, then show how this implies $$∃e(e)$$.

\begin{multline} \shoveleft \begin{aligned} ∀r[∀a(a → r) → r] \\ ∀r∀a(a → r) → ∀r(r) \\ ∀r∀a(a → r) → \texttt{Void} \\ ¬∀r∀a(a → r) \\ ∃r[¬∀a(a → r)] \\ ∃r[∃a(¬(a → r))] \\ ∃r[∃a(¬(¬a∨r))] \\ ∃r[∃a(a∧¬r)] \\ \text{(provable identities) } ∃r[∃a(a)∧¬r] \\ \text{(eliminate conjunction) } ∃r[∃a(a)] \\ \text{(eliminate redundant quantifier) } ∃a(a) \end{aligned} \end{multline}

(Apologies for the Unicode symbols, I gather it isn't the norm, but I'm trying to collect some notes in a markdown document.)

• Perhaps it is best to show equivalence, though, in which case this is only one side of the coin. – bbarker Aug 22 '19 at 15:27
• If you want a inhabitant of a type in some type theory, you should be clearer about what type theory you're using and you should endeavor to use notation that formalized in a system for which you can reference, preferably a common one like ITT. I think you intend $\exists e(e)$ to mean something like $\exists T:\mathcal U.T$ or $\Sigma T:\mathcal U.T$ where $\mathcal U$ is a universe. If so, it is easy to provide an inhabitant of it as you just need some type with an inhabitant, e.g. $\Pi T:\mathcal U.T\to T$. – Derek Elkins left SE Aug 23 '19 at 2:27