Herbrand’s Theorem and Term Induction

Matthias Baaz and Georg Moser

Archive for Mathematical Logic 45(4), pp. 447 – 503, 2006.


We study the formal first 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.


  PDF |    doi:10.1007/s00153-005-0327-6  |  © Springer


author = "Matthias Baaz and Georg Moser",
title = "Herbrand's Theorem and Term Induction",
journal = "Archive for Mathematical Logic",
volume = 45,
number = 4,
year = 2006,
pages = "447--503"
Nach oben scrollen