Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Topic: PREDICATE CALCULUS 2
Replies: 23   Last Post: Nov 29, 2012 1:13 AM

 Messages: [ Previous | Next ]
 Dan Christensen Posts: 6,760 Registered: 7/9/08
Re: PREDICATE CALCULUS 2
Posted: Nov 28, 2012 10:38 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?
>
> --

The proof of both can be found in the tutorial for my program:

Solution to Exercise 9.3
------------------------

Theorem
-------

There 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

2 r @ r <=> ~r @ r
U Spec, 1

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

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

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

Date Subject Author
11/25/12 Graham Cooper
11/27/12 Dan Christensen
11/27/12 Graham Cooper
11/27/12 Dan Christensen
11/27/12 Dan Christensen
11/27/12 Dan Christensen
11/27/12 Graham Cooper
11/27/12 Graham Cooper
11/27/12 Graham Cooper
11/27/12 Dan Christensen
11/28/12 Graham Cooper
11/28/12 Dan Christensen
11/28/12 Graham Cooper
11/28/12 Virgil
11/28/12 Dan Christensen
11/28/12 Graham Cooper
11/28/12 Dan Christensen
11/28/12 Graham Cooper
11/28/12 Dan Christensen
11/29/12 Graham Cooper
11/29/12 Dan Christensen
11/28/12 Frederick Williams
11/28/12 Dan Christensen
11/28/12 Dan Christensen