A generalized theorem concerning a restricted rule of substitution in the field of propositional calculi.
Charles H. Lambros · Notre Dame Journal of Formal Logic · 1979
Sobociήski [1] proves that certain axiomatized systems of the propositional calculus having the rule of simultaneous substitution are not weakened in their deductive power by restricting the application of the substitution rule to the axioms alone.In his proof it is shown how a proof sequence employing only the rule of substitution and a rule of detachment may be uniquely and constructively replaced by a proof sequence to the same effect employing only the restricted rule.When the rule of detachment is the classical one, since classical systems require for their completeness no more than these two rules, Sobociήski's result is already a general one for classical systems.We further generalize the theorem to apply to any system (classical or not) containing any rules whatsoever.The only stipulation made (which we will express in a precise way at the appropriate time) is that such rules are "schematically representable".Theorem If T is an axiom system in the propositional calculus such that it contains