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.