# 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