Search All of the Math Forum:

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

Topic: This is False. 0/0 {x | x ~e x} e {x | x ~e x} A single Principle

Replies: 53   Last Post: Feb 13, 2013 3:53 PM

 Messages: [ Previous | Next ]
 Charlie-Boo Posts: 1,609 Registered: 2/27/06
Re: This is False. 0/0 {x | x ~e x} e {x | x ~e x} A single Principle

Posted: Feb 5, 2013 9:10 AM

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

What does this say in English?

C-B

> Herc
>
> --www.BLoCKPROLOG.com

Date Subject Author
2/1/13 Graham Cooper
2/3/13 Charlie-Boo
2/3/13 Graham Cooper
2/3/13 Charlie-Boo
2/3/13 Graham Cooper
2/3/13 Graham Cooper
2/3/13 Charlie-Boo
2/3/13 Graham Cooper
2/3/13 Charlie-Boo
2/3/13 camgirls@hush.com
2/4/13 Charlie-Boo
2/4/13 billh04
2/4/13 Charlie-Boo
2/4/13 William Hale
2/4/13 Lord Androcles, Zeroth Earl of Medway
2/9/13 Graham Cooper
2/5/13 Charlie-Boo
2/4/13 Graham Cooper
2/5/13 Charlie-Boo
2/5/13 Graham Cooper
2/5/13 Brian Q. Hutchings
2/6/13 Graham Cooper
2/6/13 Charlie-Boo
2/4/13 fom
2/4/13 Charlie-Boo
2/4/13 fom
2/5/13 Charlie-Boo
2/7/13 fom
2/9/13 Charlie-Boo
2/9/13 Graham Cooper
2/11/13 Charlie-Boo
2/10/13 fom
2/10/13 Graham Cooper
2/10/13 fom
2/10/13 Graham Cooper
2/11/13 Charlie-Boo
2/11/13 Charlie-Boo
2/11/13 Charlie-Boo
2/11/13 Graham Cooper
2/13/13 Charlie-Boo
2/11/13 Charlie-Boo
2/11/13 fom
2/5/13 Charlie-Boo
2/5/13 fom
2/6/13 fom
2/11/13 Charlie-Boo
2/11/13 fom
2/13/13 Charlie-Boo
2/13/13 fom
2/4/13 Graham Cooper
2/4/13 Charlie-Boo
2/5/13 Charlie-Boo