[Prev][Next][Index][Thread]

well-founded induction



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