The Fallacy of the Undistributed Middle -- A Set Theoretic Approach

The classical form of this fallacy:

All p's are q's         (Major premise)
x is a q                (Minor premise)  
----------------
x is a p                (Conclusion)   


Here we prove a set theoretic version of the classical argument. We begin by 
postulating the existence of a non-empty set q with element x. Using the Subset
Axiom, we then construct a subset p of q that excludes x. Then we have:

ALL(d):[d ε p => d ε q]  (Major premise)
& x ε q                  (Minor premise)
& ~x ε p                 (The negation of the conclusion)

Thus, if there exists any non-empty set at all, we can construct an instance of
the major and minor premises being true and the conclusion being false. In this
way the fallacy is proven.

	
	Prove: 
	
	EXIST(s):EXIST(a):[Set(s) & a ε s]
	=> EXIST(a):EXIST(b):EXIST(c):[Set(a) & Set(b) 
	& ALL(d):[d ε a => d ε b] 
	& c ε b
	& ~c ε a]
	
	Suppose there exists a non-empty set.

	1	EXIST(s):EXIST(a):[Set(s) & a ε s]
		Premise

	2	EXIST(a):[Set(q) & a ε q]
		E Spec, 1

	Let q be a non-empty set with element x.

	3	Set(q) & x ε q
		E Spec, 2

	4	Set(q)
		Split, 3

	We have the minor premise...

	5	x ε q
		Split, 3

	Use the Subset Rule to construct a subset of q that excludes only the element x.

	6	EXIST(s):[Set(s) & ALL(a):[a ε s <=> a ε q & ~a=x]]
		Subset, 4

	Let p be a subset of q that excludes only the element x.

	7	Set(p) & ALL(a):[a ε p <=> a ε q & ~a=x]
		E Spec, 6

	8	Set(p)
		Split, 7

	9	ALL(a):[a ε p <=> a ε q & ~a=x]
		Split, 7

		Prove: k ε p => k ε q
		
		Suppose...

		10	k ε p
			Premise

		Apply the definition of p.

		11	k ε p <=> k ε q & ~k=x
			U Spec, 9

		12	[k ε p => k ε q & ~k=x] & [k ε q & ~k=x => k ε p]
			Iff-And, 11

		13	k ε p => k ε q & ~k=x
			Split, 12

		14	k ε q & ~k=x => k ε p
			Split, 12

		15	k ε q & ~k=x
			Detach, 13, 10

		16	k ε q
			Split, 15

	From the definition of p...

	17	k ε p => k ε q
		Conclusion, 10
	Generalizing, we obtain the major premise...

	18	ALL(d):[d ε p => d ε q]
		U Gen, 17

		Prove: ~x ε p
		
		Suppose to the contrary...

		19	x ε p
			Premise

		Apply the defintion of p.

		20	x ε p <=> x ε q & ~x=x
			U Spec, 9

		21	[x ε p => x ε q & ~x=x] & [x ε q & ~x=x => x ε p]
			Iff-And, 20

		22	x ε p => x ε q & ~x=x
			Split, 21

		23	x ε q & ~x=x => x ε p
			Split, 21

		24	x ε q & ~x=x
			Detach, 22, 19

		25	x ε q
			Split, 24

		26	~x=x
			Split, 24

		27	x=x
			Reflex

		We obtain the contradiction...

		28	~x=x & x=x
			Join, 26, 27

	By contradiction, we obtain the negation of the conclusion in the original syllogism...

	29	~x ε p
		Conclusion, 19
	Combining results...

	30	Set(p) & Set(q)
		Join, 8, 4

	31	Set(p) & Set(q) & ALL(d):[d ε p => d ε q]
		Join, 30, 18

	32	Set(p) & Set(q) & ALL(d):[d ε p => d ε q] & x ε q
		Join, 31, 5

	33	Set(p) & Set(q) & ALL(d):[d ε p => d ε q] & x ε q
		& ~x ε p
		Join, 32, 29

	Generalizing...

	34	EXIST(c):[Set(p) & Set(q) & ALL(d):[d ε p => d ε q] & c ε q
		& ~c ε p]
		E Gen, 33

	35	EXIST(b):EXIST(c):[Set(p) & Set(b) & ALL(d):[d ε p => d ε b] & c ε b
		& ~c ε p]
		E Gen, 34

	36	EXIST(a):EXIST(b):EXIST(c):[Set(a) & Set(b) & ALL(d):[d ε a => d ε b] & c ε b
		& ~c ε a]
		E Gen, 35

As Required:

37	EXIST(s):EXIST(a):[Set(s) & a ε s]
	=> EXIST(a):EXIST(b):EXIST(c):[Set(a) & Set(b) & ALL(d):[d ε a => d ε b] & c ε b
	& ~c ε a]
	Conclusion, 1