Subformulation property

From Encyclopedia of Mathematics
Jump to: navigation, search

subformula property

A property of certain logical calculi and logico-mathematical calculi (cf. Logical calculus; Logico-mathematical calculus), in which the premisses of each rule in the calculus consist of subformulas of the formulas occurring in the conclusion of the rule. The subformula property enables one to organize a "bottom-up" derivation search (see Gentzen formal system). To improve effectivity in such a search, various specializations and generalizations of the subformula property are used.



[a1] H. Schwichtenberg, "Some applications of cut-elimination" J. Barwise (ed.) , Handbook of mathematical logic , North-Holland (1977) pp. 867–896 (esp. 876)
[a2] E.W. Beth, "Formal methods" , Reidel (1962) pp. Sects. 27–28
[a3] S.C. Kleene, "Introduction to metamathematics" , North-Holland (1950) pp. 450
How to Cite This Entry:
Subformulation property. Encyclopedia of Mathematics. URL:
This article was adapted from an original article by S.Yu. Maslov (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article