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