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

I'm reading an introductory book about mathematical logic for Computation (just for reference, the book is "Lógica para Computação", by Corrêa da Silva, Finger & Melo), and would like to ask a question.

I'm currently reading the chapter that talks about deductive systems, and it begins with Axiomatization. More specifically, it talks about axiomatization as a form of logical inference, that is, an axiomatization of classical logic.

The book is in Portuguese, so all the quotes from it are translated to English.

Since I'm new to the subject, I'm not sure what I need to specify before asking the particular doubt, so I will put here some definitions and explanations that are given in the book (the context).

Context

Right before it presents an axiomatization of classical logic, it defines the concept of substitution:

The substitution of a formula B for an atom p, inside a formula A, is represented by $A[p:=B]$. Intuitively, if we have a formula $A=p\to(p\wedge q)$, and we want to substitute $(r\wedge s)$ for $p$, the result of the substitution is: $A[p:=(r\wedge s)]=(r\wedge s)\to((r\wedge s)\wedge q)$.

Then it defines an instance:

When a formula B results from the substitution of one or more atoms of a formula A, we say that B is an instance of the formula A

Then, it presents an axiomatization for classic propositional logic, which contains several axioms, including, for example, $p\to(q\to p)$ and $(p\to (q\to r))\to((p\to q)\to(p\to r))$. I'm not sure whether I should transcribe the whole set of axioms here, but I think it is not necessary (but I can detail it here if it is necessary).

The axiomatization also includes the rule of inference modus ponens: From $A\to B$ and $A$, one infers $B$.

Next, it states that axioms can be instantiated:

Axioms can be instantiated, that is, atoms can be uniformly substituted by any other formula of the logic. In this case, we say that the resulting formula is an instance of the axiom. With the notion of axiomatization, we can define the notion of deduction.

Definition 2.2.2 A deduction is a sequence of formulae $A_1,...,A_n$ such that every formula in the sequence is either an instance of an axiom, or is obtained from previous formulae by means of inference rules, that is, by modus ponens

A theorem $A$ is a formula such that there exists a deduction $A_1,...,A_n = A$. We represent a theorem as $\vdash_{\text{Ax}} A$ or simply $\vdash A$

Then, it says theorems can also be instantiated to produce new theorems:

The axiomatization presented here possesses the property of uniform substitution, that is, if A is a theorem and B is an instance of A, then B is also a theorem. The reason for that is very simple: if we can apply a substitution to obtain B from A, we can apply the same substitution in the formulas that occur in the deduction of A and, since any instance of an axiom is a deductible formula, we've transformed the deduction of A into a deduction of B.

Doubt

Now I will present the part of the text that generated doubt:

Now we will define when a formula $A$ is deductible from a set of formulae $\Gamma$, also called a theory or a set of hypotheses, which is represented by $\Gamma \vdash_{\text{Ax}} A$. In this case, this concerns adapting the notion of deduction to include the elements of $\Gamma$.

Definition 2.2.3 We say that a formula $A$ is deductible from the set of formulae $\Gamma$ if there is a deduction, that is, a sequence of formulae $A_1,...,A_n = A$ such that every formula $A_i$ in the sequence is:

1) either a formula $A_i \in \Gamma$

2) or an instance of an axiom

3) or is obtained from previous formulae by means of modus ponens.

[...] Note also that we cannot apply uniform substitution in the elements of $\Gamma$; uniform substitution can only be applied to the axioms of the logic.

This is the statement that I didn't understand: "Note also that we cannot apply uniform substitution to the elements of $\Gamma$; uniform substitution can only be applied to the axioms of the logic". Why is this particularly true? Since theorems can be instantiated, it seems that it should be possible to instantiate elements of $\Gamma$ too. Am I missing something?

Thank you in advance.

Solution 1:

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.

Solution 2:

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.

Solution 3:

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.