THEOREM

*******

For any set x and proposition P, ALL(a):[a e x & P] is always false.

ALL(x):[Set(x) => ~ALL(a):[a e x & P]]

Dan Christensen

2023-04-24

http://dcproof.com

PROOF

*****

Lemma: From Russel's Paradox (Proof: http://dcproof.com/UniversalSet.htm)

1 ALL(a):[Set(a) => EXIST(b):~b e a]

Axiom

Let x be a set

2 Set(x)

Premise

Apply lemma

3 Set(x) => EXIST(b):~b e x

U Spec, 1

4 EXIST(b):~b e x

Detach, 3, 2

5 ~y e x

E Spec, 4

6 ~y e x | ~P

Arb Or, 5

7 ~[~~y e x & ~~P]

DeMorgan, 6

8 ~[y e x & ~~P]

Rem DNeg, 7

9 ~[y e x & P]

Rem DNeg, 8

As Required:

10 ALL(x):[Set(x) => EXIST(a):~[a e x & P]]

4 Conclusion, 2

Switch quantifier

11 ALL(x):[Set(x) => ~ALL(a):~~[a e x & P]]

Quant, 10

As Required:

12 ALL(x):[Set(x) => ~ALL(a):[a e x & P]]

Rem DNeg, 11