When proving the Hypothetical Syllogism inference rule, why must you assume that p is true?

Question

I recently started learning Discrete Maths and currently studying rules of inference. I was looking at a proof of Hypothetical Syllogism, aka:

P→Q
Q→R

∴ P→R

and I came across this proof of the above rule:

(1) P→Q (Hypothesis)
(2) Q→R (Hypothesis)
(3) P (Assumption)
(4) Q (1 and 3: Modus Ponens)
(5) R (2 and 4: Modus Ponens)
(6) P→R (3 - 5: if P, then R)
∴ ((P→Q) ∧ (Q→R)) → (P→R)

I understand all the steps, except for step (3). Why do we need to assume that P is true? In that case, isn't it just a conditional proof and no longer a tautology? If P is false, would't the proof no longer hold?

Answer 1

$(3), (4), (5)$ can be seen as a subproof, within the larger proof.

We assume $P$, in order to see what follows from $P$.

In this case, after two applications of modus ponens, we see that $R$ follows from that assumption, together with the hypotheses.

So we have proven if P, then R. (Which we state in line $(6)$. In symbols, we have proven $P \rightarrow R$. We haven't proven P. But we have proven P implies R. If P is false, the implication is true (any implication with a false antecedent is true). However, we know that if P is true, then so must be R.

Answer 2

The rule says (something like) "to conclude $P\rightarrow R$, it suffices to conclude $R$ having assumed $P$". The point is that if $P$ happens to be true then $R$ must be true as well. If $P$ is false, it doesn't matter because $P\rightarrow R$ is automatically true in that case.

Answer 3

In any axiomatic system where this rule is valid you do not have to assume "p" in order to prove this rule, since in any axiomatic system where you can use conditional introduction a rule of inference, CpCqp and CCpCqrCCpqCpr are either axioms or theorems. Suppose the axioms are the following, in Polish/Lukasiewicz notation:

1. CpCqp.
2. CCpCqrCCpqCpr.

Then we can prove the rule as follows:

hypothesis  1 Cpq
hypothesis  2 Cqr
axiom 1     3 CCqrCpCqr
3, 2        4 CpCqr
axiom 2     5 CCpCqrCCpqCpr
detach 5, 4 6 CCpqCpr
detach 6, 1 7 Cpr