Suppose $B(x)$ set $(x:A)$ is a family of sets and $D$ is a set. Prove $(\Sigma x:A)B(x) \times D \to (\Sigma x:A)(B(x) \times D)$.

Using the so called Curry-Howard correspondence one may translate this statement into a predicate expression: $(\exists x \phi(x) \land \psi) \to \exists x(\phi(x) \land \psi)$ if $x \not \in \text{FV}(\psi)$. In what follows, I have tried to spell out, as clearly as possible, my incomplete solution to the question.

Subgoal 1: Prove the existence of a derivation in natural deduction of the given expression.

Let $\text{FV}(\exists x \phi(x) \land \psi)=\{z_{1},\dots,z_{k}\}$. My goal then is to show that $\mathfrak{A} \models \forall z_{1} \dots z_{n}\left[(\exists x \phi(x) \land \psi) \to \exists x(\phi(x) \land \psi) \right]$ for all structures $\mathfrak{A}$. Thus, using lemma 2.4.5 (p. 71 Van Dalen) that $\mathfrak{A} \models \exists x[\phi(x, \overline{a}_{1},\dots,\overline{a}_{k}) \land \psi(\overline{a}_{1}, \dots, \overline{a}_{k})] \iff \exists x \phi(x, \overline{a}_{1},\dots,\overline{a}_{k}) \land \psi(\overline{a}_{1}, \dots, \overline{a}_{k})$ for all $\mathfrak{A}$ and all $a_{1}, \dots, a_{k} \in |\mathfrak{A}|$. As $a_{1}, \dots, a_{k}$ remains fixed throughout the argument, I won't -

$\mathfrak{A} \models \exists x \phi(x,----) \land \psi(----) \iff \mathfrak{A} \models \exists x \phi(x,----)$ and $\mathfrak{A} \models \psi(----) \iff \mathfrak{A} \models \phi(\overline{b},----)$ for some $b$ and $\mathfrak{A} \models \psi(----) \iff \phi(\overline{b},----) \land \psi (----)$, for some $b$, $\iff \exists x \left[(\phi(x,----) \land \psi(----)\right]$, which is the desired result. $\mathfrak{Q.E.D}$

By the completeness theorem $\mathfrak{A} \models \Gamma \implies \mathfrak{A} \vdash \Gamma$, there exists a derivation in natural deduction from $(\exists x \phi(x) \land \psi)$ to $\exists x(\phi(x) \land \psi)$ (when $x \not \in \text{FV}(\psi)$).

Subgoal 2: Determine a derivation in natural deduction of $(\exists x \phi(x) \land \psi) \to \exists x(\phi(x) \land \psi)$

I have done so in a proof tree.

enter image description here

Subgoal 3: Translate the derivation obtained in the section above into a type theory

In the case I managed to produce a satisfactory derivation, I now face the somewhat daunting task of translating this into type theory. Here is where I am stuck. I have no problem forming $(\Sigma x:A)B(x) \times D$, instead it is the $\Sigma$-elimination rule (which I suppose I should use?) that brings me trouble. How exactly do I express the right branch of the tree in type theory? Help would be very much appreciated.


I think your proof tree has an error in it: $[\exists x \phi(x)\wedge\psi]$ should really be on top (so there's only one branch), followed by the elimination rule for $\exists$ which gives you the beginning of your current branch $\phi([\bar a/x])\wedge\psi$.

You can get the type-theoretic proof by just replacing all your statements and inferences with their type-theoretic versions that the Curry-Howard isomorphism gives you (this is the point of the Curry-Howard isomorphism: inferences in standard logic correspond exactly to inferences in type theory). Unfortunately, if you try to do any serious back-and-forth between logics without explicitly keeping track of contexts (i.e. lists of free variables), things get harder to see.

To use the type-theoretic elimination rule, you start with $p:(\sum x:A)B(x)\wedge D$, from which you automatically get $\pi_1(p):(\sum x:A)B(x)$ and $\pi_2(p):D$.

Then it is easy to see that the three hypotheses for the elimination rule for $\sum$ are satisfied:

  1. $p:(\sum x:A)B(x)\wedge D\vdash (\sum x:A) (B(x)\wedge D)$ Type (this just says that what we are trying to prove is well-formed)
  2. $p:(\sum x:A)B(x)\wedge D,\, a:A, b:B(a)\vdash (a,(b,\pi_2(p)):(\sum x:A) (B(x)\wedge D)$ (this says that if we had our initial assumption, and terms $a:A$ and $b:B(a)$, then we have a term of $(\sum x:A)(B(x)\wedge D)$, which is true by term-introduction first for $\wedge$, and then for $\sum$
  3. $p:(\sum x:A)B(x)\wedge D\vdash \pi_1(p): \sum(x: A)B(x):$ (this says that we do in fact have a term of $\sum(x: A)B(x)$ under our assumption)

Since the terms of $\sum(x:A)B(x)$ are supposed to be precisely (dependent) pairs of terms $x:A$, $y:B(x)$, then 3. saying that we have such a term, and since 2. says that any such dependent pair of terms gives us a term of what we want to prove, we should be able to build a term of our conclusion. This is exaftly what the elimination rule for $\sum$ says we can do! So we get:

  • $p:(\sum x:A)B(x)\vdash ind_{(\sum x:A):B)}(x.y.(y,\pi_2(p)),p):\sum(x:A)(B(x)\wedge D)$
  • $\begingroup$ Would there be any changes if we exchanged $\land$ for $\times$? $\endgroup$ – user111731 Dec 1 '13 at 21:31
  • $\begingroup$ Oops, I meant $\times$ whenever I wrote $\wedge$ in the type theory section (I happen to think of the two as different notations for the same thing). So no, everything should be the same if you have $\times$ or $\wedge$. $\endgroup$ – Vladimir Sotirov Dec 2 '13 at 3:18
  • $\begingroup$ My problem is that I have difficulties writing a proof-tree of the answer you give above. Should (1) and (3) contain no derivations, that is to say should they be written just as you wrote above directly on the line of elimination? Finally, is $p:(\Sigma x:A)B(x)$ (the last line) $p:(\Sigma x:A)B(x) \times D$ or am I missing out? $\endgroup$ – user111731 Dec 2 '13 at 10:04

Your Answer

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

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