Does S4 (and B) hold for the strongest interpretations of ♢ and □?

Question

Suppose these are the interpretations we are working with:

♢Ψ iff no explicit contradiction can be deduced from Ψ in FOL or in other words it's not provable that ~Ψ in FOL.

~♢Ψ iff an explicit contradiction can be deduced from Ψ in FOL or in other words it's provable that ~Ψ in FOL.

□Ψ iff ~♢~Ψ.

~□ iff ♢~Ψ.

It's clear that M holds for these interpretations, i.e. □Ψ / ∴ Ψ, because □Ψ based on the interpretation we've given above to □ is equivalent to ~♢~Ψ, which, in turn, based on the interpretation we've given above to ~♢ is equivalent to "an explicit contradiction can be deduced from ~Ψ in FOL or in other words it's provable that Ψ in FOL." Hence □Ψ under present interpretations is equivalent to "an explicit contradiction can be deduced from ~Ψ in FOL or in other words it's provable that Ψ in FOL." And plainly enough from this it follows that Ψ.

But I was wondering does S4 hold for these interpretations, i.e. □Ψ / ∴ □□Ψ. Once again (from above), □Ψ under present interpretations is equivalent to "an explicit contradiction can be deduced from ~Ψ in FOL or in other words it's provable that Ψ in FOL." Does it follow from this that □□Ψ, which, under present interpretations, is equivalent to "an explicit contradiction can be deduced from 'no explicit contradiction can be deduced from ~Ψ' in FOL or in other words it's provable that it's provable that Ψ in FOL."

(And I suppose for these interpretations I'm also wondering whether B holds or not, i.e. Ψ / ∴ □♢Ψ.)

Thank you.

Answer 1

This is a very natural idea, and this topic (provability logic) is well studied. Unfortunately, I am no specialist in this, but I can give you some hints.

First you have to note that you have to have a notion of provability in your object language, otherwise you cannot make sense of □□A. A (non-natural but historically significant) theory that allows that is PA, or any of its reasonable extensions T.

So intuitively one defines □A as Pr('A'), where 'A' is the Gödel Code of (the PA or T sentence represented by) A, and Pr the provability predicate from PA. Since A itself might contain modal operators, one has to be more a bit more careful. Solovay's paper "Provability Interpretations of Modal Logic", IJM 1976, gives you the details. One can then prove Solovay's theorem, which states roughly ("roughly", since I haven't defined 'A' properly, and also haven't talked about the restrictions on T):

T˫ 'A' iff ˫A in the modal logic L

The logic L is K with the additional axiom L (Löb's axiom): □(□A→A)→□A. Axiom 4 does hold in it (easy exercise), but the reflexivity axiom □A→A does not (you can find an L-model where accessibility is not reflexive).

I suppose the moral of the story is, that you want S4 to be the logic, but getting that seems difficult.

Maybe the SEP article Provability Logic is a good entry point for further study. There is also the chapter on Provability Logic in the handbook of proof theory (PDF from the author) by Japaridze and de Jongh.

Answer 2

System (M) has this axiom : ◻Ψ → Ψ, and System S4 is M in addition to this axiom : ◻Ψ → ◻◻Ψ.

◻Ψ : means, according to your interpretation, an explicit contradiction can be deduced from ~Ψ.

Let Φ = ◻Ψ

So, Φ stands for an explicit contradiction can be deduced from ~Ψ.

Now, let us add another box : ◻Φ

◻Φ : means, an explicit contradiction can be deduced from ~Φ

So, one can think of it as if it means : We can deduce a contradiction from a proposition Φ where ~Ψ does not give rise to any contradiction. Which means that it is necessary that a contradiction follows from ~Ψ, and it would be contradictory if this is not the case.

It is necessary that there is a contradiction that follows from ~Ψ

As for B, the main axiom is : Ψ → ◻◇Ψ

Using your interpretation, it means : "in system B, Ψ implies that, an explicit contradiction can be deduced from "it is not possible that Ψ"

So, it means that Ψ has to be possible.

We can go further and switch the squiggle (not possible = necessarily not) and say :

"in Modal System B, Ψ implies that, an explicit contradiction can be deduced from the proposition : It is necessary that not Ψ"

So, we can understand it as if the claim that "It is necessary that not Ψ" is contradictory and therefore impossible, which means that it is necessary that Ψ be possible.

So yes, you can use the interpretation you provided with system B