A boolean-valued model is a generalization of an ordinary model where the set of truth values is any complete boolean lattice, instead of just the smallest one $\{ \bot, \top \}$.
I will nonstandardly define a nonclassical boolean-valued model as a boolean-valued model whose boolean lattice is not $\{\bot, \top\}$.
I've seen examples of Boolean-valued models used in discussions of forcing, but I'm looking for some other settings where one can use a nonclassical boolean-valued model. I'm particularly interested in looking for cases where one might want to use a boolean-valued model whose lattice isn't "syntactic" in nature (I think in the forcing example the lattice is a collection of wffs).
I'm wondering whether a paraconsistent model, defined below, can be analyzed as a special case of a boolean-valued model with $\{\varnothing, \{\bot\}, \{\top\}, \{\bot, \top\}\}$ as its boolean lattice.
A paraconsistent model seems to very strongly resemble a kind of partially degenerate boolean-valued model over $\{\varnothing, \{\bot\}, \{\top\}, \{\bot, \top\}\}$, but I'm wondering whether it is ruled out for technical reasons (such as not respecting the rules for the truth values of expressions headed by a quantifier, mishandling function symbols, picking both $\{\top\}$ and $\{\bot, \top\}$ as designated truth values, or failing some other similar condition).
What follows is an explanation and my attempt to understand the material.
I've seen an example something that seems similar used to describe paraconsistent arithmetic and paraconsistent models. In this setting, there are three truth values because there are no classical-truth-value gaps, but this can be viewed as a special case of Belnap's four-valued logic, where the neither truth value just happens not to be used.
In this lecture, Graham Priest discusses, among other things, inconsistent arithmetic.
The motivating application of a paraconsistent model is identify certain elements together in a classical structure in such a way that the equivalence relation is a congruence with respect to the function symbols in our signature. The predicate symbols and the axioms related to them, however, are not respected when collapsing the domain like this.
Predicates can be either true, false or both at every point the new domain. From the perspective of ${\bot, \top}$, we have truth value gluts but not truth value gaps. Let $D_0$ be the old domain and $D$ be the new domain. $D$ is a set of equivalence classes on $D_0$. If $\vec{v} \in D^n $, let $\varphi^{\leftarrow}(\vec{v})$ be the set of all elements of $D_0^n$ that $\vec{v}$ corresponds to.
If $P$ is a predicate symbol, then
$$ P(\vec{v}) \; \text{is true} \;\; \text{if and only if} \;\; \exists \vec{x} \in \varphi^{\leftarrow}(\vec{v}) \mathop. P(\vec{x}) $$
$$ P(\vec{v}) \; \text{is false} \;\; \text{if and only if} \;\; \exists \vec{x} \in \varphi^{\leftarrow}(\vec{v}) \mathop. \lnot P(\vec{x}) $$
However, we can talk about paraconsistent structures in their own right, without first deriving them from a classical structure.
We can define a pair of interpretation functions $\Delta^+$ and $\Delta^-$ that give us the extension and the anti-extension of a predicate symbol.
$$ P(\vec{x}) \; \text{holds} \;\; \textit{if and only if} \;\; \vec{x} \in \Delta^+(P) $$
$$ \lnot P(\vec{x}) \; \text{holds} \;\; \textit{if and only if} \;\; \vec{x} \in \Delta^-(P) $$
And also, for all predicates symbols $P$ where $P$ has arity $n$.
$$ \Delta^+(P) \cup \Delta^-(P) = D^n $$
Speculating a bit here, this is what I think the truth conditions are supposed to be for $\exists$ in a paraconsistent setting.
$$ \exists x \mathop. \varphi(x) \; \text{holds} \;\; \textit{if and only if} \;\; \text{there exists an $x$ such that $\varphi(x)$} $$
$$ \lnot \exists x \mathop. \varphi(x) \; \text{holds} \;\; \textit{if and only if} \;\; \text{for all $x$, $\lnot\varphi(x)$ holds} $$