Back to Search Start Over

Herbrand’s Theorem for a Modal Logic

Authors :
Melvin Fitting
Source :
Logic and Foundations of Mathematics ISBN: 9789048152018
Publication Year :
1999
Publisher :
Springer Netherlands, 1999.

Abstract

Herbrand’s theorem is a central fact about classical logic [9, 10]. It provides a constructive method for associating, with each first-order formula X, a sequence of formulas X 1, X 2, X 3,..., so that X has a first-order proof if and only if some X i is a tautology. Herbrand’s theorem serves as a constructive alternative to Godel’s completeness theorem. It provides the theoretical basis for automated theorem proving, reducing a first-order problem to a search through an infinite sequence of propositional problems [12]. It provides machinery for theoretical investigations [2]. But it does not travel well. Unlike Gentzen’s cut elimination theorem, or Godel’s completeness theorem, analogs of Herbrand’s result essentially do not exist for nonclassical logics.

Details

ISBN :
978-90-481-5201-8
ISBNs :
9789048152018
Database :
OpenAIRE
Journal :
Logic and Foundations of Mathematics ISBN: 9789048152018
Accession number :
edsair.doi...........ecf0972b329d3354d3a78a6d99527178