On Feb 4, 4:14 pm, Graham Cooper <grahamcoop...@gmail.com> wrote: > 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) )
What does that say in English?
> 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)"
And don't forget strings that imply it.
> 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