A theorem concerning a restricted rule of substitution in the field of propositional calculi. I.
Bolesław Sobociński · Notre Dame Journal of Formal Logic · 1974
In this paper the rule of simultaneous substitution ordinarily used in the field of propositional calculi will be called restricted if, in the formalization of the given system, its applications are limited to the axioms of that system.So far as I know, A. Lindenbaum was the first who investigated an instance of this rule.Namely, around 1934 he informed me casually that there are some systems whose axiomatizations have a special structure of the bi-valued propositional calculus in which a replacement of the rule of simultaneous substitution by the restricted one does not affect the strength of these systems.Since Lindenbaum never published his research concerning this and related results, I have no idea exactly how his theorem was formulated and how it was proved.Much later, in [1], pp.148-151, section 27 (see especially p. 150), A. Church sketches a proof of a theorem which states that any system of the classical propositional calculus or any partial system of that calculus whose only rules of procedure are: detachment for implication and substitution (not necessarily simultaneous) may be reformulated into a system which has the same theorem as the original one and whose single rule of procedure is detachment.An inspection of Church's proof of this theorem shows that it holds simply through replacing each axiom of a system under consideration by the corresponding axiom schema.Since, certainly, Lindenbaum did not intend to reject the rule of substitution totally in formulating his theorem and, probably, he did not use the axiom schemata in the deductions which were needed for a proof of the theorem, the theorems discussed above are rather distinctly different.In this note we will prove the following theorem concerning the restricted rule of simultaneous substitution:Theorem A If (i) T is an arbitrary, consistent propositional system whose formalization satisfies the conditions: (a) The set of primitive notions of T contains at least the proposition