Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
Drexel University or The Math Forum.
|
|
|
|
Re: PROVE ALL NATURALS ARE NOT EVEN! ~ALL(X) p(X) <-> EXIST(X) ~p(X)
Posted:
Feb 23, 2013 10:50 PM
|
|
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 by
contradiction.
This is a proof by counter-example which is a variation on standard
modus ponens proof by axiomatic derivation but negative valued
equalities 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 EVEN
ALL ELEMENTS OF N ARE ELEMENTS OF EVENS
NATS C EVENS
---------------------
THEN the negative value equality is substituted with the even simpler
SET INTERSECTION predicate.
! (S1 C S2) <-> S1 /\ !S2
but 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 PROLOG
nat(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
|
|
|
|
