Search All of the Math Forum:

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

Topic: I Bet \$25 to your \$1 (PayPal) That You Can’t P
rove Naive Set Theory Inconsistent

Replies: 7   Last Post: Feb 18, 2013 1:48 PM

 Search Thread: Advanced Search

 Messages: [ Previous | Next ]
 Graham Cooper Posts: 4,045 Registered: 5/20/10
Re: I Bet \$25 to your \$1 (PayPal) That You Can’t P
rove Naive Set Theory Inconsistent

Posted: Feb 17, 2013 4:35 PM
 Plain Text Reply

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

Date Subject Author
2/17/13 Graham Cooper
2/17/13 Charlie-Boo
2/17/13 Graham Cooper
2/17/13 Charlie-Boo
2/17/13 Bernice Barnett
2/17/13 Charlie-Boo
2/18/13 fom

© Drexel University 1994-2013. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.