The Math Forum

Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Math Forum » Discussions » sci.math.* » sci.math

Topic: Peano-like Axioms for the Integers in DC Proof
Replies: 11   Last Post: Mar 3, 2013 6:13 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,495
Registered: 5/20/10
Re: Peano-like Axioms for the Integers in DC Proof
Posted: Mar 3, 2013 6:13 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

On Mar 1, 2:50 pm, Dan Christensen <>
> 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

X e S <-> p(X)


e(A, nats) <- nat(A)

Now I can refer to the predicate nat AND it's variable, as a Set
(without the variable)

nat(s(X)) <- nat(X).


So although I cant formulate 2nd Order Induction

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 pre-stipulated 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)

by doing SetWise operations, then calling
int( nats, odds)
and returning

(a counterexample witness to the proof)


In Block Prolog, prefacing each VARAIBLE with @ will stand for ALL
solutions for that variable.


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


Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© The Math Forum at NCTM 1994-2017. All Rights Reserved.