Epistemic puzzles and the general necessitation-iteration rule RK

Question

So I came across epistemic puzzles, or specifically the "Surprise Exam"/"Prediction Paradox" and found some explanation in Wesley H. Holliday's paper "Simplifying the Surprise Exam", however there is a normal modal logic K used together with the rule:

$$RK_{i}\quad\frac{(\varphi_{1}\wedge\cdots\wedge\varphi_m)\rightarrow \psi}{(\Box_{i}\varphi_{1}\wedge\cdots\wedge\Box_{i}\varphi_m)\rightarrow \Box_{i}\psi}$$

How is this rule semantically and syntactically sound for the logic K?

If $m=0$ the rule is basically standard necessitation but what about the other cases?

Answer 1

This rule is valid because $\vDash_K \Box (\varphi \land \psi) \leftrightarrow (\Box \varphi \land \Box \psi)$. This rule could be used in a sequent-style system for K.

For an intuition about why it is valid semantically, think in terms of the definition of $\Box$. Suppose that each $\varphi_m$ is true in every accessible world. If there is an accessible world where some $\varphi_m$ does not hold, then since that $\varphi_m$ is true at all accessible worlds, we get a contradiction. So, if each $\varphi_m$ holds at every accessible world, then at all accessible worlds each $\varphi_m$ holds. Thus, since $\Box (\varphi_1 \land … \land \varphi_m) \to \Box \psi$, $(\Box \varphi_1 \land … \land \Box \varphi_m) \to \Box \psi$ follows.

Answer 2

We can directly show that RK is a derived inference rule of the modal logical system K. I shall sketch out a derivation of it.

Recall that propositional calculus is a constituent of the system K. Hence, we can use the theorems of propositional calculus. In particular, we shall use

$$((A\wedge B)\rightarrow C)\leftrightarrow (A\rightarrow (B\rightarrow C))$$

citing it as THM.

Also, we shall make use of the meta-theorem transitivity of implication (TI)

$$A\rightarrow B, B\rightarrow C\vdash A\rightarrow C$$

and the distribution axiom (DIST) of K

$$\Box(A\rightarrow B)\rightarrow(\Box A\rightarrow\Box B)$$

For generalisation, we shall appeal to mathematical induction in metalanguage, which is a primary method of such proofs. So, we begin with

Basis clause. For $k=0=m$ $$\psi\vdash\Box\psi$$ holds by the rule of necessitation (NEC).

Inductive clause. Assume for $k=n$

$$(\varphi_{1}\wedge\cdots\wedge\varphi_{n})\rightarrow\xi\vdash (\Box\varphi_{1}\wedge\cdots\wedge\Box\varphi_{n})\rightarrow\Box\xi$$ holds (I have used a distinct variable $\xi$ to indicate the following step clearer).

For $k=n+1$, we write by THM (left-to-right)

$(\varphi_{1}\wedge\cdots\wedge\varphi_n\wedge\varphi_{n+1})\rightarrow \psi\vdash (\varphi_{1}\wedge\cdots\wedge\varphi_{n})\rightarrow(\varphi_{n+1}\rightarrow\psi)\qquad(\ast)$

We rewrite the inductive hypothesis as

$(\varphi_{1}\wedge\cdots\wedge\varphi_n)\rightarrow \underbrace{(\varphi_{n+1}\rightarrow\psi)}_{\xi}\vdash(\Box\varphi_{1}\wedge\cdots\wedge\Box\varphi_{n})\rightarrow\Box\underbrace{(\varphi_{n+1}\rightarrow\psi)}_{\xi}$

By DIST,

$(\Box\varphi_{1}\wedge\cdots\wedge\Box\varphi_{n})\rightarrow\Box(\varphi_{n+1}\rightarrow\psi)\vdash(\Box\varphi_{1}\wedge\cdots\wedge\Box\varphi_{n})\rightarrow(\Box\varphi_{n+1}\rightarrow\Box\psi)$

By THM (right-to-left), we write

$(\Box\varphi_{1}\wedge\cdots\wedge\Box\varphi_{n})\rightarrow(\Box\varphi_{n+1}\rightarrow\Box\psi)\vdash(\Box\varphi_{1}\wedge\cdots\wedge\Box\varphi_{n}\wedge\Box\varphi_{n+1})\rightarrow\Box\psi\qquad(\ast\ast)$

By transitivity of implication (TI), we get from $(\ast)$ and $(\ast\ast)$

$(\varphi_{1}\wedge\cdots\wedge\varphi_n\wedge\varphi_{n+1})\rightarrow \psi\vdash(\Box\varphi_{1}\wedge\cdots\wedge\Box\varphi_{n}\wedge\Box\varphi_{n+1})\rightarrow\Box\psi\quad\blacksquare$

Notice that Holliday sets out a polymodal argument; that is, each $\Box_{i}$ is a distinct modal (necessity) operator. Therefore, we have RK$_{i}$

$(\varphi_{1}\wedge\cdots\wedge\varphi_n)\rightarrow \psi\vdash(\Box_{i}\varphi_{1}\wedge\cdots\wedge\Box_{i}\varphi_{n})\rightarrow\Box\psi$

for each $i$.