Is it possible to prove that the encoding of existentials in System F is valid?

Question

In Girard's Proofs and Types, under item 11.3.5, second-order existential quantification is encoded in System F using universal quantification as follows:

$$ \Sigma X.V \equiv \Pi Y. (\Pi X.(V \to Y)) \to Y $$

Is it possible to prove this encoding is correct using natural deduction or sequent calculus? In other words, is it possible to prove the following in System F extended with existentials?

$$ (1)\quad \Sigma X.V \vdash \Pi Y. (\Pi X.(V \to Y)) \to Y \\ (2)\quad \Pi Y. (\Pi X.(V \to Y)) \to Y \vdash \Sigma X.V $$

I think I can prove (1), but not (2).

In case these propositions are invalid, how can we be sure the encoding is correct?

Thank you.

PS.

I understand intuitively why the encoding makes sense, but would like to understand the formal reasons.

This encoding is widespread, but I can't find a proof of its validity. In Haskell, for example, it is used to simulate existential types and in similar questions such as this one the explanation is informal. In this self-answered question, which attempts to produce a proof, I think there are errors involving invalid variable capturing.

Edit: Proof attempt of (2) based on Andrej's answer

I. $$ { \Pi Y. (\Pi X.(VX \to Y)) \to Y \over (\Pi X.(VX \to (\Sigma Z. V Z))) \to (\Sigma Z. V Z) } \, \Pi E $$

II. $$ { \hspace{8em} \over VT } u \\ { \hspace{8em} \over \Sigma Z. VZ } \Sigma I \\ { \hspace{10em} \over V T \to (\Sigma Z. VZ) } \to I_u \\ { \hspace{10em} \over \Pi X. (V X \to (\Sigma Z. VZ)) } \Pi I_T $$

III. From I and II: $$ { \quad (\Pi X. (V X \to (\Sigma Z. V Z))) \to (\Sigma Z. V Z) \qquad \Pi X. (V X \to (\Sigma Z. V Z)) \quad \over \Sigma Z. VZ } \to E $$

Answer 1

For second-order logic with Natural Deduction, you can see :

• Dag Prawitz, Natural Deduction A Proof-Theoretical Study (1965)

or :

• Dirk van Dalen, Logic and Structure (5th ed - 2013).

Both prove :

$ΣX.V \equiv ΠY.(ΠX.(V→Y))→Y$.

See van Dalen, page 150, Theorem 5.5 (e) :

$\vdash_2 ∃X^n \varphi ↔ ∀X^0(∀X^n((\varphi → X^0) → X^0)$.

Proof

$${ [∀X^n(\varphi→X)] \over (\varphi→X) } \, (\forall^2E)$$

$${ [\varphi] \quad (\varphi→X) \over X } \, (\rightarrow E)$$

$${ ∀X^n(\varphi→X)→X \over (\varphi→X) } \, (\rightarrow I) \, \text{(discharging the 1st assumption)}$$

$${ \exists X^n \varphi \quad ∀X^n(\varphi→X)→X \over ∀X^n(\varphi→X)→X } \, (\exists^2E) \, \text{(discharging the 2nd assumption)}$$

$${ ∀X^n(\varphi→X)→X \over \forall X(∀X^n(\varphi→X)→X) } \, (\forall^2I) $$

Thus :

$\vdash_2 ∃X^n \varphi \rightarrow ∀X^0(∀X^n(\varphi \rightarrow X^0) \rightarrow X^0)$.

---

For the other direction :

$${ [\varphi] \over \exists X^n \varphi } \, (\exists^2I)$$

$${ \varphi \rightarrow \exists X^n \varphi \over \forall X^n (\varphi \rightarrow \exists X^n \varphi) } \, (\forall^2I)$$

In parallel :

$${∀X^0(∀X^n(\varphi \rightarrow X^0) \rightarrow X^0) \over ∀X^n(\varphi \rightarrow \exists X^n \varphi ) \rightarrow \exists X^n \varphi } \, (\forall^2E)$$

$${ \forall X^n (\varphi \rightarrow \exists X^n \varphi) \quad ∀X^n(\varphi \rightarrow \exists X^n \varphi ) \rightarrow \exists X^n \varphi \over \exists X^n \varphi} \, (\rightarrow E)$$

Thus :

$\vdash_2 ∀X^0(∀X^n(\varphi \rightarrow X^0) \rightarrow X^0) \rightarrow ∃X^n \varphi$.

---

Note

For the rules, see page 147; in particular :

$${\varphi^* \over \exists X^n \varphi } \, (\exists^2I)$$

and :

$${\forall X^n \varphi \over \varphi^*} \, (\forall^2E)$$

where

$\varphi^*$ is obtained from $\varphi$ by replacing each occurrence of $X^n(t_1,\ldots, t_n)$ by $σ(t_1,\ldots, t_n)$ for a certain formula $σ$, such that no free variables among the $t_i$ become bound after the substitution.

Answer 2

Coq seems to be happy with this. The easy direction (sigT is $\Sigma$ and forall is $\Pi$):

Parameter V : Type -> Type.

Lemma rabbit : 
  sigT V -> forall Y, (forall X , V X -> Y) -> Y.
Proof.
  firstorder.
Qed.

Print rabbit.

We get the following proof:

  fun (X : sigT V) (Y : Type) (P : (forall Z : Type, V Z -> Y)) =>
    sigT_rect (fun _ : sigT V => Y)
              (fun (x : Type) (p : V x) =>
                 (fun X1 : V x -> Y => (fun X2 : Y => X2) (X1 p)) (P x)) X.

where sigT_rect is the eliminator for $\Sigma$. But you asked about the converse:

Lemma fox : 
  (forall Y, (forall X , V X -> Y) -> Y) -> sigT V.
Proof.
  intro H.
  apply H.
  intros X Y.
  exists X.
  exact Y.
Qed.

Print fox.

The proof found is

  fun H : (forall Y : Type, (forall X : Type, V X -> Y) -> Y) =>
    H (sigT V) (fun (X : Type) (Y : V X) => existT V X Y)

This is quite simple, actually, here's a translation. Suppose $$H : \Pi Y \,.\, (\Pi X \,.\,(V X \to Y)) \to Y$$ Then $G = H \,(\Sigma Z \,.\, V Z)$ has the type $$(\Pi X \,.\, (V X \to (\Sigma Z \,.\, V Z))) \to (\Sigma Z \,.\, V Z)$$ and so we just have to apply $G$ to a function of type $$\Pi X \,.\, (V X \to (\Sigma Z \,.\, V Z))$$ Such a function is $$\lambda X \,.\, \lambda W \,.\, (X, W)$$ i.e., the dependent pairing function.