The extended disjunction property is equivalent to plain disjunction property for all normal modal logics $\Delta$.

Assume that $\Delta$ contains
$$A_0\lor\bigvee_{i=1}^n\Box A_i,$$
where $A_0$ is box-free.

Let $P$ denote the set of propositional variables occurring in the formula. For each $a\colon P\to\{0,1\}$, let $\sigma_a$ denote the substitution such that $\sigma_a(p)=p^{a(p)}$ for all $p\in P$, where $p^1=p$, $p^0=\neg p$.

Since $\Delta$ is closed under substitution and classical reasoning, $\Delta$ contains
$$\bigwedge_a\Bigl(\sigma_a(A_0)\lor\bigvee_{i=1}^n\Box\sigma_a(A_i)\Bigr).\tag{$*$}\label{star}$$

If $A_0$ is a classical tautology, then $A_0\in\Delta$ and we are done. Otherwise, \eqref{star} implies
$$\bigvee_a\bigvee_{i=1}^n\Box\sigma_a(A_i)\tag{$**$}\label{starstar}$$
by classical propositional reasoning: for any assignment $e$, there is $a$ such that $e(\sigma_a(A_0))=0$, thus the rest of the disjuction holds under $\sigma_a$.

Applying the disjuction property to \eqref{starstar}, $\sigma_a(A_i)\in\Delta$ for some $i=1,\dotsc,n$ and $a\colon P\to\{0,1\}$. Applying closure under substitution once more, $\Delta$ contains $\sigma_a(\sigma_a(A_i))$, which is equivalent to $A_i$ over **K**.

The argument above applies not just to normal modal logics, but also to quasinormal logics, and even more generally, to all logics $\Delta$ that are closed under modus ponens and box-free substitutions, and that contain the tautologies of **E**. Here, **E** is the smallest logic that includes classical logic, and is closed under modus ponens and under the rule $A\leftrightarrow B\mathrel/\Box(A\leftrightarrow B)$.

`A_0 \vee \Box A_1 \vee ... \vee \Box A_n`

, one instantly sees that the last $\vee$ does not have the conventional amount of horizontal space to its right. I had a guess about the reason for that, and I'm not yet sure my guess was wrong, but when I changed the code to`A_0 \vee \Box A_1 \vee \cdots \vee \Box A_n`

, that fixed the issue, so that what appeared was $A_0 \vee \Box A_1 \vee \cdots \vee \Box A_n.$ MathJax usually$\,\ldots\qquad$ $\endgroup$`...`

as if it were`\dots`

, unlike LaTeX which renders`...`

differently from`\dots`

. I suspect there's some obvious reason for this difference in horizontal spacing after`\vee`

, but I don't know what it is. $\qquad$ $\endgroup$`\Box \neg P = \perp`

, whereas the code`\Box \neg P = \bot`

yields instead $\Box \neg P = \bot,$ which is the correct amount of horizontal space after the "equals" sign. In a case like that, the reason is clear and it's what I expect. I'm guessing I'll figure the other one out. $\endgroup$6more comments