Subformulation property

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.

References

[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