well-founded induction

• To: types@theory.LCS.MIT.EDU
• Subject: well-founded induction
• From: lcp%computer-lab.cambridge.ac.uk@nss.cs.ucl.ac.uk
• Date: Tue, 24 Jan 89 09:20:24 EST
• Sender: meyer@theory.LCS.MIT.EDU

Date: Tue, 24 Jan 89 09:30:57 GMT
To: TYPES@theory.LCS.MIT.EDU

Is it practical to use a formal derivation of well-founded induction in
Church's higher-order logic?  E.g. define (with the obvious type symbols)

    WF(>) = there is no f such that for all n,  f(n)>f(n+1)

Then from the premises of wf induction

    WF(>)       forall x ( (forall y  x>y --> P(y))  -->  P(x) )

and the negated conclusion ~P(z) it follows that for some z1, z>z1 and ~P(z1),
and so on.  Use Hilbert's epsilon to define f.  Perhaps induction over the
naturals has to be assumed.

Is the full construction presented anywhere?

Larry

• Prev: Kripke lambda models
• Next: CCCs of Stable Domains
• Index(es):
  • Main
  • Thread