Re: strange non theorem in S4

In article
<9322fcc2-c3e3-425a-961c-22ed80ed26d1@xxxxxxxxxxxxxxxxxxxxxxxxxxx>,
translogi <wilemien@xxxxxxxxxxxxxx> wrote:

....
Do you have any comments on my other post?
How to prove S5 |-A <==> S4|- <>[]A

(Or S5 |-a <==> S4|- MLa )


From right to left it's easy:

S4 |- MLa => S5 |- MLa => S5 |- La => S5 |- a.

I think the left-to-right proof can be done by an induction
argument. Here's an outline, leaving you to fill in the detailed proofs.

First, S4 |- a => S4 |- La => S4 |- MLa

so in particular the result applies to all S4 axioms. Just one more
axiom is needed for S5. You may be able to prove

S4 |- ML(MLp -> Lp)

so the result applies to all S5 axioms.

Now consider rules of inference. Uniform substitution appears to raise
no problems. As for modus ponens, you may be able to see how to prove
that

S4 |- MLa and S4 |- ML(a -> b) together imply S4 |- MLb.

Necessitation is easier:

S4 |- MLa => S4 |- MLLa.

So given any proof in S5, adding ML at the beginning of every
formula should produce a valid proof in S4. Hence indeed

S5 |- a => S4 |- MLa.

(Can anyone see a flaw in all that? :-)


....
Read about S2, seems to be T with a bit different neccesitation rule.
Don't understand the reason why not to use the normal nessecitation is
invalid or even how you decide if you can use the necessitation rule
or not....


Hughes & Cresswell, "A New Introduction to Modal Logic" has a
little bit about non-normal systems such as S2, but their earlier book
"An Introduction to Modal Logic" gives beautifully detailed explanations.

Ken Pledger.
.

Relevant Pages

  • Re: strange non theorem in S4
    ... so in particular the result applies to all S4 axioms. ... Uniform substitution appears to raise ... As for modus ponens, you may be able to see how to prove ... invalid or even how you decide if you can use the necessitation rule ...
    (sci.logic)
  • Re: Modal logic from T B and 4 to S5
    ... translogi wrote: ... can be done to add to K the axioms T B and 4 ... and then use the dual of 4: MMp -> Mp. ... Ken Pledger. ...
    (sci.logic)