Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

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


Math Forum » Discussions » sci.math.* » sci.math

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

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]
Dan Christensen

Posts: 2,799
Registered: 7/9/08
Re: PREDICATE CALCULUS 2
Posted: Nov 28, 2012 10:38 AM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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 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
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 contradiction...

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



Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.