4

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.

jackb
  • 231
  • 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 07 '13 at 01: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 07 '13 at 02: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 07 '13 at 06: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 07 '13 at 06:30
  • I suggest you delete your last comments and add them at the end of your question as an addendum (just edit your question). This will help people to more easily understand your problem. – boumol Jun 07 '13 at 09:37
  • I've done the edits. – jackb Jun 07 '13 at 09:55
  • 1
    @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

1 Answers1

1

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

jackb
  • 231