3
$\begingroup$

From "An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof" by Peter B. Andrews:


1101 Rule of Substitution (Sub). If $\mathcal{H} \vdash A$, and if $p_{1}, \ldots, p_{n}$ are distinct variables which do not occur in any wff in $\mathcal{H}$, then $\mathcal{H} \vdash S_{B_{1} \ldots B_{n}}^{p_{1} \ldots p_{n}} A$.

Proof: Let $\theta$ be the substitution $S_{B_{1} \ldots B_{n}}^{p_{1} \ldots p_{n}}$. It is easy to see that if $C_{1}, \ldots, C_{m}$ is a proof of $A$ from $\mathcal{H}$, then $\theta C_{1}, \ldots, \theta C_{m}$ is a proof of $\theta A$ from $\mathcal{H}$. Note how the condition on the variables comes into play when $C_{i}$ is a member of $\mathcal{H}$.

Of course, the sentence above is really a rather brief sketch of a proof of this metatheorem. For a more complete proof, show by complete induction on $i$ that $\mathcal{H} \vdash \theta C_{i}$ for each $i$ with $1 \leq i \leq m$. Break the proof into cases according to how $C_{i}$ was justfied in the original proof.


I am confused as to why induction is necessary for this proof. It seems that since we have shown the case for an arbitrary natural number $m$, that it holds for all natural numbers $m$. If I expand the given proof:

Proof: Let $m$ be any natural number. Suppose that $C_{1}, \ldots, C_{m}$ is a proof from $\mathcal{H}$. We will show that $\theta C_{1}, \ldots, \theta C_{m}$ is a proof from $\mathcal{H}$. Let $j$ be any natural number such that $1 \leq j \leq m$. Then either (1) $C_{j}$ is an axiom, (2) $C_{j}$ is a member of $\mathcal{H}$, or (3) there exist $i < j$ and $k < j$ such that $C_{k}$ is $[C_{i} \to C_{j}]$. Suppose $C_{j}$ is an axiom. Then $\theta C_{j}$ is an axiom. Suppose $C_{j}$ is a member of $\mathcal{H}$. Then $\theta C_{j} = C_{j}$ and hence $\theta C_{j}$ is a member of $\mathcal{H}$. Suppose there exist $i < j$ and $k < j$ such that $C_{k}$ is $[C_{i} \to C_{j}]$. Then $\theta C_{k} = \theta [C_{i} \to C_{j}] = [\theta C_{i} \to \theta C_{j}]$. Hence there exist $i < j$ and $k < j$ such that $\theta C_{k}$ is $[\theta C_{i} \to \theta C_{j}]$. Hence $\theta C_{1}, \ldots, \theta C_{m}$ is a proof from $\mathcal{H}$.

Then suppose $\mathcal{H} \vdash A$. Then for some natural number $m$ there is a proof $C_{1}, \ldots, C_{m}$ of $A$ from $\mathcal{H}$. Then $\theta C_{1}, \ldots, \theta C_{m}$ is a proof of $\theta A$ from $\mathcal{H}$. Hence $\mathcal{H} \vdash \theta A$.

EDIT:

The text also states: A proof of a wff $B$ from the set $\mathcal{H}$ of hypotheses is a finite sequence $B_{1}, \ldots, B_{m}$ of wffs such that $B_{m}$ is $B$ and for each $j$ $(1 \leq j \leq m)$ at least one of the following conditions is satisfied: (1) $B_{j}$ is an axiom. (2) $B_{j}$ is a member of $\mathcal{H}$. (3) $B_{j}$ is inferred by Modus Ponens from wffs $B_{i}$ and $B_{k}$, where $i < j$ and $k < j$. An alternative way of expressing condition (3) is to say that there exist $i < j$ and $k < j$ such that $B_{k}$ is $[B_{i} \to B_{j}]$.

$\endgroup$
13
  • 1
    $\begingroup$ The author actually gives two methods for proving the theorem, one by induction and one using the formation sequence definition of proof. You elaborated the sequence version, which does not require induction because the objects of study already have the induction "baked in" so to speak. The alternate characterization takes $\mathcal{H}\vdash$ to be the least relation containing the axioms, such that $\mathcal{H}\vdash A$ and $\mathcal{H}\vdash A\to B$ implies $\mathcal{H}\vdash B$. With this definition an inductive proof is natural (and simpler to some extent than the sequence version). $\endgroup$ Commented Apr 13, 2018 at 2:43
  • $\begingroup$ @MarioCarneiro I see. I got the impression from "for a more complete proof" that what he had given was lacking and that induction was required to complete it. This has gotten me thinking about whether induction is required in other metatheorems, like the deduction theorem, as well. $\endgroup$
    – user695931
    Commented Apr 13, 2018 at 3:50
  • $\begingroup$ @MarioCarneiro I emailed the author to be certain and it turns out that he believes that any rigorous proof of this metatheorem will involve some form of induction. $\endgroup$
    – user695931
    Commented Apr 21, 2018 at 18:38
  • $\begingroup$ @MarioCarneiro What would it take to formally prove the sequence version? Is it likely that this is already done? $\endgroup$
    – user695931
    Commented Apr 25, 2018 at 2:54
  • $\begingroup$ I don't think stressing about whether the proof uses induction or not is relevant. You gave a proof (the sequence proof as I put it), and it's perfectly fine as it is, and that's all that matters. Unless you mean something else by formal proof... $\endgroup$ Commented Apr 25, 2018 at 17:17

1 Answer 1

3
$\begingroup$

In (3) you are forgetting an important thing: the formula $C_i$ must either be an axiom, an hypothesis in $\mathcal H$ or an already proven proposition, that is that $C_1,\dots,C_i$ is a valid proof.

Hence in order to prove that the sequence $\theta C_1,\dots, \theta C_n$ is the valid proof you have to prove inductively that for all those $C_i$'s that are neither axioms or hypotheses the sequence $\theta C_1,\dots,\theta C_i$ is a valid proof.

Edit: I have noticed that the OP has added the definition of proof. According to this definition the argument without induction seems correct. Do not be that surprise by that, it may happen that sometimes authors suggested proofs may be moe complex than they actually need to be, after all we are all humans.

Hope this helps.

$\endgroup$
6
  • $\begingroup$ Thank you for your response. I'm sorry, I'm still not certain. This seems somewhat different than the definition of a proof as given by the text. I have added that definition to the question. $\endgroup$
    – user695931
    Commented Apr 9, 2018 at 1:15
  • $\begingroup$ @user695931useI have add a little comment in the answer :-) $\endgroup$ Commented Apr 9, 2018 at 9:55
  • $\begingroup$ @user695931user keep me posted, now I'm interested in what he/she has to say. $\endgroup$ Commented Apr 13, 2018 at 9:12
  • $\begingroup$ I emailed the author to be certain and it turns out that he believes that any rigorous proof of this metatheorem will involve some form of induction. $\endgroup$
    – user695931
    Commented Apr 21, 2018 at 20:49
  • $\begingroup$ @user695931 Did he provide any argument? $\endgroup$ Commented Apr 21, 2018 at 21:57

You must log in to answer this question.

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