|
|
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
|
|
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
|
|
