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).


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.


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.

  • 1
    $\begingroup$ Someone could have came along and said something like "uniform substitution can also get applied to theorems." Though, of course, the body of the text made it clear that this wouldn't answer what got asked. $\endgroup$ Commented Aug 27, 2016 at 17:33

3 Answers 3


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.

  • 2
    $\begingroup$ This seems more to the point than my old answer. I don't think it's right to say that Γ is the set of all propositional formulas? As far as I can tell, it is the set of assumptions forming the basis for a deduction. But that is a minor nit, really. I am puzzled by your choice of notation, though. Using Polish notation is one thing, but you seem to use C for implication? It took me a while to figure that out. What is wrong with good old ⇒, even in Polish notation, as in →pq? $\endgroup$ Commented Jun 15, 2013 at 20:54
  • $\begingroup$ I had to look up what Polish notation was, but is this what you mean? $1:\ \ (p\to q)$, $2:\ \ p\to(q\to p)$, $3: \ \ ((p\to(q\to p)))\to q$ (from 1 by mistaken uniform substitution $p$ / $p\to (q\to p)$ ). Then, from the deduction theorem, it would follow that $(p\to q)\to q$, and it's easy to verify that this is not a tautology. Is that it? $\endgroup$
    – favq
    Commented Jun 15, 2013 at 21:05
  • 1
    $\begingroup$ @anonymous Yes, that's it. $\endgroup$ Commented Jun 15, 2013 at 21:27
  • $\begingroup$ @HaraldHanche-Olsen C comes from the Polish term for "conditional", or at least the transation I have of Lukasiewicz's "Elementy logiki matematycznej" says "If the symbol C, introduced above, stands for an implication, the law can be written in the following form: CCpqCCqrCpr. This law is a conditional sentence..." Lukasiewicz and people who used Polish notation first used "C". If you want to use the arrow instead, go right ahead. It's not my preference, and I find using more conventional symbols in prefix notation less clear than Polish notation. I don't have this text, but... $\endgroup$ Commented Jun 16, 2013 at 23:47
  • 2
    $\begingroup$ @DougSpoonwood: It says that Γ is a set of formulae, or assumptions, or hypotheses. I think this is what Harald Hanche-Olsen was saying. It can be any arbitrary set of formulae, and the intention is to the derive logical consequences given these assumptions. This set of formulae is also called a theory by the authors. $\endgroup$
    – favq
    Commented Jun 17, 2013 at 0:17

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.

  • $\begingroup$ Thank you. To see if I understood: (1) Then, it is done to give axioms special treatment, but it wouldn't necessarily be logically incorrect to use uniform substitution to produce instances of formulas from $\Gamma$? (2) But what about instantiating theorems that were derived from formulas of $\Gamma$ by means of modus ponens? For example, if I have a formula $(A \to B) \in \Gamma$ and I deduce $B$ by modus ponens, am I allowed to instantiate $B$? $\endgroup$
    – favq
    Commented Jun 24, 2012 at 11:58
  • 4
    $\begingroup$ This isn't just a matter of keeping the number of inference rules down. As some other answers in the thread point out, this is an issue of soundness. Suppose that we assume $A$, and then by uniform substitution derive $B$. Then by the deduction theorem, $A \to B$ is a theorem, but this is clearly mistaken. Uniform substitution, in general, applies only to theorems. Within a proof that has assumptions, it is not necessary that each line is actually a theorem (because it may depend on an assumption), so uniform substitution isn't applicable. $\endgroup$ Commented Jun 15, 2013 at 19:21
  • $\begingroup$ Ah, that's an interesting point. Too bad I never saw the followup question from the OP last year; I guess summer vacation must have gotten in the way … $\endgroup$ Commented Jun 15, 2013 at 20:48
  • $\begingroup$ @HaraldHanche-Olsen: That's all right. $\endgroup$
    – favq
    Commented Jun 15, 2013 at 21:00
  • 1
    $\begingroup$ I notice that my answer here has gotten a downvote. That's fair enough I suppose, though I think the answer is more addressing the wrong issue than actually being wrong. But I don't want to delete it, if only to preserve the comment by @JoshuaTaylor above. $\endgroup$ Commented Jun 16, 2013 at 5:39

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.

  • 1
    $\begingroup$ I think you've implicitly used a definition of an axiom which makes them end up as just formulas, as opposed to a special "type" or "kind" of a formula. Usually when I see a set of axioms for a propositional calculus, each axiom qualifies as a tautology for the intended logical matrix. If all axioms of the system qualify as formulas according to the formation rules (and the formation rules don't result in ambiguity), and if each axiom qualifies as a tautology for the intended logical matrix, then uniform substitution can get applied to any of the axioms of the system. $\endgroup$ Commented Jul 25, 2013 at 21:51
  • $\begingroup$ Also, if A and B qualify as propositional variables in two-valued logic, does anyone use (A→B) as an axiom? I do understand that (A→B) that can qualify as a hypothesis (or assumption or supposition). But, an axiom in a development of two-valued propositional logic from what I see almost universally qualifies as a tautology also. So, axioms end up distinct from hypotheses in that hypotheses may hold true or may not hold true for the intended semantics, but on the other hand axioms definitely do hold true for the intended semantics. $\endgroup$ Commented Jul 25, 2013 at 22:06
  • $\begingroup$ An arbitrary theory may have arbitrary formulas as axioms. $\endgroup$ Commented Jul 26, 2013 at 1:42
  • $\begingroup$ What do you mean by an "arbitrary theory"? A complete system of two-valued propositional calculus is simply not arbitrary (the selection of two truth values can get regarded as arbitrary, and sure different axiom sets can work with different rules of inference can work). You can't, for instance, found such a theory with only a connective for logical conjunction with only the rule of conjunction-elimination. You can't found such a theory with only the axiom Cpp, modus ponens, and uniform substitution as rules of inference. So what do you mean by "arbitrary theory" here? $\endgroup$ Commented Jul 26, 2013 at 2:00
  • $\begingroup$ (A→B) makes for a perfectly good axiom for one-valued logic, and it should come as possible to derive (C→D) from that axiom. There do not exist any valuations where (A→B) is true and (C→D) false. It does qualify as sound to apply substitution to arbitrary wffs in one-valued logic. $\endgroup$ Commented Oct 1, 2013 at 0:21

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .