```Date: Feb 23, 2013 10:50 PM
Author: Graham Cooper
Subject: Re: PROVE ALL NATURALS ARE NOT EVEN! ~ALL(X) p(X) <-> EXIST(X) ~p(X)

On Feb 23, 5:51 am, Charlie-Boo <shymath...@gmail.com> wrote:> On Feb 20, 5:51 am, Graham Cooper <grahamcoop...@gmail.com> wrote:>>BLOCK PROLOG is really coming along!>> > This proof outline uses>> > ~ALL(X)  p(X)  <->  EXIST(X)  ~p(X)>>  >  Now I can (automatically) prove that not all numbers are even!>> I liked the title better: PROVE ALL NATURALS ARE NOT EVEN!   Can you> do that?>> Now, here's how:>> P(N) = "All sets of N natural numbers contain only numbers that are> not even."  Proof (all x)P(x) by induction:>> P(0): {} contains only number that are not even.>> P(N) => P(N+1).  Given that all sets of N natural numbers contain only> non even numbers, consider any set of N+1 numbers.  Take all but one> of them.  That set has N numbers so they are not even.  Now remove one> element and add in the remaining number of the set of N+1 numbers.> Then it too is noneven and all numbers in sets of N+1 number are not> even.>> qed>> C-B>You can forward chain from an assumption to F^~F proof bycontradiction.This is a proof by counter-example which is a variation on standardmodus ponens proof by axiomatic derivation but negative valuedequalities are used to dispense with ALL(X) quantifiers since ALL(X)is an expensive operation, especially for infinite sets!The method is entirely simple rewording of the problem.ALL NATS ARE EVEN!ALL ELEMENTS OF N ARE EVENALL ELEMENTS OF N ARE ELEMENTS OF EVENSNATS C EVENS---------------------THEN the negative value equality is substituted with the even simplerSET INTERSECTION predicate.! (S1 C S2)   <->   S1 /\ !S2but what is a NEGATIVE SET  !S2 ??These are user-defined at the SET LEVEL!(odds) <- evens!(evens) <- odds-----------------Now all you need to do is find an intersection between NATS and ODDS!Which was my topic for today...INFINITE SETS IN PROLOGnat(0).nat(s(X)) :- nat(X).even(0).even(s(s(X))) :- even(X).odd(s(0)).odd(s(s(X))) :- odd(X).*** e is SET MEMBERSHIP ***e(A,nats) :- nat(A).e(A,evens) :- even(A).e(A,odds) :- odd(A).insect(S1,S2) :- e(A,S1), e(A,S2).?- insect(nats,odds).>>> > ~ALL(n):N div(n,2,0)> > -->> > !(subset(nats,evens))>Herc
```