```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 ofthemselves.~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, 1By contradiction, we have...3	~EXIST(r):ALL(a):[a @ r <=> ~a @ a]	Conclusion, 1Example 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, 20Therefore, there cannot exist a set u as defined in theinitial premise.22	~EXIST(u):[Set(u) & ALL(a):a @ u]	Conclusion, 1DanDownload my DC Proof 2.0 software at http://www.dcproof.com
```