2 replaced all greek letters with regular characters

# 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

# Prove the rule that proves 𝜒(𝜙) from 𝜒(𝛼) 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 π(π) from π(πΌ) preserves derivability (i.e. if β’π(πΌ) then β’π(π) in modal system K, where πΌ is a sentence letter which occurs zero or more times in an MPL-wff π(πΌ), and π(π) is the result of replacing every instance of πΌ with the wff π.

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: πβ(πβπ)

PL2: (πβ(πβπ))β((πβπ)β(πβπ))

PL3: (~πβ~π)β((~πβπ)βπ)

K: β»(πβπ)β(β»πββ»π)

and the rules modus ponens and necessitation.

I really can't see how I can go from π(πΌ) to π(π) using these, so I'd appreciate any help you could offer.

# 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

1

# Prove the rule that proves 𝜒(𝜙) from 𝜒(𝛼) 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 π(π) from π(πΌ) preserves derivability (i.e. if β’π(πΌ) then β’π(π) in modal system K, where πΌ is a sentence letter which occurs zero or more times in an MPL-wff π(πΌ), and π(π) is the result of replacing every instance of πΌ with the wff π.

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: πβ(πβπ)

PL2: (πβ(πβπ))β((πβπ)β(πβπ))

PL3: (~πβ~π)β((~πβπ)βπ)

K: β»(πβπ)β(β»πββ»π)

and the rules modus ponens and necessitation.

I really can't see how I can go from π(πΌ) to π(π) using these, so I'd appreciate any help you could offer.