Modal logic K4: strong box quantifier

[nomadreid]

In an exposition about the modal logic system K4, after introducing the box "necessity" quantifier \Box (where \BoxP is essentially that the Gödel number of P is provable), then introduces the "strong box" quantifier (I don't know how to put an s inside a box in LaTex) as:
A = A \wedge \BoxA.
But since K4 is sound, shouldn't \BoxA imply A? In that case, I do not see the difference between box and strong box.
Thanks in advance for clearing this up. (The exposition that I am following is in Smorynski's "Self-Reference and Modal Logic")

 

[yossell]

It's been ages since I've looked at this stuff - as I recall, K is very weak and 4 is the principle Box A - > Box Box A. So I don't see why you think Box A should imply A.

Of course, for most natural readings of Box, it's a form of necessity, and so the principle should be true. But in this context, Box A is an abbreviation for the formula P is provable. This won't Give you that Box A implies A, or that Box A - > A is a theorem.

Indeed, if I remember right, possible world models for provability logics, the accessibility relation is not reflexive - so Box A can be true at a world while P is false at that world.

But this all a bit hazy in my brain.

 

[nomadreid]

Yossell, thanks for the reply. Yes, K4 is the system (which Smorynski calls "Basic Modal Logic"), "K" plus the new axiom you mentioned (which he labels "A3") \BoxA\rightarrow\Box\BoxA.

I did not understand your comment

Box A is an abbreviation for the formula P is provable

Shouldn't that be
"Box A is an abbreviation for the formula A is provable"? Where does P come from? The same comment goes for

so Box A can be true at a world while P is false at that world.

Do you mean
"so Box A can be true at a world while A is false at that world"?
I see that you are correct in saying that the axioms of K4 do not allow
\BoxA\rightarrowA
So -- and this is what puzzles me--if we interpret \BoxA as Pr("A") (the quotes being Gödel#), then we do not have soundness.
Is this correct? Can we then say that K4 is not sound?
Thanks for digging up this material out of the recesses of your past and helping me make it part of my present.

 

[yossell]

Sorry nomadreid- I flipped between A and P a couple of times... Uhhh, I blame autocorrect. :-) It should be A throughout.

I'm not sure exactly what your worry is concerning soundness. If we're assessing K4 as a system of modal logic, then whether it is sound or not depends on the models relative to which we are defining soundness or completeness. Normally, these are possible worlds models, with a particular choice of accessibility relation.

Alternatively, the system you might have in mind is just plain old first order arithmetic, with Pr("A") just another sentence of the language. But then there is nothing new here and we just have the standard soundness and completeness results of first order logic.

Or it might be that you take the sentences Pr("A")-> A to be expressing soundness. In this sense, soundness fails here.

Now, I agree that last can seem quite shocking. Why not move to a system where Pr("A") - >A is always provable? Unfortunately, such systems are too strong - for whenever this is provable, A itself is also provable. See http://en.wikipedia.org/wiki/Löb's_theorem

However, rather than seeing this as a failure of soundness, you can question the degree to which PA (peano arithmetic) can fully encode the concept of provability. For something is provable iff there is a *finite* number of steps, each of which is either an axiom or follows from earlier steps by a rule of inference. While PA is good at encoding and defining axiomhood and following, it is not good at expressing the concept of finitude. Indeed, it cannot express it.

Another way to see things is to remember that PA (peano arithmetic) cannot prove its own consistency (godless second incompleteness theorem) . Accordingly, the statement Pr("P and ¬P")is consistent with PA. So one can add the statement to PA and the result is a consistent theory. So Pr("P and ¬P") had better not imply "P and ¬P".

Anyway, that's my take on things. Bound to be more mistakes here - apologies in advance

 

[nomadreid]

Yossell, many thanks for that analysis, which helped clear things up a lot. (I also liked your pun on "Gödel's"). In particular, I had not thought about Löb's theorem, and your example of adding a contradiction to PA was a very instructive one. So, I now have more food for thought. Thanks again.
Also, I think that I was being sloppy: as you say, I took \BoxA\rightarrowA to be a definition of soundness, and I guess I should have taken |-\BoxA\rightarrow|-A. ("|-" is turnstile.)

 

[nomadreid]

Postscript: I meant, obviously, adding the provability of a contradiction, not adding the contradiction itself.