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