Herbrand's theorem and term induction

We study the formal rst order system Tind in the standard language of Gentzen's LK. Tind extends LK by the purely logical rule of term-induction, that is a restricted induction principle, deriving numerals instead of arbitrary terms. This rule may be conceived as the logical image of full induction.

• Type: Journal
• Year: 2006
• Where: AML
• Authors: Matthias Baaz, Georg Moser
• Keywords: AML 2006, Formal Rst Order, Logical Rule, Restricted Induction Principle