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