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.