Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

I would like to ask if the following proof is correct:

$\exists X.B\Leftrightarrow \forall Y. (\forall X. B\to Y)\to Y$

Starting with a $B\in\Gamma$ in the sequent set and:

$\exists X.B\Rightarrow \forall Y. (\forall X. B\to Y)\to Y$

Applying the $\Rightarrow_i$ rule, I'll obtain $\Gamma=\Gamma\cup\{\exists X.B\}$ and:

$\forall Y. (\forall X. B\to Y)\to Y$

Hereby, using $\forall_i$ with a $C\notin \Gamma$, I will obtain:

$(\forall X. B\to C)\to C$

Using again $\Rightarrow_i$ and $\Gamma=\Gamma\cup\{\forall X. B\to C\}$ I will now have to provide a proof for $C$ (*). Now i will start from the shared hypothesis

$(\forall X. B\to C)$

and using $\forall_e$ with $D$ as $X$ I will obtain the $B\to C$ hypothesis (H1). From the shared hypothesis:

$\exists X.B.$

and applying the $\exists_e$ rule with $D$ as $X$, I will obtain the $B$ hypothesis (H2). Hence, I could use H1 and H2 to obtain the $C$ (*):

$\frac{B\to C\;(H1)\qquad B\;(H2)}{C\;(*)}$

Now I believe that this demonstration is wrong in the elimination of the existential but, how could I proof the vice versa (the right to left implication)? Thanks in advance.


I would like then to proof that the existential Type could be expressed with an universal form, hence my proof given above. In fact, using the Curry-Howard isomorphism, I could also express some connectives as conjunction, disjunction of formulas with this encoding, so:

$A\wedge B\equiv\forall X.(A\to B\to X)\to X$.

and for disjunction:

$A\vee B\equiv\forall X.(A\to X)\to (B\to X)\to X$

If you read the "Types and programming languages" by Benjamin Pierce at chapter 24, section 3, page 377 it states that: “The encoding of pairs as a polymorphic type... suggests a similar encoding for existential types in terms of universal types, using the intuition that an lement of an existential type is a pair of a type and a value”:

$\{\exists X,T\}\equiv\forall Y.(\forall X.T\to Y)\to Y$

So, the whole construction will be defined as:

$\{S^\ast,t\}\;as\;\{\exists X,T\}\equiv \lambda Y.\lambda f:(\forall X.T\to Y).\;f\;[S]\;t$

The unpacking funtion could be defined as:

$let\{X,x\}=t_1\;in\;t_2\equiv t_1[T_2](\lambda X.\lambda x:T_{11}.t_2) $

Infact, using the Matita Interactive Theorem Prover, the existential type is encoded as:

inductive ex (A:Type[0]) (P:A → Prop) : Prop ≝ ex_intro: ∀ x:A. P x → ex A P.

that has the following type:

$(\forall A: Type[0] .(A\to Prop)\to Prop)$

In particular, i could give the following proofs of what I want:

lemma test: ∀B:Prop. (∃X:Prop. B)→(∀Y:Prop. (∀X:Prop. B→Y)→Y). 

#B * #e #b #Y #H lapply (H B) #H2 lapply (H2 b) #H @H qed.

lemma test2: ∀B:Prop. (∀Y:Prop. (∀X:Prop. B→Y)→Y)→(∃X:Prop. B). 

#B #H lapply (H B) #H2 % [ 2: @H2 #H3 #I @I | @False]

My problem hence is giving the former proofs in a natural deduction way. Thanks again.

share|cite|improve this question
It's not clear to me what exactly your proof is supposed to establish. What are the hypotheses and what is the conclusion? – Andreas Blass Jun 7 '13 at 1:55
@Andreas Blass: I am a little confused by a deleted comment. If $(\forall X) B$ is false, then $\lnot \lnot (\forall X) B$ is false, so in this case won't $(\forall Y)([(\forall X)B \to Y]\to Y)$ also be false (e.g. when $Y = \bot)$ even if $(\exists X)B$ is true? I am missing something. – Carl Mummert Jun 7 '13 at 2:18
What you have written makes no sense to me. You can only write in a formula something like $\forall Y$ in case that $Y$ is a (first-order or second-order) variable, but then $B \to Y$ is not a formula. In other words, the expression $\forall Y.( \forall X. B \to Y) \to Y$ is not a formula, even assuming $B$ is a formula. – boumol Jun 7 '13 at 6:26
On the other hand, it is obvious that universal and existential quantifiers are interdefinable using negation. Since "negation" coincides with "implies a contradiction" I would suspect you could make sense of your ideas using instead of the variable "Y" any formula that is a contradiction formula. – boumol Jun 7 '13 at 6:30
@CarlMummert You missed a dot in the formula, right after $\forall X$. That's a Principia-style dot, intended to replace parentheses (while being easy to overlook). The scope of $\forall X$ is supposed to be the implication $B\to Y$, not just $B$. – Andreas Blass Jun 11 '13 at 16:26
up vote 0 down vote accepted

Here's my solution in natural deduction. enter image description here

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.