Hostname: page-component-7c8c6479df-7qhmt Total loading time: 0 Render date: 2024-03-28T10:00:25.636Z Has data issue: false hasContentIssue false

Linear reasoning. A new form of the Herbrand-Gentzen theorem

Published online by Cambridge University Press:  12 March 2014

William Craig*
Affiliation:
The Pennsylvania State University

Extract

In Herbrand's Theorem [2] or Gentzen's Extended Hauptsatz [1], a certain relationship is asserted to hold between the structures of A and A′, whenever A implies A′ (i.e., A ⊃ A′ is valid) and moreover A is a conjunction and A′ an alternation of first-order formulas in prenex normal form. Unfortunately, the relationship is described in a roundabout way, by relating A and A′ to a quantifier-free tautology. One purpose of this paper is to provide a description which in certain respects is more direct. Roughly speaking, ascent to A ⊃ A′ from a quantifier-free level will be replaced by movement from A to A′ on the quantificational level. Each movement will be closely related to the ascent it replaces.

The new description makes use of a set L of rules of inference, the L-rules. L is complete in the sense that, if A is a conjunction and A′ an alternation of first-order formulas in prenex normal form, and if A ⊃ A′ is valid, then A′ can be obtained from A by an L-deduction, i.e., by applications of L-rules only. The distinctive feature of L is that each L-rule possesses two characteristics which, especially in combination, are desirable. First, each L-rule yields only conclusions implied by the premisses.

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 1957

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

BIBLIOGRAPHY

[1]Gentzen, G., Untersuchungen über das logische Schliessen, Mathematische Zeitschrift, vol. 39 (1934–1935), pp. 176–210, 405431.CrossRefGoogle Scholar
[2]Herbrand, J., Recherches sur la théorie de la démonstration, Travaux de la Société des Sciences et Lettres de Varsovie, Classe III sciences mathématiques et physiques, no. 33, 128 pp.Google Scholar
[3]Kleene, S. C., Introduction to metamathematics, Amsterdam (North Holland), Groningen (Noordhoff), New York and Toronto (van Nostrand), 1952, X + 550 pp.Google Scholar