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: SET THEORY and QUANTIFIER LOGIC are SUPERFLUOUS! You only need
1 or the other!

Replies: 8   Last Post: Nov 22, 2012 4:20 PM

 Messages: [ Previous | Next ]
 Graham Cooper Posts: 4,495 Registered: 5/20/10
Re: SET THEORY and QUANTIFIER LOGIC are SUPERFLUOUS! You only need 1
or the other!

Posted: Nov 22, 2012 4:17 PM

On Nov 23, 5:39 am, Dan Christensen <Dan_Christen...@sympatico.ca>
wrote:
> On Nov 20, 4:09 am, Graham Cooper <grahamcoop...@gmail.com> wrote:
>
>
>
>
>
>
>
>
>

> > The notation in
>
> > { x | p(x) }
>
> > stands for ALL VALUES OF x
> > that are satisfied in p(x)

>
> > This is the SAME 'ALL' as   ALL(x) ....predicate(..predicate...
> > x  ...) ...)

>
> > ALL is merely SUBSET!
>
> > ALL(n):N  n+1 > n
>
> > is just
>
> > { n | neN }  C  { n | n+1>n }
>
> How do you propose to do proof by induction e.g. prove 1+2+3+...+n =
> n(n+1)/2?
>

probably with an inference rule since I can range over predicates
using WFFT(..formula..)

I'm going to use

DEFN:
iand(X,Y,Z)

for

if( and(X,Y) , Z )

--------------

iand( if(X,Y) , if(Y,Z) , if(X,Z) )
this is the inference rule for transitive implication.

iand( t(X(0)) , if(X(n),X(s(n)), t(X(n) )

This needs work - it's high order PROLOG like that with a capital
(VAR) predicate name.

Let me think about whether I can use my SUBSET NOTATION to do this, or
have to hard code X as an argument like eval(TM, TAPE).

********************

This is a proof by Ghost In The Machine I'm interested in automating..

[1] If P(1) and P(i) => P(i+1), then P(n) for all n in N.
[2] If S is a subset of N, 1 is an element of S, and
(As)(s in S => (s+1) in S), then one can state S = N.

Herc

Date Subject Author
11/20/12 Graham Cooper
11/20/12 Frederick Williams
11/20/12 Charlie-Boo
11/20/12 Frederick Williams
11/22/12 Dan Christensen
11/22/12 Graham Cooper
11/22/12 Graham Cooper
11/22/12 Graham Cooper