nLab rule C


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 (x)ϕ(x)(\exists x)\phi(x) then one introduces a new constant bb (“chosen xx”) and states ϕ(b)\phi(b). Then one continues proof and finally arrives at a new theorem not containing bb.

A basic metatheorem is that if a theorem not containing such a bb is provable with rule CC then it is provable without rule CC, written P CQP \vdash_C Q then PQP\vdash Q.


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

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

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.