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

Replies: 8   Last Post: Nov 22, 2012 4:20 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
Re: SET THEORY and QUANTIFIER LOGIC are SUPERFLUOUS! You only need 1
or the other!

Posted: Nov 22, 2012 4:17 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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



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.