Date: Nov 28, 2012 10:29 AM
Author: Dan Christensen
Subject: Re: PREDICATE CALCULUS 2
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]
Iff-And, 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