Date: Feb 4, 2013 4:14 PM Author: Graham Cooper Subject: Re: This is False. 0/0 {x | x ~e x} e {x | x ~e x} A single Principle<br> to Resolve Several Paradoxes On Feb 4, 10:26 pm, Charlie-Boo <shymath...@gmail.com> wrote:

> If e(x,y) were a predicate then not(e(x,x)) would be a predicate but

> because of diagonalization it is not.

>

> What I believe about Prolog consists only of its being a database and

> query language similar to predicate calculus (aka FOL.)

>

> Then I take it that:

>

> if [ not [ e rs rs ]] [ e rs rs ] Line 1 X => rs

> if [ e rs rs ] [ not [ e rs rs ]] Line 2 X => rs

> [ not [ e rs rs ]] = = [ e rs rs ] Def = = , if

> ~P = = P [ e rs rs ]

> => P

>

> Then some axiom about ~P = = P.

Yes, something like

thm( X ) <- if( not(X), P ) ^ if( not(X), not(P) )

but this is forward chaining so it needs to be depth limited or PROLOG

will just recurse the first if(L,R) rule it finds!

>

> In Combinatory Logic:

>

> M x => N x x Def M

> M M => N M M x => M

>

> There is no M M = = N M M because it is executed (no Turing Machine

> can halt both yes and no because it stops as soon as it halts either

> cf Rosser 1936.) M M and N M M occur at different points in time!

> The system simply changes its mind as it goes along learning using AI

> techniques. The circle is amicable.

>

> In CBL:

>

> M # P(x) / Q(a,b) means program/wff M enumerates/represents set P and

> is written in programming language/logic Q meaning Q(x,y) iff program/

> wff M outputs at some point/is provable on input y. Then Q(M,x) = =

> P(x) (all x). Abbreviated M#P/Q means P=Q(M).

>

> P(x) / Q(a,b) means (exists M) M # P(x) / Q(a,b) There is a program/

> wff that enumerates/represents set P.

>

> Let SE(x,y) iff set x contains element y.

>

> Then the Russell Paradox is:

>

> ~SE(x,x) / SE(a,b) There is a set of all sets that do not contain

> themselves.

> M # ~SE(x,x) / SE(a,b) Let M be the set of all sets that do not

> contain themselves.

> SE(M,x) = = ~SE(x,x) Def # /

> SE(M,M) = = ~SE(M,M) x => M

> P = = ~P SE(M,M) => P

>

> This is encapsulated in axiom (lower level theorem) - ~P/P where - E

> means expression E is not true and P/Q abbreviates P(x)/Q(a,b) or

> P(x,x)/Q(a,b) if P is 2-place. Then if P/Q then P differs from Q and

> we prove truth, provability and unrefutability distinct (Godel,

> Rosser, Smullyan) - see 18 Word Proof in FOM July 2010.

>

> C-B

>

Sure you can syntactically eliminate strings like "~e(X,X)"

in NFU Set Theory.

I'm working on using

NOT( PROVABLE( T ) ) <-> DERIVE( NOT(T) )

EXISTS( SET( S ) ) <-> PROVABLE ( EXIST (SET (S) ) )

AXIOM OF SET SPECIFICATION

Herc

--

www.BLoCKPROLOG.com