Search All of the Math Forum:

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

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: PROVE ALL NATURALS ARE NOT EVEN! ~ALL(X) p(X) <-> EXIST(X) ~p(X)
Replies: 2   Last Post: Feb 23, 2013 10:50 PM

 Messages: [ Previous | Next ]
 Charlie-Boo Posts: 1,635 Registered: 2/27/06
Re: PROVE ALL NATURALS ARE NOT EVEN! ~ALL(X) p(X) <-> EXIST(X) ~p(X)
Posted: Feb 22, 2013 2:51 PM

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

> ~ALL(n):N div(n,2,0)
> -->
> !(subset(nats,evens))
>
> nat(0)
> nat(s(X)) <- nats(X)
>
> even(0)
> even(s(s(X))) <- even(X)
>
> odd(s(0))
> odd(s(s(X))) <- odd(X)
>
> !(odds) <- evens
> !(evens) <- odds
>
> **** DEFINE SETS AS PLURALS****
> e(X,nats) <- nat(X)
> e(X,evens) <- even(X)
> e(X,odds) <- odd(X)
>
> !(!(intersect(nats,!(evens))))
> intersect(nats,odds)
> e(X,nats) ^ e(X,odds)
> nats(X) ^ odds(X)
> nats(0) ^ odds(0) FAIL
> nats(s(0)) ^ odds(s(0))
>
> Basically it uses Set Reasoning instead of ALL(x) Logic
> and finds the counterexample Number 1!
>
> !(subset(S1,S2))
> <->
> intersect(S1,!(S2))
>
> Herc
> --www.BLoCKPROLOG.com

Date Subject Author
2/20/13 Graham Cooper
2/22/13 Charlie-Boo
2/23/13 Graham Cooper