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.)

  • $\begingroup$ Perhaps it is best to show equivalence, though, in which case this is only one side of the coin. $\endgroup$ – bbarker Aug 22 '19 at 15:27
  • 1
    $\begingroup$ 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$. $\endgroup$ – Derek Elkins left SE Aug 23 '19 at 2:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.