
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

