Date: Jul 18, 2013 12:00 PM
Author: Dan Christensen
Subject: Re: Proposed Schema for Double Induction
(Correction)

Compare...

SCHEMA FOR ORDINARY INDUCTION

P(1)

& ALL(a):[a in N => [P(a) => P(a+1)]]

=> ALL(a):[a in N => P(a)]

where P is a unary predicate

SCHEMA FOR DOUBLE INDUCTION

P(1,1)

& ALL(a):[a in N => [P(1,a) => P(1,a+1)]]

& ALL(a):ALL(b):[a in N & b in N => [P(a,b) => P(a+1,b)]]

=> ALL(a):ALL(b):[a in N & b in N => P(a,b)]

where P is a binary predicate

Dan

Download my DC Proof 2.0 software at http://www.dcproof.com