Proof of $\triangledown(\top,\top)$ in modal logic

Question

My textbook has this definition in it (actually, the textbook gives a definition for a modal language with arbitrary modal operators, but i believe the simple language with a single binary operator is enough to demonstrate what i want); a set of formulas $\Lambda$ is a normal modal logic iff all of the following is true:

1. All propositional tautologies belong to $\Lambda$,
2. If $\phi \in \Lambda$ and $\phi\rightarrow\psi \in \Lambda$, then $\psi \in \Lambda$,
3. If $\sigma$ is a map from propositional letters to formulas, and $\phi \in \Lambda$, then $\phi^\sigma \in \Lambda$, where $\phi^\sigma$ is $\phi$ with its propositional letters substituted as per defined by $\sigma$ (in other words, $\Lambda$ is closed for the uniform substituion operation),
4. $\triangledown(p,r)\rightarrow(\triangledown(p\rightarrow q,r)\rightarrow \triangledown(q,r))\in \Lambda$ and $\triangledown(r,p)\rightarrow(\triangledown(r,p\rightarrow q)\rightarrow \triangledown(r,q))\in \Lambda$ (these are the analogs of the K axiom for the binary modal operator),
5. $\triangle(p,q)\leftrightarrow\neg\triangledown(\neg p,\neg q) \in \Lambda$ (this is the analog of the Dual axiom),
6. If $\phi \in \Lambda$ then $\triangledown(\phi,\bot) \in \Lambda$ and $\triangledown(\bot,\phi) \in \Lambda$ (the analogs for the generalization rule),

(where $p,q$ and $r$ are distinct propositional letters)

The modal language in question is what you'd expect; given a set of propositional letters, modal formulas are either a propositional letter, or $\bot$, or $\phi \lor \psi$, or $\neg\phi$, or $\triangle(\phi,\psi)$, where $\phi$ and $\psi$ are modal formulas. Other symbols are the usual definitions ($\phi\rightarrow\psi$ is $\neg\phi\lor\psi$, $\triangledown(\phi,\psi)$ is $\neg\triangle(\neg\phi, \neg\psi)$, $\top$ is $\neg\bot$ and so on).

Now, as an easy semantic argument shows, $\triangledown(\top,\top)$ is valid (or, more precisely, it is valid on the class of all Kripke frames). We would expect it to be the case that $\triangledown(\top,\top)\in\Lambda$, for all normal modal logics $\Lambda$.

Is that actually the case?

