Search All of the Math Forum:

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

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: Peano-like Axioms for the Integers in DC Proof
Replies: 11   Last Post: Mar 3, 2013 6:13 PM

 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

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

Date Subject Author
2/23/13 Graham Cooper
2/24/13 Graham Cooper
2/24/13 Graham Cooper
2/28/13 Graham Cooper
3/3/13 Graham Cooper
2/24/13 Graham Cooper