Is the transitivity of subset proof incomplete everywere?

Question

We are working in ZFC, so under first order logic we introduce the undefined predicate $\in$ and the ZFC axioms.

(1) $\forall A,B,C ((\forall(x \in A \rightarrow x \in B) \land \forall(x \in B \rightarrow x \in C)) \rightarrow \forall(x \in A \rightarrow x \in C))$

By universal elimination rule let $A', B',C'$ be sets.

(2) $(\forall(x \in A' \rightarrow x \in B') \land \forall(x \in B' \rightarrow x \in C')) \rightarrow \forall(x \in A' \rightarrow x \in C')$

Now by the deduction first order theorem if we can deduce $\forall(x \in A' \rightarrow x \in C')$ from $(\forall(x \in A' \rightarrow x \in B') \land \forall(x \in B' \rightarrow x \in C'))$, (2) and consequentially the theorem (1) would be proved. So, we assume

(3) $(\forall(x \in A' \rightarrow x \in B') \land \forall(x \in B' \rightarrow x \in C'))$

To prove

(4) $\forall(x \in A' \rightarrow x \in C'))$

By universal elimination let $x'$ be a set.

(5) $x' \in A' \rightarrow x' \in C'$

Z (The Bourbaki danger)

By the deduction first order theorem again if we can deduce $x \in C'$ from $x \in A'$, then (5) would be proved. So, we assume

(6) $x' \in A'$

If we prove $x' \in C'$ then we have proved (5) and so (4),(2) and (1).

By (6) and (3)

(7) $x' \in B'$

By (7) and (3)

$x' \in C'$ QED!

In all the places where I found the theorem (1) ('the transitivity of subset'), there is some version of this proof that is considered complete and correct. However, it seem to me that this proof is not correct if first we not analyze the case $A'$ is empty in which case (2) is true by vacuity, then we can assume $A'$ is not empty. If we don't do that, (6) is a contradiction in the case $A'$ is empty and so the whole proof is wrong. Am I the wrong one? If so, why?

Answer 1

Here's your basic mistake:

If we don't do that, (6) is a contradiction in the case $A'$ is empty and so the whole proof is wrong. Am I the wrong one?

There's nothing wrong with having contradictory assumptions at some point in a proof. On the contrary, that is a good thing to happen, because it means you can use the Principle of Explosion to conclude whatever you want right away and be done with that branch of the proof.

A more semantic way of saying this is that, finding yourself with contradictory assumptions means that you're in a branch of the proof that doesn't correspond to a possible situation you're trying to prove something about. Therefore no proof is needed in that branch -- or, in yet other words, "eh, whatever" will suffice as a proof. That's the reasoning behind the principle of explosion.

If your particular case, you don't even have a contradicting assumption, only the possibility that there is no $x\in A'$ to prove anything about. Again, this is not a problem for a proof: if it turns out that $A'$ is empty, it still doens't harm you to have had a plan for what to do with its elements.

Answer 2

One point of view which might be useful would be the Curry-Howard correspondence: this point of view interprets (formal) proofs as being programs in a certain typed lambda calculus. (And the more typical informal proofs written in mathematical papers and textbooks correspond to pseudocode...)

So, for this problem, the "program" you need to build is one which takes inputs of a proof of $A \subseteq B$ and a proof of $B \subseteq C$, and outputs a proof of $A \subseteq C$. Furthermore, a "proof" of $A \subseteq B$ consists of a function which takes an object $x : V$ and a proof of $x \in A$ and outputs a proof of $x \in B$ -- and similarly for $B \subseteq C$ and $A \subseteq C$. So, what the typical proof that you outlined does to construct this program is: given inputs $x : V$ and $HA : x \in A$, it first feeds $x$ and $HA$ into the input proving $A \subseteq B$ to get a proof of $HB : x \in B$; then, it feeds $x$ and $HB$ into the input proving $B \subseteq C$ to get $HC : x \in C$. In summary, the proof ends up transforming to the "program" $$ \lambda (A, B, C : V) (HAB : A \subseteq B) (HBC : B \subseteq C) . (\lambda (x : V) (HA : x \in A) . HBC(x, HAB(x, HA))). $$

Now, where I have been leading up to in this discussion is: the "programming language" for first-order logic allows for some types to be empty. On the other hand, you don't necessarily have to make special allowances for the possibility that one of the types might be empty in writing programs: as long as the proof "type-checks" then the corresponding program will automatically handle these cases correctly. So for example, if $A$ is an empty set, then for any $x : V$ then the type $x \in A$, consisting of all proofs that $x \in A$, will be an empty type; therefore, in this case it will not ever be possible for this function to be called since there is no possible input for the $HA$ parameter.

(On the other hand, the explosion principle mentioned in other answers corresponds to a family of operators $except_A : \bot \to A$, where $\bot$ is a canonical empty type and $A$ is an arbitrary type. What this means is: if at some point your program seems to be able to construct an element of the empty type $\bot$, then that means that branch of the code must be unreachable, so whatever type you're supposed to be returning from that part of the code, you can just return a synthetic value of that type in order to satisfy the type checker.)