# Prove the rule that proves X(P) from X(a) preserves derivability in modal system K

I'm trying to solve a problem which asks me to show that the meta-rule defined by deriving X(P) from X(a) preserves derivability (i.e. if ⊢X(a) then ⊢X(P) in modal system K, where a is a sentence letter which occurs zero or more times in an MPL-wff X(a), and X(P) is the result of replacing every instance of a with the wff P.

This would be relatively easy to do semantically and then use completeness of K to give the desired result, but the problem asks me to do this without making use of completeness.

In system K, I have the axioms

PL1: P→(Q→P)

PL2: (P→(Q→R))→((P→Q)→(P→R))

PL3: (~Q→~P)→((~Q→P)→P)

K: ◻(P→Q)→(◻P→◻Q)

and the rules modus ponens and necessitation.

I really can't see how I can go from X(a) to X(P) using these, so I'd appreciate any help you could offer.

EDIT: Have replaced all greek letters with regular characters: note P, Q, R here represent arbitrary wffs and not just sentence letters

• Most of symbols look like crossed boxes to me. – rus9384 Feb 3 '19 at 22:09
• @rus9384 I've replaced all the greek letters with regular characters - is that any better? – digifu Feb 3 '19 at 22:17

## 1 Answer

The correct answer is: that is obvious. Now we only have to understand, why it is obvious. I hope you know this mathematical joke, p.32 left column on the bottom.

Consider it like this: a proof is a sequence of sentences, in which every line is an axiom, or follows by modus ponens from two previous lines. Since you derive X(a), this sequence ends with X(a). Now replace in each line a by P. Is it still a valid proof, i.e. is still every line an axiom or obtained by modus ponens?

One would make this (overly) precise by using induction on the length of the proof. Start with proofs of length 1 (or 0 if you are lazy and don't want to prove an induction start). This single line must be X(a) and it has to be an axiom. But if X(a) is an axiom, then so is X(P), since there are only axiom schemata (I know people who would require you to prove that X(P) is an axiom too. Don't do that, unless you don't find it obvious). For the induction step you can argue similarly if X(a) is an axiom. If the last line is obtained by modus ponens, then there are two previous lines of form Y(a)→X(a), Y(a). Since replacing a by P in all except the last line results by induction hypothesis in a valid proof up to the second to last line, these were replaced by Y(P)→X(P) and Y(P) resp. So replacing the last line by X(P) does no damage.