(I actually suspect it isn't! It feels that, since you can't use the K-like axioms to change both variables at once, and the generalization-like rules always add $\bot$, you're kinda stuck with $\bot$ on one side of the $\triangledown$ formulas.)

Answer 1

No, it isn't.

The basic idea of the proof is this: We can define an alternative interpretation for the logic such that the logic is correct with respect to said interpretation, but $\triangledown(\top, \top)$ isn't valid in the interpretation, therefore implying that $\triangledown(\top, \top)$ can't be an theorem of the logic.

We'll restrict ourselves to the minimal normal modal logic $K_2$. We need the following alternative characterization of it:

For all modal formulas $\phi$, $\psi$ and $\rho$, we have that

1. All propositional tautologies (and the result of any uniform substitution applied to them, in other words, any of their instances, including those containing modal formulas) belong to $K_2$
2. If $\phi \in K_2$ and $\phi\rightarrow\psi \in K_2$, then $\psi \in K_2$,
3. $\triangledown(\phi,\rho)\rightarrow(\triangledown(\phi\rightarrow \psi,\rho)\rightarrow \triangledown(\psi,\rho))\in K_2$ and $\triangledown(\rho,\phi)\rightarrow(\triangledown(\rho,\phi\rightarrow \psi)\rightarrow \triangledown(\rho,\psi))\in K_2$,
4. $\triangle(\phi,\psi)\leftrightarrow\neg\triangledown(\neg \phi,\neg \psi) \in K_2$,
5. If $\phi \in K_2$ then $\triangledown(\phi,\bot) \in K_2$ and $\triangledown(\bot,\phi) \in K_2$,

and no other formula belongs to $K_2$.

At this point, we should prove that $K_2$ is indeed a normal modal logic, or more precisely, we should prove that $K_2$ is closed for uniform substitution, as the rest follows trivially. Note that the notion of "belonging to $K_2$" has a natural inductive structure; do an induction on that, and the proof for closure under uniform substituition follows.

Next, let's define the alternative interpretation. First, define an A-Kripke frame to be a tuple of $(W,R_a,R_b)$, where $W$ is a set, and $R_a,R_b$ are binary relations over $W$ (that is, $R_a,R_b \subseteq W\times W$). An A-Kripke model is a tuple $(F,V)$, where $F$ is an A-Kripke frame, and $V$ is a valuation function, a function from propositional letters to sets of elements of W (that is, $V : \Phi \rightarrow P(W)$, where $\Phi$ is the set of propositional letters, and $P(W)$ is the set of all subsets of $W$).

Next, we define the A-satisfaction relation $\Vdash^A$, a relation between A-Kripke models, elements of W, and modal formulas. Let $w,v\in W$, $M=((W,R_a,R_b),V)$ be an A-Kripke model, and $\phi, \psi$ be modal formulas. We have:

$$ M,w \Vdash^A p \textrm{ iff } w \in V(p) $$ $$ M,w \Vdash^A \phi\lor\psi \textrm{ iff } M,w \Vdash^A \phi \textrm{ or } M,w \Vdash^A \psi $$ $$ M,w \Vdash^A \neg\psi \textrm{ iff } M,w \Vdash^A \psi \textrm{ isn't the case (that is, $M,w \nVdash^A \psi$) } $$ $$ M,w \Vdash^A \triangledown(\phi, \psi),\textrm{ with }\phi\neq\bot\textrm{ and }\psi\neq\bot, \textrm{ or } \phi=\psi=\bot,\textrm{ is never the case} $$ $$ M,w \Vdash^A \triangledown(\bot, \psi),\textrm{ with }\psi\neq\bot, \textrm{ iff for all worlds } v\in W \textrm{ such that } R_awv, \textrm{ we have } M,v \Vdash^A \psi $$ $$ M,w \Vdash^A \triangledown(\phi, \bot),\textrm{ with }\phi\neq\bot, \textrm{ iff for all worlds } v\in W \textrm{ such that } R_bwv, \textrm{ we have } M,v \Vdash^A \phi $$

All other formulas can be defined in terms of those mentioned above; in particular, $\top$ is defined as $\neg\bot$, and $\triangle(\phi,\psi)$ is defined by duality, as $\neg\triangledown(\neg\phi,\neg\psi)$. So this gives us the satisfability of $\triangledown(\top, \top)$ in this interpretation as impossible, since $\top\neq\bot$.

Then all that remains is establishing the main correctness result; we'll prove that, for all modal formulas $\phi$, if $\vdash_{K_2}\phi$ (that is, $\phi\in K_2$), then for all A-Kripke models $M$ and its worlds $w$, $M,w\Vdash^A \phi$, or in more usual notation, simply $\Vdash^A \phi$ (this means: $\phi$ is a valid formula). From there, we can reason counterpositively - if $\triangledown(\top, \top)$ is not valid (in fact it is not even satisfiable!), then it can't possibly belong to $K_2$, and so doesn't belong to all modal logics; which clearly means our definition of modal logic is bogus.

We must once again reason inductively on the structure of $K_2$; this time, let's not skip the proof (at least, not the basic structure!). Let $\phi\in K_2$ be a modal formula. Then our original hypothesis, $\vdash_{K_2}\phi$ gets divided into 5 cases, the 5 possibilities we listed as justification for a formula to belong to $K_2$ (and we have to prove $\Vdash^A \phi$ in all of them):

1. $\phi$ is an instance of a propositional tautology. Our satisfaction relation agrees completely with the usual definitions for the propositional conectives; it must be the case that $\phi$ is valid.
2. $\phi$ can be derived from modus ponens, that is, there exist $\psi\in K_2$ and $\psi\rightarrow\phi\in K_2$. In this case, the inductive hypothesis tells us that $\Vdash^A \psi$ and $\Vdash^A \psi\rightarrow\phi$. Again, our satifaction relation behaves as usual regarding propositional conectives, so we do have $\Vdash^A \phi$.
3. $\phi$ is one of the $K$ axioms. Then consider $\phi=\triangledown(\eta,\rho)\rightarrow(\triangledown(\eta\rightarrow \psi,\rho)\rightarrow \triangledown(\psi,\rho))$ (we'll leave the other possibility for the reader, as it is rather similar to this one). We're trying to establish $\Vdash^A \triangledown(\eta,\rho)\rightarrow(\triangledown(\eta\rightarrow \psi,\rho)\rightarrow \triangledown(\psi,\rho))$. Then consider an A-Kripke model $M=(W,R_a,R_b,V)$, and $w\in W$. Next, suppose $M,w\Vdash^A \triangledown(\eta,\rho)$ and $M,w\Vdash^A \triangledown(\eta\rightarrow \psi,\rho)$. If with those hypotheses we prove $M,w\Vdash^A \triangledown(\psi,\rho)$, then we'll have proven what we wanted. Now, do observe that $\rho$ must be $\bot$, for if it were not, then we'd have $M,w\Vdash^A \triangledown(\eta\rightarrow \psi,\rho)$ and both subformulas would be different from $\bot$, a situation defined as impossible. Also note that, since $\rho=\bot$ then $\eta\neq\bot$, for if not then we'd have an impossible situation arising from $M,w\Vdash^A \triangledown(\eta,\rho)$ and $\eta=\rho=\bot$. Then consider a $v$ such that $R_bwv$. By our hypotheses and observations, we have $M,w\Vdash^A \triangledown(\eta,\bot)$ and $M,w\Vdash^A \triangledown(\eta\rightarrow \psi,\bot)$, with $\eta\neq\bot$. Then, by definition of the satisfaction relation, it must be the case that $M,v\Vdash^A \eta$, and $M,v\Vdash^A \eta\rightarrow\psi$. As our satisfaction relation is propositionally sound, we have $M,v\Vdash^A \psi$, and since we made no stipulation over $v$ other than $R_bwv$, we conclude that $M,w\Vdash^A \triangledown(\psi,\bot)$, which, since $\rho=\bot$, is what we wanted to conclude.
4. $\phi$ is one of the duality axioms. This is trivial, since $\triangle$ is defined in terms of $\triangledown$ exactly as postulated by the axiom.
5. $\phi$ was obtained from an application of a generalization rule. Let's handle one of them, again leaving the second one for the reader. So we have $\phi=\triangledown(\psi,\bot)$, and $\psi \in K_2$. This time, our inductive hypothesis is simply $\Vdash^A \psi$. But then we have that, for any world in any A-Kripke model, $\psi$ is satisfied there; in particular, we have that in any A-Kripke model $M=(W,R_a,R_b,V)$, for any pair of worlds $w,v$ such that $R_bwv$, $M,v\Vdash^A \psi$, and by the definition of $\Vdash^A$, $M,w\Vdash^A \triangledown(\psi,\bot)$, or simply, $M,v\Vdash^A \phi$. As this was proven for any model and world, we get $\Vdash^A \phi$.

Therefore, $K_2$ is correct with respect to $\Vdash^A$, and as we've reasoned before, we now know that $\triangledown(\top,\top)\notin K_2$, thus proving that $\triangledown(\top,\top)$ doesn't actually belong to all modal logics as defined in this question (and by the textbook). Since $\triangledown(\top,\top)$ is indeed a validity in the usual semantics, the given definition of modal logic is incomplete, in the proper logical sense of the word.

(As a final note, it is rather trivial to fix this definition. One simple way to go at is is by replacing the $\bot$ in the generalization rule with arbitrary formulas $\psi_1,...,\psi_n$, for each $\bot$ in the modal operator, though i'm not sure if this is the best one. Also, another development would be finding an actually complete semantics for this flawed definition of modal logic (or proving that there can't be one!); if someone has a link to that i'd be grateful.)

Answer 2

So I think that $\triangledown(\top,\top)$ does follow for all normal logics in the sense you have defined. The following would be a proof in any extension of the logic you have given.

A $\vdash\top$ by 1

B $\vdash\triangledown(\top,\bot)$ by 6

C $\vdash\triangledown(\top,\bot)\to(\triangledown(\top,\bot\to\top)\to\triangledown(\top,\top))$ by 4 and 3

D $\vdash\top\to\bot$ by 1

E $\vdash \triangledown(\top,\bot\to\top)$ by 6

Now apply MP twice to C. I think that would work unless I have misunderstood something.