Abstract

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.

BibTeX

@article{MBGM-AML06,
  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"
}