Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

Views expressed in these public forums are not endorsed by Drexel University 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,295
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 <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)

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


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



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

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.