2 replaced all greek letters with regular characters
source | link

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
source | link

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.