Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

As you all know, the Curry-Howard correspondance provides a link between type theory and predicate logic. Concepts featured in the former, such as $\Pi$-type and $\Sigma$-type can, by the interpretation of propositions-as-types, be thought of as $\forall$ and $\exists$. This remarkable feature is very convenient for someone like me, who is just starting out learning more about intuitionistic type theory. My current goal is to learn more about how to construct proofs (i.e. derivations) for statements such as $(\Pi x\in A)(B(x) \times C(x)) \to ((\Pi x \in A)B(x) \times (\Pi x \in A)C(x))$, $(\Sigma x \in A)(B(x) \times D) \to ((\Sigma x \in A)B(x) \times D)$, and $(\Pi x \in A)(B(x) \to C(x)) \to ((\Pi x \in A)B(x) \to (\Pi x \in A)C(x))$ - where $B(x),C(x)$ represents families of sets and $D$ is just one set.

I figure that intuitionistic type theory is a much more complicated system than first-order logic. For one thing, more information is carried around in the derivations due to the identification of propositions and types. Furthermore, the well-formed formulas have to be generated simultaneously with the provable true formulas.

By reason of this, I would very much appreciate if anyone would be so kind as to explain how to write proofs in type theory, preferably with respect to the two examples given below. Thanks!

Predicate Logic Derivations

Given the Curry-Howard correspondance, we may translate the type theoretical statement $(\Pi x\in A)(B(x) \times C(x)) \to ((\Pi x \in A)B(x) \times (\Pi x \in A)C(x))$ into a predicate statement $\forall x(B \land C) \to (\forall x B \land \forall x C)$

\begin{array}{lr} 1. & \forall x (B \land C) & \text{Assumption} \\ 2. & B \land C & \text{Universal Elimination 1} \\ 3. & B & \text{Conjunction Elimination 2} \\ 4. & \forall xB & \text{Universal Instantiation 3} \\ 5. & \forall x(B \land C)& \text{Assumption} \\ 6. & B \land C & \text{Quantifier Elimination 5} \\ 7. & C & \text{Conjunction Elimination 6} \\ 8. & \forall x C & \text{Universal Instantiation 6} \\ 9. & \forall x B \land \forall x C & \text{Conjunction Instantiation 4,8} \\ 10.& \forall x (B \land C) \to (\forall x B \land \forall x C) & \text{Discharge 1,5} \\ \\ \end{array}

Again, using Curry-Howard correspondance $(\Pi x \in A)(B(x) \to C(x)) \to ((\Pi x \in A)B(x) \to (\Pi x \in A)C(x))$ can be translated into $\forall x(B \to C) \to (\forall x B \to \forall x C)$.

\begin{array}{lr} 1. & \forall x (B \to C) & \text{Assumption} \\ 2. & B \to C & \text{Universal Elimination 1} \\ 3. & \forall xB & \text{Assumption} \\ 4. & B & \text{Universal Elimination 3}\\ 5. & C & \text{Modus Ponens 3,4} \\ 6. & \forall x C& \text{Universial Instantiation 5} \\ 7. & \forall xB \to \forall xC& \text{Discharge 3} \\ 8. & \forall x(B \to C) \to (\forall x B \to \forall x C)& \text{Discharge 1} \end{array}

PS Information regarding the rules in question can be found here http://www.csie.ntu.edu.tw/~b94087/ITT.pdf, from page 13 to page 26. DS

share|improve this question
add comment

1 Answer

In order to exhibit a term having type $$ (\Pi x \in A)(B(x) \times C(x)) \rightarrow ((\Pi x \in A) B(x) \times (\Pi x \in A) C(x)) $$ you just have to garnish the proof of the corresponding proposition with proof terms. I will write the derivation in lines, but it would be clearer to see it as a proof-tree.

  1. $f \in (\Pi x \in A)(B(x) \times C(x))$ (assumption, discarded in 11)
  2. $x \in A$ (assumption, discarded in 5)
  3. $\mathsf{Ap}(f, x) \in B(x) \times C(x)$ (by 1, 2)
  4. $\pi_1(\mathsf{Ap}(f, x)) \in B(x)$ (by 3)
  5. $(\lambda x) \pi_1 (\mathsf{Ap}(f, x)) \in (\Pi x \in A) B(x)$ (by 4, discard 2)
  6. $x \in A$ (assumption, discarded in 9)
  7. $\mathsf{Ap}(f, x) \in B(x) \times C(x)$ (by 1, 6)
  8. $\pi_2(\mathsf{Ap}(f, x)) \in C(x)$ (by 7)
  9. $(\lambda x) \pi_2 (\mathsf{Ap}(f, x)) \in (\Pi x \in A) C(x)$ (by 8, discard 6)
  10. $\langle (\lambda x) \pi_1(\mathsf{Ap}(f, x)), (\lambda x) \pi_2 (\mathsf{Ap}(f, x)) \rangle \in (\Pi x \in A) B(x) \times (\Pi x \in A) C(x)$ (by 5, 9)
  11. $(\lambda f) \langle (\lambda x) \pi_1(\mathsf{Ap}(f, x)), (\lambda x) \pi_2 (\mathsf{Ap}(f, x)) \rangle \in (\Pi x \in A)(B(x) \times C(x)) \rightarrow ((\Pi x \in A) B(x) \times (\Pi x \in A) C(x))$ (by 10, discard 1)

So in the end $(\lambda f) \langle (\lambda x)\pi_1(\mathsf{Ap}(f, x)), (\lambda x) \pi_2 (\mathsf{Ap}(f, x)) \rangle$ is the desired proof term (I have used $\langle \cdot, \cdot \rangle$ for the constructor of the binary cartesian product, and $\pi_1$, $\pi_2$ for its two projections. Maybe you would use a different notation, but I hope the meaning is clear).

Indeed, we obtained a function taking a term $f$ of type $(\Pi x \in A)(B(x) \times C(x))$ as an argument and returning a pair, whose two components are functions taking a term of type $A$ and returing a term of type $B(x)$ and a term of type $C(x)$ respectively, i.e. the pair is a term of type $(\Pi x \in A) B(x) \times (\Pi x \in A) C(x)$.

share|improve this answer
add comment

Your Answer

 
discard

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.