Sound rule

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.

Comments

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.

References

[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