Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

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


Math Forum » Discussions » sci.math.* » sci.math

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

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]
Graham Cooper

Posts: 4,348
Registered: 5/20/10
PROVE ALL NATURALS ARE NOT EVEN! ~ALL(X) p(X) <-> EXIST(X) ~p(X)
Posted: Feb 20, 2013 5:51 AM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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!

~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



Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

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