Does it follow that □ ~ ( A → B)?

Question

Is this argument valid: 1. □ (B ↔ □ B) 2. ◊ ~ (A → B) 3. Therefore, □ ~ ( A → B).

I would appreciate any explanation as to whether or not it is valid. I think it is valid because if B is possibly false due to 2, and given 1, 2 should be necessarily false but I am not sure.

I know that if something T is a necessary truth, any conditional A → T will be necessarily true. Given ~ T is a necessary falsehood, it would seem A → T would be necessarily false given A holds in all possible worlds.

Here's my attempt so far but I don't know if this works: from 1, we can derive B → □B, so ◊B → ◊□B, by S5, ◊□B → □B, so ◊B → □B. Using contraposition, ~□B → ~◊B ≡ ◊~B → □~B. So, we have ◊~B → □~B. Since A is a necessary truth, substitute B by (A → B) in 2 to get 3.

Answer 1

This argument is trivially valid in GL Provability Logic since it has an inconsistent set of premises in that system. GL has a transitive and conversely well-founded frame relation, which entails that there cannot be an infinite ascending chain of worlds $x_i$ such that $x_1Rx_2Rx_3R….$ GL is achieved by adding Löb’s Theorem $\Box (\Box P \to P) \to \Box P$ as an axiom schema to system K.

Proof:

1. Suppose that at a state $\mathit v$ we have $\mathit v \vDash \Box (B \leftrightarrow \Box B)$ and $\mathit v \vDash \Diamond \sim (A \to B)$.
2. By Necessitation, K, and propositional logic, $v \vDash \Box (\Box B \to B)$, which yields $v \vDash \Box B$ by Löb’s Theorem.
3. Since $v \vDash \Diamond \sim (A \to B)$, by propositional logic, Necessitation, K, and the definition of $\Diamond$, $v \vDash \Diamond \sim B$.
4. By the definition of $\Diamond$, we have $v \vDash \sim \Box B$, which is a contradiction.
5. So, by the principle of explosion, $v \vDash \Box \sim (A \to B)$.

Answer 2

This argument is not locally valid in $S5$ and so not even locally valid in $K$. By local validity is meant truth preservation in all worlds from all models.

Here is an $S5$ counter model. Let $M = (W, R, V)$ with $ W =\{w,v,u\}, R = \{(w,w), (v,v), (u,u), (w,v), (v,u), (w,u), (v,w), (u,v), (u.w)\}, V(p) =\{v\}, V(q)= \varnothing.$

Since $M, x \not \models q$, for all $x \in W$ we have $M, w \models \Box(q \leftrightarrow \Box q )$. Because $M, v \models p$ it follows that $M, w \models \Diamond \neg (p \rightarrow q)$. But as $M, u \not \models p$ it holds that $M, u \models (p \rightarrow q)$ and so $M, w \not \models \Box \neg(p \rightarrow q).$