
Re: Peanolike Axioms for the Integers in DC Proof
Posted:
Mar 3, 2013 6:13 PM


On Mar 1, 2:50 pm, Dan Christensen <Dan_Christen...@sympatico.ca> wrote: > On Thursday, February 28, 2013 7:20:42 PM UTC5, 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)
nat(0). nat(s(X)) < nat(X).

So although I cant formulate 2nd Order Induction
p(0) A(x) p(x) > p(s(x))  A(x) p(x)
because I can't refer to the inside of a general predicate p(..[X]..)
I can do Quantifier Style formulas in Sets instead, since the argument X is prestipulated here!
e(A, nats) < nat(A)

nat(A) is a 1OL predicate nats is a 2OL set

e.g. finite subset will be
ss( S1, S2 ) < e( @A , S1 ) , e( A , S2 )
intersection is
int( S1,S2) < e(A, S1) , e(A, S2)

So I can already do:
~ A(X) p(X) <> E(X) ~p(X)
with sets, without using Quantifier Syntax (referring to inside general predicates)
not(ss(S1,S2)) < int(S1, not(S2))
ss(S1,S2) is the same as ALL(X) XeS1 > XeS2
and I have negation of Sets also
e( A , not(evens) ) < e( A , odds)
So PROLOG can prove that NOT ALL NATS ARE EVEN by doing SetWise operations, then calling int( nats, odds) and returning s(0)
(a counterexample witness to the proof)

In Block Prolog, prefacing each VARAIBLE with @ will stand for ALL solutions for that variable.
So PREDICATE INDUCTION might be:
p @N p 0 if [p @N] [p [s N]]
@N means ALL(N) ... N...

or using an inference rule
if [ and [ [ p 0 ] [ if [ p @N ] [ p [s N] ] ] [ p @ N]

But these are 2OL, predicates are all lowercase terms, not Variables.
No Query will match a theorem or predicate with 'p'.
So I will try Induction with your SET FORMULA as it's a higher level
Then I will abandon infinite sets for the foreseeable future so Prolog can enumerate ALL(x) statements (which will be encoded as subset statements)
Herc  www.BLoCKPROLOG.com

