I've heard of impossible worlds being used in modal logic before. (This question is one such question with an impossible world in it.) I don't understand exactly how they're intended to be used in the literature, so I'm trying to come up with a really simple formalism that only uses one of them and asking if it corresponds to an existing logic.
I have a universe with two worlds in it, a possible world $w$ and an impossible world $i$.
Let $M$, our model, consist of $M_V$ a set of primitive variables which hold at $w$ and $M_I$, a set of propositions that hold at our impossible world $p$.
Let $M_I$ be subject to the constraint that if $M, w \models \varphi$ holds, then $M, i \not\models \lnot \varphi$.
- $M, w \models A$ if and only if $A$ is in $M_V$.
- $M, w \models \varphi \land \psi$ if and only if $M, w \models \varphi$ and $M, w \models \psi$.
- $M, w \models \varphi \lor \psi$ if and only if $M, w \models \varphi$ or $M, w \models \psi$.
- $M, w \models \lnot \varphi$ if and only if $M, i \not\models \varphi$
- $M, i \models \varphi$ if and only if $\varphi$ is in $M_I$.
Let's distinguish $w$ as our start world, i.e. $\varphi$ is true if and only if it holds at $w$.
Right out of the gate, we have some rules that are shared with classical logic:
$$ \frac{A \land B}{A} \;\; \text{and} \;\; \frac{A}{A \lor B} $$
We also have double negation introduction:
$$ \frac{A}{\lnot \lnot A} $$
As proof, if $A$ holds at $w$, then $\lnot A$ does not hold at $i$ and thus $\lnot \lnot A$ holds at $w$.
However, we don't have double negation elimation, consider the model $M$ where:
- $V_M = \varnothing$
- $V_I = \varnothing$
$\lnot\lnot A$ holds at $w$, but $A$ doesn't hold at $w$.
This logic is paraconsistent. $A \land \lnot A$ is not necessarily a contradiction $(M_V = \{A\}, M_I = \varnothing)$.
By the same token $A \lor \lnot A$ is not necessarily true $(M_V = \{A\}, M_I = \{A\})$.