# How to prove □Q from P→Q and □P?

Given P→Q, and □P, in what systems can we conclude □Q?

I want to know in which system the consequent is derivable from the premises and in which it is axiomatic (or perhaps we can include it as an axiom). Both parts of the question are contingent on the possibility of it existing in the first place.

Feel free to answer part of the question if you can not answer the whole thing.

Regards.

• Is P->Q a theorem, or just valued true in the current world? May 16 '19 at 2:41
• @GrahamKemp tbh, I am not sure. Let us take it as a true in current world. May 16 '19 at 2:42
• Near as I can tell, that would require a reflexive frame with only one world. May 16 '19 at 3:48
• If p→q is just a material implication in the actual world it has no bearing on what happens in other worlds, so it gives you no information to combine with Np, unless there is a single world, as Graham suggested. On the other hand, if you have N(p→q) then the distribution axiom N(p→q)→(Np→Nq) (valid even in the weakest of standard modal logics, K) combined with Np will give you Nq. May 16 '19 at 6:25
• @GrahamKemp I don't think you need to restrict the model to contain only one world, but to every world only seeing one world, namely itself. May 16 '19 at 13:30

I am aware of no standard modal logic which allows for such a derivation.

What you do have in system K is □(p → q), □p ⊨ □q:

In system K, we have the Axiom scheme K/Distribution axiom

□(A → B) → (□A → □B)

If we had □(p → q), then using distributivity we could obtain (□p → □q), which, combined with the premise □p, immediately gives us □q by modus ponens.

The problem is that we can't immediately deduce □(p → q) from (p → q) alone. For this step to be valid, we would need a particular setting: If we want to claim that from the fact that a formula is valid in some world, we can deduce that it is necessarily true, this amounts to stating that the only possible scenario any world can reach, if anything, is itself (we must exclude the possibility that the world can "imagine" other worlds at which the formula might not be true, which would invalidate the necessity), so every world just has nothing but themselves in mind, if at all: You can easily verify that in such a setting, if A is true at any given world , then so is □A: The only world that w can access is w itself, so A is true at all w-accessible worlds, hence □A. If w can not even see itself, then □A becomes vacuously true, as there are no w-accessible worlds for which A does not hold, which is consistent with A → □A. So a frame setting where each world can access at most itself gives us the desired property A → □A. Conversely, we could prove by contraposition that if A → □A is a theorem, then we obtain a frame were no world must see any other than itself. This gives us the usual duality between the formulation of logical axioms and properties of the permissible frames.

Note that we don't need the reverse direction of the implication to be true: To deduce our desired formula, we don't need □A → A. This axiom, which defines system T (together with the axiom K), is equivalent to reflexivity:

□A → A

∀w(R(w,w))

where R is the accessibility relation. In a reflexive frame, the world w itself is always among the set of worlds that are accessible from w, so if A is necessary (true at all worlds which w can reach), then A is also true at w itself. And conversely, if for any world from A follows □A, then we must demand that every world can see itself. Hence, the axiom and the frame property are equivalent.

But we don't need this in our frame: It might just be that □A is true without A being true, so it is permissible that a world can not even reach itself.¹

So the only thing we need to make sure is that every world can see at most itself, i.e. no worlds other than itself. Let's call this the axiom of necessitation², or the frame property of isolation:

A → □A

∀ww'(R(w,w') → w=w') (or equivalently, ∀w¬∃w'(R(w,w')∧w≠w')))

You can easily verify that the axiom A → □A and the isolation property are equivalent.

If we assume this, we can make the desired deduction (here presented in a Hilbert-style manner):

1. p → q (premise)
2. (p → q) → □(p → q) (new axiom of necessitation, instantiated to A = p → q)
3. □(p → q) (modus ponens on 1,2)
4. □(p → q) → (□p → □q) (axiom K, instantiated to A = p, B = q)
5. □ p → □ q (modus ponens on 3,4)
6. □ p (premise)
7. □ q (modus ponens on 5,6)

As said, I am not aware of any standard modal logic that includes such an axiom.

¹ If we were to combine isolation with reflexivity, the result would be a frame where the set of possible worlds accessible from any given world is exactly that world itself, so every world has itself and only itself in mind - let's call this this the property of egocentrism:

∀w,w'(R(w,w') ↔ w=w')

In such a setting, we would obtain a bi-implication between any formula and its necessitation:

A ↔ □A

It is easily verifiable that we would even obtain equivalence with ◇:

A ↔ □A ↔ ◇A

Egocentrism makes the idea of the modal operators a somewhat trivial one: If the only possible world you can imagine is your own one, then there is not point in setting up a model of interconnected possible worlds in the first place, and possiblity and necessity reduces to truth in your own world.

² This is not to be confused with the necessitation rule A ⊢ □A which holds in deduction sytems like Hilbert calculus for system K: Applying this rule requires that the formula A be derived by rules, not a free assumption (as (p → q) in our case). A → □A is not an axiom (and neither a derivable rule) in system K.

• Thank you for the in-depth answer. I am aware of K-distribution; however, I was looking for a standard system such that in it either a) the conditional derivation is an axiom or b) nec(Q) is derivable via valid inferences given the aforementioned premises. Thanks a ton for the explanation, but it seems like the framework will be quite useless if we employ the restrictions required for deriving nec(Q) given the the premises on hand. Regards May 17 '19 at 11:45