Date: Feb 17, 2013 4:35 PM
Author: Graham Cooper
Subject: Re: I Bet $25 to your $1 (PayPal) That You Can’t P<br>	rove Naive Set Theory Inconsistent

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