Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
Drexel University or The Math Forum.



Re: 2ndorder 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 UTC4, fom wrote: > > On 3/15/2013 11:22 PM, Dan Christensen wrote: > > > > Using my own ZFlike 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 ZFlike 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
[DANS LINK]
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 1221)
N2: ALL(a):[a e n => f(a) e n] (2248)
N3: ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]] (4970)
N4: ALL(a):[a e n => ~f(a)=s1] (7181)
N5: ALL(b):[Set(b) (82106) & 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



