[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