Rule C is a formal analogue in predicate logic of making a (single) choice when reasoning (in a line of logical proof). Thus, if one has a premise that $(\exists x)\phi(x)$ then one introduces a new constant $b$ (“chosen $x$”) and states $\phi(b)$. Then one continues proof and finally arrives at a new theorem not containing $b$.

A basic metatheorem is that if a theorem not containing such a $b$ is provable with rule $C$ then it is provable without rule $C$, written $P \vdash_C Q$ then $P\vdash Q$.

It seems that the rule is introduced in VI.7 of

- J. Barkley Rosser,
*Logic for mathematicians*, 1954

and is now more widely known from 2.6 in

- Elliott Mendelson,
*Introduction to mathematical logic*, Chapman and Hall 1964, 1979, 1987, 1997

See also a comment about the proof of the basic metatheorem at

- math.stackexchange:confusion-about-steps-of-proof-of-rule-c

category: logic

Created on November 2, 2022 at 12:01:26. See the history of this page for a list of all contributions to it.