Search All of the Math Forum:

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

Topic: 2nd-order mathematical induction as a derivable theorem
Replies: 2   Last Post: Mar 16, 2013 1:45 AM

 Graham Cooper Posts: 4,421 Registered: 5/20/10
Re: 2nd-order mathematical induction as a derivable theorem
Posted: Mar 16, 2013 1:45 AM

On Mar 16, 2:50 pm, Dan Christensen <Dan_Christen...@sympatico.ca>
wrote:
> On Saturday, March 16, 2013 12:31:35 AM UTC-4, fom wrote:
> > On 3/15/2013 11:22 PM, Dan Christensen wrote:
>
> > > Using my own ZF-like axioms, I can prove that, if we have an injective function f such that
>
> > >    f: s -> s /\ s1 in s /\ Ax in s (f(x)=/=s1)
>
> > > then there exists a unique subset of s on which all the Peano Axioms hold (including second order induction) with f as the successor function, and s1 as the "first element."
>
> > > See:http://www.dcproof.com/ProofByInduction.html(previously posted here)
>
> > > In this way, the principle of mathematical induction can actually be derived. The only set theoretic method I use in this proof is the construction of a subset of s (equivalent to specification in ZF), so it can probably be easily translated into a more standard ZF/FOL format. Comments?
>
> > > Dan
>
> > > Download my DC Proof 2.0 software athttp://www.dcproof.com
>
> > > Visit my new math blog athttp://www.dcproof.wordpress.com
>
> > Where are your ZF-like axioms?
>
> > I would like to see them.
>
> They are described in the user manual for my DC Proof freeware.
>
> In this particular proof they are invoked only on lines 8 (to construct n) and 130 (for set equality to show n = n').
>
> Dan
> Download my DC Proof 2.0 software athttp://www.dcproof.com
> Visit my new math blog athttp://www.dcproof.wordpress.com

INFORMAL OUTLINE
----------------

We construct n = {s1, f(s1), f(f(s1)), ... }

The usual axioms for the natural numbers, with f as the successor
function, are shown
here to apply on n:

N1: s1 e n (lines 12-21)

N2: ALL(a):[a e n => f(a) e n] (22-48)

N3: ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]] (49-70)

N4: ALL(a):[a e n => ~f(a)=s1] (71-81)

N5: ALL(b):[Set(b) (82-106)
& ALL(c):[c e b => c e n]
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n => c e b]]

N5 is Proof By Induction, usually more like:

p(0) & A(n) p(n)->p(n+1)
--> A(n) p(n)

-------------------

I should be able to get this running in PROLOG SET THEORY.

N5: ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s1 e b

nat(0)

or e(0,nats)

& ALL(c):[c e b => f(c) e b]

nat(s(C)) :- nat(C)

then probably

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

=> ALL(c):[c e n => c e b]]

ss(N,B)

-------------------

So despite Dan's extensive code to parse Quantified Logic...

he has resorted to using SUBSETS to simplify referencing quantified
predicates!

Herc

--
www.BLoCKPROLOG.com