An extension of the disjunction property in modal logic

A normal modal propositional logic $$\Delta$$ has the disjunction property if and only if

For any formulas $$A_1,\dotsc,A_n$$, if $$\Box A_1 \vee \dotsb\vee \Box A_n \in \Delta$$ then $$A_k\in \Delta$$ for some $$k$$ with $$1\leq k\leq n$$.

Let us say that $$\Delta$$ has the extended disjunction property if and only if

For any formulas $$A_1,\dotsc,A_n$$ and non-modal formula $$A_0$$, if $$A_0 \vee \Box A_1 \vee \dotsb \vee \Box A_n \in \Delta$$ then $$A_k\in \Delta$$ for some $$k$$ with $$0\leq k\leq n$$.

Does there exist a normal modal propositional logic with the disjunction property but not the extended disjunction property?

I came across the second property in some unpublished notes of Kit Fine's from the '70s, but I do not know of much discussion of it elsewhere.

• Perhaps I misunderstand your question, but doesn't it work to consider the modal propositional theory with four propositions, $P$, $\neg P$, $\top$, and $\perp$, with $\Box P = P$ and $\Box \neg P = \perp$? Looks to me like this satisfies the disjunction property, but not the extended disjunction property, since $\neg P \vee \Box P = \top$ and yet $P \neq \top$. Sorry if I've misunderstood your question and this isn't useful. Aug 25, 2023 at 2:41
• @user509184 That's not a normal modal logic. Aug 25, 2023 at 5:49
• Sometimes one finds oddities of typesetting software by looking at things here. Looking at $A_0 \vee \Box A_1 \vee ... \vee \Box A_n,$ coded as 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$ Aug 25, 2023 at 19:16
• MathJax usually treats ... 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$ Aug 25, 2023 at 19:19
• (In the comment from user509184 above, one sees $\Box \neg P = \perp,$ coded as \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. Aug 25, 2023 at 19:22

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)$$.

• I had a déjà vu feeling when writing down the argument. I think I used it before somewhere on this site. Aug 25, 2023 at 7:13
• Oh, of course: here. Aug 25, 2023 at 7:19
• Re, "déjà écrit"? 😄 Aug 25, 2023 at 23:07
• Thanks! I asked that previous question, but I didn't notice the connection to your answer. My bad! Aug 26, 2023 at 22:06
• There isn’t really much of a connection that I can see. It’s just that a similar trick works for both. Aug 27, 2023 at 6:47