%
\label{thm:explosion-barrier}
Let $\mathrm{val} : \mathrm{Prop}_\tau \to \mathrm{Truth4}$
be a valuation assigning truth values
in the four-valued lattice
$\{\mathsf{T}, \mathsf{F}, \mathsf{B}, \mathsf{N}\}$.
Then:
\begin{enumerate}
    \item \textbf{Overdetermination does not explode.}
          If $\mathrm{val}(P) = \mathsf{B}$
          (i.e., $P$ is both true and false),
          then for an arbitrary proposition $Q$:
          \[
              \boxed{%
              \mathrm{val}(P) = \mathsf{B}
              \;\not\vdash\;
              \mathrm{val}(Q) = \mathsf{T}.}
          \]
          Specifically,
          $\mathrm{val}(P \Rightarrow Q)
          = \mathsf{B} \Rightarrow \mathrm{val}(Q)$,
          which equals $\mathsf{T}$ only if
          $\mathrm{val}(Q) \in \{\mathsf{T}, \mathsf{B}\}$,
          and equals $\mathsf{N}$ if
          $\mathrm{val}(Q) \in \{\mathsf{N}, \mathsf{F}\}$.
    \item \textbf{Underdetermination does not explode.}
          If $\mathrm{val}(P) = \mathsf{N}$,
          then $\mathrm{val}(P \Rightarrow Q)
          = \mathsf{N} \Rightarrow \mathrm{val}(Q)$,
          which is $\mathsf{T}$ only if
          $\mathrm{val}(Q) \in \{\mathsf{T}, \mathsf{N}\}$,
          and is $\mathsf{B}$ if
          $\mathrm{val}(Q) \in \{\mathsf{B}, \mathsf{F}\}$.
    \item \textbf{Classical explosion is preserved.}
          If $\mathrm{val}(P) = \mathsf{F}$,
          then $\mathrm{val}(P \Rightarrow Q) = \mathsf{T}$
          for all $Q$.
\end{enumerate}
In particular, \textbf{disjunctive syllogism fails}
for $\mathsf{B}$-valued propositions:
from $P \lor Q$ and $\lnot P$,
one cannot conclude $Q$
when $\mathrm{val}(P) = \mathsf{B}$.

All three statements follow by inspection
of the implication table
(Definition~\ref{def:truth4-material-implication}).

\textbf{Statement (1).}
The row $\mathsf{B} \Rightarrow \cdot$ is
$(\mathsf{T}, \mathsf{T}, \mathsf{N}, \mathsf{N})$:
\begin{align*}
    \mathsf{B} \Rightarrow \mathsf{T} &= \mathsf{T}, \\
    \mathsf{B} \Rightarrow \mathsf{B} &= \mathsf{T}, \\
    \mathsf{B} \Rightarrow \mathsf{N} &= \mathsf{N}, \\
    \mathsf{B} \Rightarrow \mathsf{F} &= \mathsf{N}.
\end{align*}
When $\mathrm{val}(Q) = \mathsf{F}$,
the implication $P \Rightarrow Q$ has value $\mathsf{N}$,
not $\mathsf{T}$.
Therefore the principle
``from $\mathrm{val}(P) = \mathsf{B}$,
derive $\mathrm{val}(Q) = \mathsf{T}$
for arbitrary $Q$''
fails:
the conclusion $Q$ inherits at most
the underdetermined value $\mathsf{N}$,
not the clean truth value $\mathsf{T}$.

\textbf{Statement (2).}
The row $\mathsf{N} \Rightarrow \cdot$ is
$(\mathsf{T}, \mathsf{B}, \mathsf{T}, \mathsf{B})$.
When $\mathrm{val}(Q) \in \{\mathsf{B}, \mathsf{F}\}$,
the implication has value $\mathsf{B}$,
not $\mathsf{T}$.

\textbf{Statement (3).}
The row $\mathsf{F} \Rightarrow \cdot$ is
$(\mathsf{T}, \mathsf{T}, \mathsf{T}, \mathsf{T})$:
genuine falsehood still implies anything,
exactly as in classical logic.

\textbf{Disjunctive syllogism failure.}
In classical logic,
disjunctive syllogism states:
from $P \lor Q$ and $\lnot P$, conclude $Q$.
Suppose $\mathrm{val}(P) = \mathsf{B}$.
Then $\mathrm{val}(P \lor Q) = \mathsf{B} \lor \mathrm{val}(Q)
= \mathsf{T}$ (or $\mathsf{B}$, depending on $\mathrm{val}(Q)$),
and $\mathrm{val}(\lnot P) = \lnot \mathsf{B} = \mathsf{N}$.
The conclusion requires extracting $Q$
from the disjunction $P \lor Q$
using $\lnot P$.
But $\mathrm{val}(\lnot P) = \mathsf{N} \neq \mathsf{T}$:
the negation of $P$ is underdetermined, not cleanly true,
so $P$ is not cleanly eliminated from the disjunction.
The disjunctive syllogism step fails.