
Re: PREDICATE CALCULUS 2
Posted:
Nov 28, 2012 10:29 AM


On Nov 28, 9:36 am, Frederick Williams <freddywilli...@btinternet.com> wrote: > Irrelephant newsgroups removed. > > Dan Christensen wrote: > > 2. {x  ~x in x} cannot exist > > 3. {x  x=x} cannot exist > > Why? >
Well, since you asked...
The proof of both can be found the tutorial for my program:
Solution to Exercise 9.3 
Theorem 
The does not exit a set of all sets that are not elements of themselves.
~EXIST(r):ALL(a):[a @ r <=> ~a @ a]
Proof 
Define r such that...
1 ALL(a):[a @ r <=> ~a @ a] Premise
Applying the definition of r to r itself results in the contradiction...
2 r @ r <=> ~r @ r U Spec, 1
By contradiction, we have...
3 ~EXIST(r):ALL(a):[a @ r <=> ~a @ a] Conclusion, 1
Example 10 
Theorem 
The set of all things cannot exist.
~EXIST(s):[Set(s) & ALL(a):a@s]
Proof 
Suppose to the contrary...
1 Set(u) & ALL(a):a @ u Premise
2 Set(u) Split, 1
3 ALL(a):a @ u Split, 1
Apply the Subset Axiom for u
4 EXIST(sub):[Set(sub) & ALL(a):[a @ sub <=> a @ u & ~a @ a]] Subset, 2
Define: r, the subset of all things that are not elements of themselves.
5 Set(r) & ALL(a):[a @ r <=> a @ u & ~a @ a] E Spec, 4
6 Set(r) Split, 5
7 ALL(a):[a @ r <=> a @ u & ~a @ a] Split, 5
Apply the definition of r to itself
8 r @ r <=> r @ u & ~r @ r U Spec, 7
9 [r @ r => r @ u & ~r @ r] & [r @ u & ~r @ r => r @ r] IffAnd, 8
10 r @ r => r @ u & ~r @ r Split, 9
11 r @ u & ~r @ r => r @ r Split, 9
Prove: ~r @ r
Suppose to the contrary...
12 r @ r Premise
13 r @ u & ~r @ r Detach, 10, 12
14 r @ u Split, 13
15 ~r @ r Split, 13
Obtain the contradiction...
16 r @ r & ~r @ r Join, 12, 15
Apply the Conclusion Rule.
As Required:
17 ~r @ r Conclusion, 12
Apply the defintion of u to r
18 r @ u U Spec, 3
19 r @ u & ~r @ r Join, 18, 17
20 r @ r Detach, 11, 19
We obtain the contradicition...
21 ~r @ r & r @ r Join, 17, 20
Therefore, there cannot exist a set u as defined in the initial premise.
22 ~EXIST(u):[Set(u) & ALL(a):a @ u] Conclusion, 1
Dan Download my DC Proof 2.0 software at http://www.dcproof.com

