|
|
Re: I Bet $25 to your $1 (PayPal) That You Can’t P
rove Naive Set Theory Inconsistent
Posted:
Feb 17, 2013 6:07 PM
|
|
On Feb 18, 8:17 am, Charlie-Boo <shymath...@gmail.com> wrote:
> On Feb 17, 4:35 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
>
>
>
>
>
>
>
>
>
> > On Feb 16, 7:56 am, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > > Agreement:
>
> > > I, the owner of email account shymathgu...@aol.com, do hereby agree to
> > > wager $25 against $1 from anyone, payable through PayPal, that they
> > > cannot prove Naïve Set Theory inconsistent, subject to the condition
> > > that the person states here that they enter into this wager within 24
> > > hours after this offer appears and they are the first to give their
> > > proof as part of this wager.
>
> > > C-B
>
> > Here is a Small Depth Limited Formal Set Theory in PROLOG!
>
> > *** t( THEOREM , LEVEL ) ***
>
> > t(1,z(1)).
> > not(0).
>
> > *** PREDICATE CONSTRUCTION ***
>
> > if( and(X,Y) , or(X,Y) ).
> > if( and(not(X),Y) , or(X,Y) ).
> > if( and(X,not(Y)) , or(X,Y) ).
> > if( and(not(X),not(Y)) , not(or(X,Y)) ).
>
> > if( and(not(X),not(Y)) , not(and(X,Y)) ).
> > if( and(not(X),Y) , not(and(X,Y)) ).
> > if( and(X,not(Y)) , not(and(X,Y)) ).
>
> > if( and(X,Y) , if(X,Y) ).
> > if( and(not(X),not(Y)) , if(X,Y) ).
> > if( and(not(X),Y) , if(X,Y) ).
> > if( and(X,not(Y)) , not(if(X,Y)) ).
>
> > if( and(X,Y) , iff(X,Y) ).
> > if( and(not(X),not(Y)) , iff(X,Y) ).
> > if( and(not(X),Y) , not(iff(X,Y)) ).
> > if( and(X,not(Y)) , not(iff(X,Y)) ).
>
> > *** NEGATION ***
>
> > if( not(and(X,Y)) , or(not(X),not(Y)) ).
> > if( not(or(X,Y)) , and(not(X),not(Y)) ).
> > if( not(xor(X,Y)) , iff(X,Y) ).
> > if( not(not(X)) , X ).
> > if( X , not(not(X)) ).
>
> > *** TRANSITIVE RELATIONS ***
>
> > if( and(if(A,B),if(B,C)) , if(A,C) ).
> > if( and(or(A,B),if(B,C)) , or(A,C) ).
> > if( and(and(A,B),if(B,C)) , and(A,C) ).
>
> > *** ASSOCIATIVE RELATIONS ***
>
> > if( and(A,B) , and(B,A) ).
> > if( or(A,B) , or(B,A) ).
>
> > *** THEOREMHOOD ***
>
> > t(if(X,Y),z(1)) :- if(X,Y).
> > t(not(X),z(1)) :- not(X).
> > t(X,z(Z)) :- t(X,Z).
>
> > *** CARTESIAN JOIN ON THEOREM PAIRS ***
>
> > t( and(X,Y) , z(Z)) :- t(X,Z), t(Y,Z).
> > t( and(X,not(Y)) , z(Z)) :- t(X,Z), not(Y).
> > t( and(not(X),Y) , z(Z)) :- not(X), t(Y,Z).
> > t( and(not(X),not(Y)) , z(Z)) :- not(X), not(Y).
>
> > *** SETHOOD ***
>
> > t(e(A,B),z(1)) :- e(A,B).
>
> > *** DEMO SET ***
>
> > if( e(X,X) , e(X,selfish) ).
> > e( ideas, abstract ).
> > e( abstract, abstract ).
> > e( dog, animals ).
> > e( cat, animals ).
>
> > *** ARITHMETIC ***
>
> > add(1,2,3).
>
> > t(add(M,N,S),z(1)) :- add(M,N,S).
> > t(bigger(N,M),z(1)) :- bigger(N,M).
> > if( bigger(N,M) , not(bigger(M,N)) ).
> > if( not(bigger(N,M)) , bigger(M,N) ).
> > if( add(M,N,SUM) , bigger(SUM,M) ).
> > if( add(M,N,SUM) , bigger(SUM,N) ).
> > if( add(M,N,SUM) , add(N,M,SUM) ).
>
> > *** MODUS PONENS ***
>
> > t(R,z(Z)) :- if(L,R) , t(L,Z).
>
> > *** DEMO QUERIES ***
>
> > ?- t( e(X,selfish) , z(z(1)) ).
>
> > if( not(e(X,X)) , e(X,rusl) ).
> > if( e(X,russell) , not(e(X,X)) ).
>
> > not(e(rusl,rusl)).
>
> > ?- t( not(e(rusl,rusl)) , z(1) ).
> > ?- t( e(rusl,rusl) , z(z(1)) ).
>
> > ************************
>
> > The output is:
>
> > abstract
> > YES
> > YES
>
> > e.g. the last 2 queries
>
> > ?- t( not(e(rusl,rusl)) , z(1) ).
>
> > READS: Is it a theorem that russells set is not an element of
> > russells set with 1 deduction?
>
> > YES
>
> > ?- t( e(rusl,rusl) , z(z(1)) ).
>
> > READS: Is it a theorem that russells set is an element of russells set
> > with 2 or less deductions?
>
> > YES
>
> > Therefore
>
> > |- rusl e rusl
> > AND
> > |- not( rusl e rusl)
>
> > which satisifies the conditions of an Inconsistent System!
>
> > Herc
> > --
>
> > Next Week : Proving 1+1=4 in an Inconsistent System!www.BLoCKPROLOG,.com
>
> Yes, there is no set of sets that don't contain themselves - the proof
> is 3-4 lines long. But NST doesn't imply that there is.
>
> C-B
Is any definable collection a set?
That is the usual meaning of Naive Set Theory.
EXIST(S) ALL(x) xeS <-> d(x)
for all WFF d
*** RUSSELLS SET ***
if( not(e(X,X)) , e(X,rusl) ).
if( e(X,russell) , not(e(X,X)) ).
Since not(e(X,X)) is a WFF rusl is a SET
Herc
--
www.BLoCKPROLOG.com
|
|
