# Second Order Logic: Existential could be expressed as a universal quantifier.

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.

Edit:

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.

-
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