
Re: Proposed Schema for Double Induction
Posted:
Jul 18, 2013 11:56 AM


Compare...
SCHEMA FOR ORDINARY INDUCTION
P(1) & ALL(a):[a in N => [P(a) => P(a+1)]] => ALL(a):[a in P => 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

