
Re: Double Induction  A brief note that may help
Posted:
Jul 15, 2013 10:22 PM


On Monday, July 15, 2013 8:22:09 PM UTC4, David Melik wrote: > On Mon, 15 Jul 2013 13:50:39 0700 (PDT) > > Dan Christensen <Dan_Christensen@sympatico.ca> wrote: > > > > > The explanations of double induction online can be quite confusing. > > > No doubt I am reinventing wheel here, but you may find the following > > > analogy to ordinary induction to be useful. > > > > > > With ordinary induction, we want to prove that for all x in N, we > > > have P(x) where P is a unary predicate. > > > > > > With double induction, we want to prove that for all x, y in N, we > > > have P(x,y) where P is a binary predicate. > > > > > > 1. Base case: > > > > > > Ordinary induction: Prove P(1) > > > > > > Double induction: Prove P(1,1) > > > > > > 2. Inductive step: > > > > > > Ordinary induction: For x in N, assume P(x) and prove P(x+1) > > > > > > Double induction: For x, y in N, assume P(x,y) and prove P(x+1,y) > > > and P(x,y+1). > > > > > > Comments? > > > > > > Sounds like an interesting idea... is there an example proof somewhere?
I have a formal proof of the concept starting from Peanolike axioms (163 lines) using my DC Proof system. I am working on some sample applications. I hope to post them here over the next week or so.
Dan Download my DC Proof 2.0 software at http://www.dcproof.com

