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.

  • $\begingroup$ 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. $\endgroup$
    – user509184
    Aug 25, 2023 at 2:41
  • $\begingroup$ @user509184 That's not a normal modal logic. $\endgroup$ Aug 25, 2023 at 5:49
  • $\begingroup$ 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$ $\endgroup$ Aug 25, 2023 at 19:16
  • $\begingroup$ 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$ $\endgroup$ Aug 25, 2023 at 19:19
  • $\begingroup$ (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. $\endgroup$ Aug 25, 2023 at 19:22

1 Answer 1


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

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.