On Mar 1, 2:50 pm, Dan Christensen <Dan_Christen...@sympatico.ca> wrote: > On Thursday, February 28, 2013 7:20:42 PM UTC-5, Graham Cooper wrote: > > [snip] > > > Ah ok. Can you post the proof of Induction formula or is it part of > > > the 1000 lines of formal stuff? > > I derived the induction formula for integers using well over 1,000 lines in the DC Proof format. In my previous thread here, I posted the text of a proof that derived the induction formula for natural numbers (only about 100 lines) starting with a single injective function defined on a set. > > I am currently trying to derive integer addition -- at least another 1,000 lines, and much more complicated. When (if?)I finish that, I will include all of these proofs in their entirety in the samples downloaded with DC Proof. I will also post key parts of it here and at my math blog for discussion. > > > > > I'm guessing you used Axiom Of Extensionality. > > So far, I haven't had to use what I call the Set Equality Axiom (Extensionality in ZFC) in these proofs. I'm guessing I won't need it. >
I'll see if I can work this set induction format into my Prolog set theory. for NATS.
14 ALL(p):[Set(p) & ALL(a):[a @ p => a @ z] & 0 @ p & ALL(a):[a @ p => next(a) @ p] & ALL(a):[a @ p => next'(a) @ p] => ALL(a):[a @ z => a @ p]]
And that will finish Infinite Sets in PROLOG as its not necessary for Logic in Natural Language
A(X) X e S <-> p(X)
Like NAIVE SET THEORY, I use
e(A, nats) <- nat(A)
Now I can refer to the predicate nat AND it's variable, as a Set (without the variable)