In axiomatization of propositional logic, why can uniform substitution be applied only to axioms?

If you did that at least in the way the author understands, the theory would no longer come as sound.

Note that the definition of the set Γ doesn't say anything about its members as axioms or coming as derivable from the axioms. The first clause of definition 2.2.3 says "a formula A$_i$∈Γ" What is Γ? The text says "the set of formulae Γ". The author doesn't clarify, but it does work out that Γ can be any finite subset of the set of all propositional formulas. So, yes you can apply uniform substitution to an element, or even some elements of Γ provided that those element(s) you apply uniform substitution to qualify as either an axiom, a theorem, or the negation of a theorem. But, you can't apply uniform substitution to all elements of Γ without mangling things. More specifically, uniform substitution in terms of deductions can't get applied to semantic contingencies.

Examples of how you might apply uniform substitution to elements of Γ. Suppose Γ contains only C-Kpq-q and K.Kpq.r as formulas (the "-"s and "."s are informal punctuation marks to hopefully make these formulas easier to read... K stands for logical conjunction, C for the material conditional here and I use Polish notation). Then we can write a deduction like this:

  • K.Kpq.r -----hyothesis 1
    • C-Kpq-q -----hypothesis 2
    • C-K.Kpq.r-r -----2 p/Kpq, q/r 3
    • r -----1, 3 conditional-out 4
  • C-C.Kpq.q-r -----2-4 conditional-in 5

$\vdash$C-KKpqr-C.CKpqq.r -----1-5 conditional introduction 6

Suppose we have C-p-C.Cpq.q and C-Cpq-C.Cqr.Cpr, and C.CCpqq.r as hypotheses. Then we can write a deduction like this:

  • C-p-C.Cpq.q -----hypothesis 1
    • C-Cpq-C.Cqr.Cpr -----hypothesis 2
      • C.CCpqq.r -----hypothesis 3
      • C-C p CCpqq-C.C CCpqq r.Cpr -----2 q/CCpqq 4
      • C.C CCpqq r.Cpr -----1, 4 conditional-out 5
      • Cpr -----3, 5 conditional-out, 6
    • C.CCCpqqr.Cpr -----3-6 conditional-in 7
  • C.CCpqCCqrCpr.CCCCpqqrCpr -----2-7 conditional-in 8

$\vdash$C-CpCCpqq-C.CCpqCCqrCpr.C:CCCpqqr:Cpr -----1-8 conditional-in 9

Suppose we have K-p-Np (the negation of a theorem), C-Kpq-p (a theorem), and q (a contingent proposition) as hypotheses. Then we can write:

  • p -------hypothesis 1
    • C-Kpq-p ------ hypothesis 2
      • K-p-Np -------hypothesis 3
      • K-Cpq-NCpq ------- 3, p/Cpq 4
      • C-KCpqNCpq-Cpq ----- 2, p/Cpq, q/NCpq 5
      • Cpq ------- 2, 3 conditional-out 6
    • C-KpNp-Cpq ------3-6 conditional-in 7
  • C-CKpqp-C.KpNp.Cpq ------2-7 conditional-in 8

$\vdash$C-p-C.CKpqp.C:KpNp:Cpq ------1-8 conditional-in 9

Now suppose you were to apply uniform substitution to any possible permissible element of Γ. Then, it would become possible to write deductions like the following:

 1 C   p   q  |hypothesis
 2   CaCba    |axiom
 3 C CaCba q  |1 p/CaCba, q/q where "x/y" indicates x has gotten substituted by y
 4 q          |2, 3 modus ponens

Since that system has the deduction meta-theorem (or equivalently conditional introduction), it follows that CCpqq would become a theorem in propositional calculus. But, if p is false and q is false, then CCpqq=CC000=C10=0. Consequently, such a theory would no longer come as sound. Also, you would have inference rules whereby you could "prove" the consequent of a conditional from the conditional itself.

Added: You can apply uniform substitution to contradictions given the deduction metatheorem, and not mangle things since contradictions are false for all interpretations. Contradictions always take on a designated value. Thus, any substitution instance of a contradiction is false also. So, when you discharge any introduced contradictions by conditional introduction, you'll end up with a tautology of classical propositional logic, and thus soundness holds.

Added: There does exist something of another exception, if the author were to introduce propositional logic with quantifiers. St. Jaskowski's original paper The Rules of Supposition in Formal Logic on what we call "natural deduction" has a substitution rule when you have what we call a universal quantifier under special conditions.


It is done to keep the number of inference rules down to a minimum, in order to be able to reason more easily about theorems and deductions. The axioms need special treatment in order to have a sufficiently rich theory.

It is more common practice (I think) to talk about axiom schemas, which are infinite sets of axioms – corresponding to what your book calls instances of an axiom.

One important feature is that it must be effectively decidable whether or not a given formula is an (instance of an) axiom or not.


If $A \to B$ is an axiom, it should not be possible to derive $C \to D$; there are valuations in which the former is true and the latter is false. But, the latter is a substitution instance of the former. Thus it is not sound to apply substitution to arbitrary axioms.