|
|
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
|
|
