Sound rule

From Encyclopedia of Mathematics
Jump to: navigation, search

admissible rule

A derivation rule the addition of which to a calculus does not alter the collection of derivable formulas in this calculus. The introduction of a sound rule into a calculus is a powerful and frequently used method for abbreviating proofs, and is often useful in improving the algorithms for the establishment of derivability. One of the most important results in mathematical logic is the theorem stating that the cut rule is sound (see Gentzen formal system). See Deducible rule; Derived rule.


A (logical) theory is sound if everything provable in it is true, cf. [a2], [a3] for a discussion of the concept of a sound theory and related mathematical principles such as consistency, $\omega$-consistency, completeness and reflection principles.


[a1] R. Wojcicki, "Theory of logical calculi" , Kluwer (1988) pp. Chapt. 2
[a2] C. Smorinsky, "The incompleteness theorems" J. Barwise (ed.) , Handbook of mathematical logic , North-Holland (1977) pp. 821–865
[a3] W. Hodges, "Elementary predicate logic" D. Gabbay (ed.) F. Guenther (ed.) , Handbook of philosophical logic , I , Reidel (1983) pp. 1–132
How to Cite This Entry:
Sound rule. 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