4cm4cm3.5cm3.5cm

# Paraconsistent and Paracomplete Zermelo-Fraenkel Set Theory

Yurii Khomskii, Hrafn Valtýr Oddsson Amsterdam University College and Hamburg
University. ILLC, University of Amsterdam and Ruhr-Universität Bochum.

###### Abstract

We present a novel treatment of set theory in a four-valued paracomplete and
paraconsistent logic, i.e., a logic in which propositions can be neither true
nor false, and can be both true and false. By prioritising a system with an
ontology of non-classical sets that is easy to understand and apply in
practice, our approach overcomes many of the obstacles encountered in previous
attempts at such a formalization.

We propose an axiomatic system $\mathrm{BZFC}$, obtained by analysing the
$\mathrm{ZFC}$-axioms and translating them to a four-valued setting in a
careful manner. We introduce the anti-classicality axiom postulating the
existence of non-classical sets, and prove a surprising results stating that
the existence of a single non-classical set is sufficient to produce any other
type of non-classical set.

We also look at bi-interpretability results between $\mathrm{BZFC}$ and
classical $\mathrm{ZFC}$, and provide an application concerning Tarski
semantics, showing that the classical definition of the satisfaction relation
yields a logic precisely reflecting the non-classicality in the meta-theory.

MSC2020 Classification: 03E70, 03B53, 03B60

Keywords: Non-classical set theory; paraconsistent set theory; paraconsistent
logic; paraconsistent and paracomplete set theory

##  1 Introduction

The classical Zermelo-Fraenkel axiom system $\mathrm{ZFC}$ is generally
accepted as the foundation of all mathematics. $\mathrm{ZFC}$ is formalized in
classical logic in which any statement is either true or false, and cannot be
both at the same time. Throughout the course of the 20th century, there has
been a continuous interest in foundations of mathematics formalized in various
non-classical logics. The most notable examples are constructive set theories,
such as $\mathrm{IZF}$, $\mathrm{CZF}$ and $\mathrm{CST}$, proposed by Harvey
Friedman [11], John Myhill [18] and Peter Aczel [1] among others. These
theories are based in intuitionistic logic and aim to formalize the
constructive side of mathematics.

A more significant departure from classical logic would be a _paraconsistent_
set theory, i.e., a set theory in which statements can be both true and false
at the same time. For such a theory to be non-trivial, the underlying logic
must, at the very least, fail to satisfy the ex falso quodlibet principle.
Attempts at such a formalization have independently been proposed by various
authors to a various degree of success, see, e.g., [16, 13] and the more
recent [8]. Sometimes, a motivating factor was the desire to adopt some form
of full comprehension as an axiom and avoid Russell’s paradox.

In this paper, we are explicitly _not_ concerned with full comprehension. In
our view, Russell’s paradox is a natural consequence of the distinction
between formal language and meta-language, and not something that needs to be
avoided. Instead, we prioritise an intuitive treatment of non-classical sets
so as to make our theory accessible to the classical mathematician used to
working in $\mathrm{ZFC}$.

We propose a natural formalization of set theory in the logic $\mathrm{BS4}$.
This is a four-valued, paraconsistent and paracomplete predicate logic based
on developments by Dunn [10], Belnap [6, 7] and [4]. The propositional
fragment of $\mathrm{BS4}$ appeared under the name $\mathsf{CLoNs}$ in [5],
and our version is essentially due to Omori, Sano and Waragai [20, 23] (from
where we also take its name). In the semantics of $\mathrm{BS4}$, truth and
falsity are formally separated, so a statement $\varphi$ can be true and not
false ($1$), false and not true ($0$), both true and false ($\mathfrak{b}$),
or neither true nor false ($\mathfrak{n}$). We formulate an axiomatic system
called $\mathrm{BZFC}$, based on a careful generalisation of $\mathrm{ZFC}$,
together with the _anti-classicality axiom_ postulating the existence of non-
classical sets.

In our opinion, previous attempts at a similar approach have not been fully
successful. We conjecture that this is, in part, due to an insufficiently
careful treatment of the language of set theory. For example, in our logic
$\mathrm{BS4}$, there are two types of negations: the (native) paraconsistent
negation and the (defined) classical negation. Likewise, there are two types
of implications: the native implication, and the (defined) strong implication.
When formulating the axioms of our set theory, a careful approach is needed to
determine what the proper generalization of each axiom should be. For
instance, we think the failure to properly address this issue is one of the
reason that the approach in [8] has not been fully successful.

Our theory will come together with a clear and intuitive ontology where a non-
classical set $u$ can be described by a positive extension (the collection of
all $x$ such that $x\in u$ is true) and a negative extension (the collection
of all $x$ such that $x\in u$ is false),111Since the negative extension is, in
general, a proper class, we will actually talk about the complement of the
negative extension and call it the $?$-extension, see Section 3. and this can
be expressed within the system. The universe of non-classical sets naturally
extends the classical _von Neumann_ universe of sets, and every model of
$\mathrm{BZFC}$ contains within it a natural model of $\mathrm{ZFC}$ given by
the “hereditarily classical” sets. On the other hand, starting in
$\mathrm{ZFC}$ one can produce a natural model of $\mathrm{BZFC}$, leading to
an intuitive bi-interpretability between the two theories.222The situation is
analogous to Peter Aczel’s theory of non-well-founded sets [2], which can be
viewed as another enrichment of the von Neumann universe, itself consistent
relative to $\mathrm{ZFC}$ and containing within it a natural copy of a model
of $\mathrm{ZFC}$.

This paper is almost entirely self-contained—in particular, no prior knowledge
of paraconsistent logic is required. In Section 2 we provide the syntax and
semantics of the logic $\mathrm{BS4}$ which is used to set up the theory. In
Sections 3 and 4 we first motivate and then postulate the axiomatic system
$\mathrm{PZFC}$, and in Section 5 we add the Anti-Classicality Axiom to obtain
the full theory $\mathrm{BZFC}$. Sections 6, 7 and 8 are devoted to the
construction of models and bi-interpretability with $\mathrm{ZFC}$, and
finally, Section 9 is devoted to a question of philosophical interest: how
does formal model theory (using Tarski semantics) depend on the logical
properties of the ambient meta-theory in which it is defined?

The work in this paper was carried out in the course of the Master’s thesis of
the second author [19]. On occasion, we will refer to the thesis which goes in
more depth on some points, and contains more details which have been left out
of this paper for clarity.

##  2 The Logic $\mathrm{BS4}$

The logic $\mathrm{BS4}$ is due to [23] with the exception that we take the
contradictory constant $\bot$ as primary instead of the classicality operator
$\circ$. We start by introducing $\mathrm{BS4}$ from a semantic point of view.
In this section, the meta-theory is classical mathematics, e.g.,
$\mathrm{ZFC}$.333For more about formalizing the semantics of $\mathrm{BS4}$
within $\mathrm{BZFC}$, see Section 9.

###  2.1 Syntax and Semantics

The main idea behind $\mathrm{BS4}$ is the separation of truth from falsity,
i.e., if $\varphi$ is a sentence and $\mathcal{M}$ a model, then $\varphi$ can
be or not be true in $\mathcal{M}$ and, independently, can be or not be false
in $\mathcal{M}$. This is achieved by considering two satisfaction relations,
$\models^{T}$ and $\models^{F}$, separating the inductive definition for the
logical connectives and quantifiers, and considering two interpretation of all
predicate symbols (a “true” and a “false” interpretation). For convenience we
will consider vocabularies without function symbols.

######  Definition 2.1.

(The Syntax of $\mathrm{BS4}$)

The syntax of $\mathrm{BS4}$ is the usual syntax of first order logic, except
that we use “$\sim$” to denote negation. We also use the constant connective
$\bot$.

######  Definition 2.2.

(T/F-models)

Suppose $\tau$ is a vocabulary with constant and relation symbols. A T/F-model
$\mathcal{M}$ consist of a domain $M$ together with the following:

  * •

An element $c^{\mathcal{M}}\in M$ for every constant symbol $c$.

  * •

For every $n$-ary relation symbol $R$, a “positive” interpretation
$(R^{\mathcal{M}})^{+}\subseteq M^{n}$ and a “negative” interpretation
$(R^{\mathcal{M}})^{-}\subseteq M^{n}$.

  * •

A binary relation $=^{+}$ which coincides with the true equality relation; and
a binary relation $=^{-}$ satisfying $a=^{-}b$ iff $b=^{-}a$.

######  Definition 2.3.

(T/F-semantics for $\mathrm{BS4}$)

Suppose $\tau$ is a vocabulary without function symbols and $\mathcal{M}$ a
T/F-model. We define two relations, $\models^{T}$ and $\models^{F}$, by
induction on the complexity of $\varphi$:

  1. 1.

$\mathcal{M}\models^{T}(t=s)[a,b]\;\;\;\Leftrightarrow\;\;\;a=^{+}b$.

$\mathcal{M}\models^{F}(t=s)[a,b]\;\;\;\Leftrightarrow\;\;\;a=^{-}b$.

  2. 2.

$\mathcal{M}\models^{T}R(t_{1},\dots,t_{n})[a_{1}\dots
a_{n}]\;\;\;\Leftrightarrow\;\;\;R^{+}(a_{1},\dots,a_{n})$ holds.

$\mathcal{M}\models^{F}R(t_{1},\dots,t_{n})[a_{1}\dots
a_{n}]\;\;\;\Leftrightarrow\;\;\;R^{-}(a_{1},\dots,a_{n})$ holds.

  3. 3.

$\mathcal{M}\models^{T}{\sim}\varphi\;\;\;\Leftrightarrow\;\;\;\mathcal{M}\models^{F}\varphi$.

$\mathcal{M}\models^{F}{\sim}\varphi\;\;\;\Leftrightarrow\;\;\;\mathcal{M}\models^{T}\varphi$.

  4. 4.

$\mathcal{M}\models^{T}\varphi\land\psi\;\;\;\Leftrightarrow\;\;\;\mathcal{M}\models^{T}\varphi$
and $\mathcal{M}\models^{T}\psi$.

$\mathcal{M}\models^{F}\varphi\land\psi\;\;\;\Leftrightarrow\;\;\;\mathcal{M}\models^{F}\varphi$
or $\mathcal{M}\models^{F}\psi$.

  5. 5.

$\mathcal{M}\models^{T}\varphi\lor\psi\;\;\;\Leftrightarrow\;\;\;\mathcal{M}\models^{T}\varphi$
or $\mathcal{M}\models^{T}\psi$.

$\mathcal{M}\models^{F}\varphi\lor\psi\;\;\;\Leftrightarrow\;\;\;\mathcal{M}\models^{F}\varphi$
and $\mathcal{M}\models^{F}\psi$.

  6. 6.

$\mathcal{M}\models^{T}\varphi\to\psi\;\;\;\Leftrightarrow\;\;\;$ if
$\mathcal{M}\models^{T}\varphi$ then $\mathcal{M}\models^{T}\psi$.

$\mathcal{M}\models^{F}\varphi\to\psi\;\;\;\Leftrightarrow\;\;\;\mathcal{M}\models^{T}\varphi$
and $\mathcal{M}\models^{F}\psi$.

  7. 7.

$\mathcal{M}\models^{T}\varphi\leftrightarrow\psi\;\;\;\Leftrightarrow\;\;\;$
($\mathcal{M}\models^{T}\varphi$ if and only if $\mathcal{M}\models^{T}\psi$).

$\mathcal{M}\models^{F}\varphi\leftrightarrow\psi\;\;\;\Leftrightarrow\;\;\;$
($\mathcal{M}\models^{T}\varphi$ and $\mathcal{M}\models^{F}\psi$) or
($\mathcal{M}\models^{F}\varphi$ and $\mathcal{M}\models^{T}\psi$).

  8. 8.

$\mathcal{M}\models^{T}\exists
x\varphi(x)\;\;\;\Leftrightarrow\;\;\;\mathcal{M}\models^{T}\varphi[a]$ for
some $a\in M$.

$\mathcal{M}\models^{F}\exists
x\varphi(x)\;\;\;\Leftrightarrow\;\;\;\mathcal{M}\models^{F}\varphi[a]$ for
all $a\in M$.

  9. 9.

$\mathcal{M}\models^{T}\forall
x\varphi(x)\;\;\;\Leftrightarrow\;\;\;\mathcal{M}\models^{T}\varphi[a]$ for
all $a\in M$.

$\mathcal{M}\models^{F}\forall
x\varphi(x)\;\;\;\Leftrightarrow\;\;\;\mathcal{M}\models^{F}\varphi[a]$ for
some $a\in M$.

  10. 10.

$\mathcal{M}\models^{T}\bot\;\;\;\Leftrightarrow\;\;\;$ never.

$\mathcal{M}\models^{F}\bot\;\;\;\Leftrightarrow\;\;\;$ always.

If $\mathcal{M}\models^{T}\varphi$ then we say that $\varphi$ is true in
$\mathcal{M}$, and if $\mathcal{M}\models^{F}\varphi$ then we say that
$\varphi$ is false in $\mathcal{M}$.

######  Definition 2.4.

(Semantic consequence) If $\Sigma$ is a set of formulas and $\varphi$ another
formula, then semantic consequence is defined by

$\Sigma\vdash_{\mathrm{BS4}}\varphi$

iff for every T/F-model $\mathcal{M}$, if $\mathcal{M}\models^{T}\Sigma$ then
$\mathcal{M}\models^{T}\varphi$.

######  Remark 2.5.

While most of the inductive steps in Definition 2.3 are unsurprising, there
are two points that need to be addressed:

  1. 1.

The symbol “$\bot$” should be understood as more than merely a contradiction.
While many classical contradictions such as $\varphi\land{\sim}\varphi$ will
be satisfiable, the symbol $\bot$ stands for a much stronger contradiction,
i.e., one which is not satisfiable even in “paraconsistent” models. Some
readers might find the addition of $\bot$ to the logic distasteful as it seems
to run counter to the idea of paraconsistent logic. However, when dealing with
a vocabulary $S$ with only finitely many relation symbols, one can consider
the following sentence:

$\forall x\forall y(x=y\land x\neq y)\land\bigwedge_{R\in S}\forall
x_{1}\dots\forall x_{n}(R(x_{1},...,x_{n})\land{\sim}R(x_{1},...,x_{n})).$

This sentence is satisfiable, but only in the trivial model consisting of
exactly one object $a$, which is both equal and not equal to itself ($a=^{+}a$
and $a=^{-}a$) and for which all relation-interpretations are true and false.
Adding “$\bot$” to the language is equivalent to disregarding this trivial
model. Since we focus on set theory, we will have no interest in such a model
and thus have no reservations about $\bot$.

  2. 2.

The truth-definition for the material implication $\varphi\to\psi$ is designed
to reflect semantic consequence and guarantee that $\mathrm{BS4}$ satisfies
the deduction theorem. This definition may be debatable, because (together
with $\bot$) it will allows us to define classical negation, and to refer not
only to truth and falsity, but also to the absence of truth and/or falsity,
from within the system. But this should not be seen as a drawback of the
system. In fact, the original formulation of $\mathrm{BS4}$ from [23]
explicitly contained a “classicality” operator.

######  Definition 2.6.

(Truth value) For every $\varphi$ and T/F-model $\mathcal{M}$ we define:

$\llbracket\varphi\rrbracket^{\mathcal{M}}\;\;:=\;\;\begin{cases}1&\text{if
}\mathcal{M}\models^{T}\varphi\text{ and }\mathcal{M}\not\models^{F}\varphi\\\
\mathfrak{b}&\text{if }\mathcal{M}\models^{T}\varphi\text{ and
}\mathcal{M}\models^{F}\varphi\\\ \mathfrak{n}&\text{if
}\mathcal{M}\not\models^{T}\varphi\text{ and
}\mathcal{M}\not\models^{F}\varphi\\\ 0&\text{if
}\mathcal{M}\not\models^{T}\varphi\text{ and }\mathcal{M}\models^{F}\varphi\\\
\end{cases}$

We can now view $\mathrm{BS4}$ as a four-valued logic with truth tables for
propositional connectives given in Table 1.

| ${\sim}$
---|---
1 | 0
$\mathfrak{b}$ | $\mathfrak{b}$
$\mathfrak{n}$ | $\mathfrak{n}$
0 | 1

$\land$ | 1 | $\mathfrak{b}$ | $\mathfrak{n}$ | 0
---|---|---|---|---
1 | 1 | $\mathfrak{b}$ | $\mathfrak{n}$ | 0
$\mathfrak{b}$ | $\mathfrak{b}$ | $\mathfrak{b}$ | 0 | 0
$\mathfrak{n}$ | $\mathfrak{n}$ | 0 | $\mathfrak{n}$ | 0
0 | 0 | 0 | 0 | 0

$\lor$ | 1 | $\mathfrak{b}$ | $\mathfrak{n}$ | 0
---|---|---|---|---
1 | 1 | 1 | 1 | 1
$\mathfrak{b}$ | 1 | $\mathfrak{b}$ | 1 | $\mathfrak{b}$
$\mathfrak{n}$ | 1 | 1 | $\mathfrak{n}$ | $\mathfrak{n}$
0 | 1 | $\mathfrak{b}$ | $\mathfrak{n}$ | 0

$\rightarrow$ | 1 | $\mathfrak{b}$ | $\mathfrak{n}$ | 0
---|---|---|---|---
1 | 1 | $\mathfrak{b}$ | $\mathfrak{n}$ | 0
$\mathfrak{b}$ | 1 | $\mathfrak{b}$ | $\mathfrak{n}$ | 0
$\mathfrak{n}$ | 1 | 1 | 1 | 1
0 | 1 | 1 | 1 | 1

$\leftrightarrow$ | 1 | $\mathfrak{b}$ | $\mathfrak{n}$ | 0
---|---|---|---|---
1 | 1 | $\mathfrak{b}$ | $\mathfrak{n}$ | 0
$\mathfrak{b}$ | $\mathfrak{b}$ | $\mathfrak{b}$ | $\mathfrak{n}$ | 0
$\mathfrak{n}$ | $\mathfrak{n}$ | $\mathfrak{n}$ | 1 | 1
0 | 0 | 0 | 1 | 1

Table 1: Truth tables for the propositional connectives of $\mathrm{BS4}$

###  2.2 Defined connectives

We will need several defined connectives to make the presentation more smooth
and intuitive.

First we look at material implication: notice that
$\mathcal{M}\models^{T}\varphi\to\psi$ tells us that if $\varphi$ is true in
$\mathcal{M}$ then $\psi$ is true in $\mathcal{M}$, but does not tell us that
if $\psi$ is false in $\mathcal{M}$ then $\varphi$ is false in $\mathcal{M}$,
as can easily be verified. Similarly, a bi-implication
$\varphi\leftrightarrow\psi$ tells us that, in a model $\mathcal{M}$,
$\varphi$ is true iff $\psi$ is true, but not that $\varphi$ is false iff
$\psi$ is false. In particular, $\varphi\leftrightarrow\psi$ does not allow us
(as we are used from classical logic) to substitute an arbitrary occurrences
of $\varphi$ with $\psi$ within a larger formula.

For this reason, we define the following abbreviations, which we call strong
implication and strong bi-implication, respectively.444The strong implication
appears, e.g., in [22, Chapter XII].

  * •

$\varphi\Rightarrow\psi\;\;\;\text{abbreviates}\;\;\;(\varphi\rightarrow\psi)\land({\sim}\psi\rightarrow{\sim}\varphi)$

  * •

$\varphi\Leftrightarrow\psi\;\;\;\text{abbreviates}\;\;\;(\varphi\leftrightarrow\psi)\land({\sim}\varphi\leftrightarrow{\sim}\psi).$

In particular, if $\varphi\Leftrightarrow\psi$ is true then any occurrence of
$\varphi$ may be substituted with $\psi$ and vice versa. The distinction
between regular and strong implication and bi-implication will play a crucial
role in the generalization of the axioms of set theory.

Next, following up on Remark 2.5 we define classical negation as follows:

  * •

$\neg\varphi\;\;\;\text{abbreviates}\;\;\;\varphi\rightarrow\bot$

One can easily check that $\mathcal{M}\models^{T}\lnot\varphi$ iff
$\mathcal{M}\not\models^{T}\varphi$ while $\mathcal{M}\models^{F}\lnot\varphi$
iff $\mathcal{M}\models^{T}\varphi$. So in a model $\mathcal{M}$,
$\lnot\varphi$ can be either true and not false (when
$\mathcal{M}\models^{T}\varphi$) or false and not true (when
$\mathcal{M}\not\models^{T}\varphi$). Using classical negation as a defined
notion we can talk about presence and absence of truth and falsity (and, more
generally, specify the truth value of a formula) from within the system. We
will use the following important abbreviations:

  * •

$!\varphi\;\;\;\text{abbreviates}\;\;\;{\sim}\lnot\varphi$

  * •

$?\varphi\;\;\;\text{abbreviates}\;\;\;\lnot{\sim}\varphi$

We think of $!\varphi$ as presence of truth and $?\varphi$ as absence of
falsity. The truth tables for ${\sim},\lnot,!$ and $?$ in Table 2 make this
clear. Notice that $\lnot\varphi$, $!\varphi$ and $?\varphi$ will always have
truth value $1$ or $0$. Moreover, the truth value of $\lnot\varphi$ and
$!\varphi$ depends only on whether $\varphi$ was true in the model, and
completely disregards whether $\varphi$ was false. Similarly, $?\varphi$
depends only on whether $\varphi$ was false and disregards whether it was
true.

$\varphi$ | ${\sim}\varphi$ | $\lnot\varphi$ | $!\varphi$ | $?\varphi$
---|---|---|---|---
1 | 0 | 0 | 1 | 1
$\mathfrak{b}$ | $\mathfrak{b}$ | 0 | 1 | 0
$\mathfrak{n}$ | $\mathfrak{n}$ | 1 | 0 | 1
$0$ | 1 | 1 | 0 | 0
Table 2: Truth table for ${\sim},\lnot,!$ and $?$.

A $\mathrm{BS4}$-formula is _complete_ if it can never obtain the truth-value
$\mathfrak{n}$, and consistent if it can never obtain the truth-value
$\mathfrak{b}$. It is called _classical_ if it is both complete and
consistent, i.e., if in every model it has truth-value $1$ or $0$. In
particular, $\lnot\varphi$, $!\varphi$ and $?\varphi$ are classical formulas
for any $\varphi$. Notice also that classicality, completeness and consistency
can each be expressed within the system, by
${!}\varphi\leftrightarrow{?}\varphi$, ${?}\varphi\to{!}\varphi$ and
$!\varphi\to?\varphi$ respectively. We will use the following abbreviation in
accordance to [4]:

  * •

$\circ\varphi\;\;\;\text{abbreviates}\;\;\;{!}\varphi\leftrightarrow{?}\varphi$

###  2.3 Proof system

A sound and complete proof calculus for the propositional fragment of
$\mathrm{BS4}$ is presented in [23]. We present a slightly modified but
equivalent version, consisting of the following axioms and rules of inference:

  * •

Axioms of classical predicate logic:

    1. 1.

$\varphi\rightarrow(\psi\rightarrow\varphi)$

    2. 2.

$(\varphi\rightarrow(\psi\rightarrow\chi))\rightarrow\\\
((\varphi\rightarrow\psi)\rightarrow(\varphi\rightarrow\chi))$

    3. 3.

$\varphi\lor(\varphi\rightarrow\psi)$

    4. 4.

$(\varphi\wedge\psi)\rightarrow\varphi$

    5. 5.

$(\varphi\wedge\psi)\rightarrow\psi$

    6. 6.

$\varphi\rightarrow(\psi\rightarrow(\varphi\wedge\psi))$

    7. 7.

$\varphi\rightarrow(\varphi\vee\psi)$

    8. 8.

$\psi\rightarrow(\varphi\vee\psi)$

    9. 9.

$(\varphi\rightarrow\chi)\rightarrow((\psi\rightarrow\chi)\rightarrow\\\
((\varphi\vee\psi)\rightarrow\chi))$

    10. 10.

$\bot\rightarrow\varphi$

    11. 11.

$\forall x\varphi(x)\rightarrow\varphi(t)$

    12. 12.

$\varphi(t)\rightarrow\exists x\varphi(x)$

    13. 13.

$x=x$

    14. 14.

$x=y\rightarrow(\varphi(x)\rightarrow\varphi(y))$

  * •

Axioms for negation:

    1. 15.

${\sim}{\sim}\varphi\leftrightarrow\varphi$

    2. 16.

${\sim}(\varphi\wedge\psi)\leftrightarrow({\sim}\varphi\vee{\sim}\psi)$

    3. 17.

${\sim}(\varphi\vee\psi)\leftrightarrow({\sim}\varphi\wedge{\sim}\psi)$

    4. 18.

${\sim}(\varphi\rightarrow\psi)\leftrightarrow(\varphi\wedge{\sim}\psi)$

    5. 19.

${\sim}\bot$

    6. 20.

${\sim}\forall x\varphi\leftrightarrow\exists x{\sim}\varphi$

    7. 21.

${\sim}\exists x\varphi\leftrightarrow\forall x{\sim}\varphi$

    8. 22.

${\sim}(x=y)\rightarrow{\sim}(y=x)$.555Axiom 22 does not occur in the original
formulation in [23], but we need to add it to take care of the semantic
requirement that $=^{-}$ is a symmetric relation.

  * •

The rules of inference:

    * –

From $\varphi$ and $\varphi\rightarrow\psi$, infer $\psi$ (modus ponens).

    * –

Infer $\varphi\rightarrow\forall x\psi$ from $\varphi\rightarrow\psi$,
provided $x$ does not occur free in $\varphi.$

    * –

Infer $\exists x\varphi\rightarrow\psi$ from $\varphi\rightarrow\psi$,
provided $x$ does not occur free in $\psi.$

######  Lemma 2.7.

The calculus described above is sound and complete with respect to
T/F-semantics.

###### Proof.

This follows from [23, Corollary 5.15], after an adaptation to refer to $\bot$
as the primary symbol as opposed to the classicality operator $\circ$. We
leave out the details. ∎

In practice, we will reason informally within the system $\mathrm{BS4}$ using
arguments which can, in principle, be formalized in the calculus. We will
often be referring to the defined connectives as well. Below, we specifically
mention a few provable statements concerning defined connectives which will
frequently be needed in later arguments.

######  Lemma 2.8.

The following statements are provable in $\mathrm{BS4}$:

  * •

$\varphi\leftrightarrow\;!\varphi$

  * •

${\sim}\varphi\leftrightarrow{\sim}?\varphi$

(This describes the fact that $!$ talks only about truth and $?$ only about
faslity.)

  * •

$x=y\rightarrow(\varphi(x)\Leftrightarrow\varphi(y))$

(This says that a true equality allows us to interchange terms).

  * •

${\circ\varphi}\;\;\to\;\;((\varphi\Leftrightarrow\;!\varphi)\land(\varphi\Leftrightarrow\;?\varphi))$

  * •

${\circ\varphi}\;\;\to\;\;({\sim}\varphi\Leftrightarrow\lnot\varphi)$

  * •

${\circ\varphi\land\circ\psi}\;\;\to\;\;((\varphi\to\psi)\Leftrightarrow(\varphi\Rightarrow\psi))$

(The last three points say that for classical formulas there is no
distinctions between strong and weak implication, between native and classical
negation, and that $!$ and $?$ may be dropped.)

##  3 Non-classical sets

Before delving into the axioms, it is helpful to think about the concept of a
set in a paraconsistent and paracomplete setting from a naive point of view.
In classical ZFC, a set $x$ is identified with the class of its elements
$\\{y:y\in x\\}$ and divides the entire universe of sets in two parts: those
$y$ that are in $x$, and those $y$ that are not in $x$. In the context of
paraconsistent and paracomplete logic, we can have a situation where a set $y$
is both in $x$ and not in $x$, or a situation where $y$ is neither in $x$, nor
is it the case that $y$ is not in $x$.

Therefore, it seems natural to identify a set $x$ with the pair consisting of
a positive extension $\\{y:y\in x\\}$ and a negative extension $\\{y:y\notin
x\\}$666We write $y\notin x$ instead of ${\sim}(y\in x)$. without the added
requirement that one is the complement of the other. In fact, it makes sense
to call a set consistent if its positive and negative extensions do not
intersect, complete if their union is the whole universe, and classical if it
is both consistent and complete.

There is, however, an asymmetry between the positive and negative extensions:
$\\{y:y\in x\\}$ is a set while $\\{y:y\notin x\\}$ is a proper class.
Therefore, it turns out to be more appropriate to talk about the complement of
the negative extension, i.e., the collection of all $y$ for which the
statement “$y\notin x$” is not true, or, equivalently, for which the statement
“$y\in x$” is not false). We will refer to this collection as the ?-extension
of $x$.

Above, we have naively referred to statements being true or false, which, a
priori, seem to be meta-theoretic notions. However, recall that the operators
$!$ and $?$ allow us to discuss truth and falsity from within the system as
well. In particular, $!(y\in x)$ is true if and only if $y\in x$ is true, and
$?(y\in x)$ is true if and only if $y\in x$ is not false. This motivates the
following

######  Definition 3.1.

Let $x$ be a set:

  * •

The !-extension of $x$ is

$x^{!}:=\\{y\;:\;\;!(y\in x)\\}$

  * •

The ?-extension of $x$ is

$x^{?}:=\\{y\;:\;\;?(y\in x)\\}$

For the time being, it is not clear that the above collections describe sets
and not proper classes, but we shall set up the axiomatic framework in such a
way that if $x$ is a set, then both $x^{!}$ and $x^{?}$ are sets. The four
boolean combinations of $x^{!}$ and $x^{?}$ determine the classes consisting
of all $y$ for which the statement “$y\in x$” has one of the four possible
truth-values, as visualized in Figure 1.

We remark that the property of sets being complete, consistent and classical
can be expressed within the system. In fact the following holds:777For now,
the symbols $=$ and $\subseteq$ should be understood informally; this will be
made precise later.

  * •

$x$ is complete if $x^{?}\subseteq x^{!}$

  * •

$x$ is consistent if $x^{!}\subseteq x^{?}$

  * •

$x$ is classical if $x^{!}=x^{?}$

The intuition is that classical sets behave as we are used to in
$\mathrm{ZFC}$: in particular, it does not matter whether we consider the
native negation $\sim$ or classical negation $\neg$, nor whether we use $\to$
or $\Rightarrow$. It is not hard to see that $(x^{!})^{!}=(x^{!})^{?}=x^{!}$
and $(x^{?})^{!}=(x^{?})^{?}=x^{?}$, so the !-extension and ?-extension
themselves are classical sets.

$x^{!}$$x^{?}$$\mathfrak{b}$1$\mathfrak{n}$0 Figure 1: The four truth values
of “$y\in x$” depending on the boolean combination of $x^{!}$ and $x^{?}$.

Let us now look more closely at the notion of equality of two sets and the
extensionality principle.888Although we have already used notation such as
“$x=y$” and even “$x\subseteq y$” without properly defining it, in fact we
only used them for classical sets, in which case it means the same thing as in
classical ZFC. In ZFC, two sets are equal precisely if the classes of their
elements are the same; equivalently, two sets are different precisely if one
set contains an element which the other does not, or vice versa.

In our setting, $x=y$ and $x\neq y$ could both be true statements999Again, we
write $x\neq y$ instead of ${\sim}(x=y)$. or it could happen that neither
$x=y$ nor $x\neq y$ are true statements. But we still require that “$x=y$”
express the idea that $x$ and $y$ are the same set-theoretic objects, meaning
that both its !-extension and ?-extension must be the same. Likewise, we still
want “$x\neq y$” to express that there is something in $x$ which is not in
$y$, or vice versa. So the guiding principle behind the extensionality axiom
must be the following:

  * •

$x=y\;\;\leftrightarrow\;\;(x^{!}=y^{!}\land x^{?}=y^{?})$

  * •

$x\neq y\;\;\leftrightarrow\;\;\exists z((z\in x\land z\notin y)\lor(z\in
y\land z\notin x))$

Figure 2 illustrates the situation in which two sets $x$ and $y$ are equal
(because their !-extensions and ?-extensions are the same) but also unequal
(because there is a set $z$ such that $z\in x$ but $z\notin y$). In fact, if
$x$ is any inconsistent set, then $x=x$ and $x\neq x$.

$x^{!}=y^{!}$$x^{?}=y^{?}$$\bullet$$z\in x$$z\notin y$ Figure 2: $x=y$ and
$x\neq y$.

It is customary in set theory to use notation such as $\\{y:\varphi(y)\\}$ to
refer to the set (if it exists) of all objects $y$ satisfying property
$\varphi$. In our setting, where a set is determined by its !-extension and
?-extension, it makes sense to agree on the following:

######  Convention 3.2.

$x=\\{y:\varphi(y)\\}\;\;\;\;\text{ abbreviates }\;\;\;\;\forall y\;(y\in
x\;\Leftrightarrow\;\varphi(y)).$

The use of the strong implication means that $x^{!}$ is the set of all $y$ for
which $\varphi(y)$ is true, and $x^{?}$ is the set of all $y$ for which
$\varphi(y)$ is not false.

Notably, our theory does not, and does not attempt to, satisfy full
comprehension or avoid Russell’s paradox. In fact, the same proof as usual
shows that $R:=\\{x:\lnot(x\in x)\\}$ is a proper class and not a set.
Likewise, the universe of all sets does not form a set.

A last point of subtlety should be discussed: how do we understand notation
such as $\\{u\\}$, for a set $u$? One might initially assume that this is
$\\{y:y=u\\}$ (referring to Convention 3.2). However, a closer look reveals
the following: if $\\{y:y=u\\}$ is a set, then we would like its $?$-extension
to also be a set. However, a bit of work following the definitions shows that
this $?$-extension would be the collection of all sets $a$ such that
$a^{!}\subseteq u^{?}$ and $u^{!}\subseteq a^{?}$. Since there is no upper
bound on $a^{?}$, it would seem (following classical intuition) that there are
class-many sets $a$ satisfying this condition, meaning that the ?-extension of
this set is, in fact, a proper class.101010We will provide a proper proof of
this result in Lemma 5.5

Instead, we opt for the following:

######  Convention 3.3.

If $u$ is a set, then $\\{u\\}$ is the set $\\{y\>:\>!(y=u)\\}$; and more
generally if $u_{0},\dots,u_{n}$ are sets, then $\\{u_{0},\dots,u_{n}\\}$ is
the set $\\{y\>:\>\>!(y=u_{0})\lor\dots\lor!(y=u_{n})\\}$. This is always a
classical set whose !-extension and ?-extension are exactly the finite set
consisting of the elements in question.

A similar phenomenon occurs with other set-theoretic operations, most notably
the power set operation.

##  4 The theory $\mathrm{PZFC}$

We will now present the axiomatic system in this. The first step is to
formulate an appropriate generalization of the $\mathrm{ZFC}$ axioms, which is
the task of the current section. It will give rise to the theory
$\mathrm{PZFC}$, which is an intermediate step to the full theory
$\mathrm{BZFC}$ presented in the next section.

Here it is important to have a careful look, and put in some additional
effort, to make sure that the axioms are translated in accordance with the
intuition described in the previous section. For this to succeed, it is
usually not enough to merely re-interpret the $\mathrm{ZFC}$ axioms in our
logic.

###  4.1 Extensionality

The first and most essential axiom needed to sustain an ontology of sets is
the following version of the extensionality axiom.

$\textbf{Extensionality: }\;\;\;\;\;\boldsymbol{\forall x\forall
y(x=y\;\Leftrightarrow\;\forall z(z\in x\Leftrightarrow z\in y))}.$

Why do we choose strong rather than weak bi-implications? For the first one
the choice is clear: extensionality seeks to define the meaning of the
expression “$x=y$” in terms of the elements of $x$ and $y$, and this needs to
talk both about truth and falsity. Notice that the use of this strong
implications allows us to interchange the expression “$x=y$” with the
expression on the right-hand side within any given formula.

The second bi-implication is more interesting: recall that we want $x=y$ to
express that both the !-extension and ?-extension of $x$ and $y$ coincide. The
statement with a weak implication $\forall z(z\in x\leftrightarrow z\in y))$
would only say that the !-extensions coincide.

At this point it is instructive to define subsets:

$x\subseteq y\;\;\;\text{abbreviates}\;\;\;\forall z\;(z\in x\Rightarrow z\in
y)$

Again, the use of the strong implication makes sure that $x\subseteq y$ says
that both the !-extensions and ?-extensions of $x$ are included in that of
$y$. In particular, the Axiom of Extensionality can now be reformulated as
follows: $\forall x\forall y(x=y\;\Leftrightarrow\;x\subseteq y\land
y\subseteq x)$.

###  4.2 Comprehension

The second most important axiom is comprehension, which is as usual and again
uses the strong bi-implication:111111We suppress mention of parameters to
simplify notation.

$\textbf{Comprehension:}\;\;\;\boldsymbol{\forall u\exists x\forall y\;(y\in
x\Leftrightarrow y\in u\land\varphi(y))}$

This axiom allows us to use traditional set-theoretic notation

$x=\\{y\in u:\varphi(y)\\}.$

As in Convention 3.2, this is an abbreviation for $y\in x\Leftrightarrow y\in
u\land\varphi(y)$, and the Comprehension axiom guarantees that if $u$ is a set
then $x$ is also a set.

###  4.3 Classical Supersets

The development of our theory is greatly simplified by considering an axiom
postulating that every set is contained within a classical superset. In
Section 3 we said that a set was classical if its $!$-extension and
$?$-extension are the same. We do not know yet whether !-extensions and
$?$-extensions are sets, but we can express that $C$ is a classical set with
the sentence $\forall y\;{\circ}(y\in C)$, where $\circ$ is the classicality
operator.

$\textbf{Classical Superset:}\;\;\;\boldsymbol{\forall x\>\exists
C\>(x\subseteq C\;\land\;\forall y\;{\circ}(y\in C))}$

Strictly speaking, this axiom is superfluous: it can be proved to follow from
the remaining axioms in a roundabout way. However, adopting it at this stage
allows us to frame the remaining axioms, and the theory in general, in a more
intuitive way. In particular, it allows us to confirm several properties of
sets we postulated in the previous section.

######  Lemma 4.1 (Cl. Superset + Comprehension).

If $x$ is a set, then its !-extension and ?-extension are sets.

###### Proof.

Let $C$ be a classical set with $x\subseteq C$. Then

$x^{!}\;=\;\\{y\in C\;:\;!(y\in x)\\}$ $x^{?}\;=\;\\{y\in C\;:\;?(y\in x)\\}$

are both sets by the Comprehension axiom. ∎

Since $x^{!}$ and $x^{?}$ are classical, a posteriori we see that a
particularly convenient classical superset of $x$ is obtained by considering
$x^{!}\cup x^{?}$. This is the smallest classical set containing $x$ and we
will sometimes call this the _realm_ of $x$:

$\mathrm{rlm}(x):=x^{!}\cup x^{?}.$

The next lemma elaborates on the meaning of equality and the subset relation
between sets; note that the bi-implications are native and not strong, so the
equivalence relates to truth values of the statements in question.

######  Lemma 4.2 (Cl. Superset + Extensionality + Comprehension).

  1. 1.

$x\subseteq y\;\;\leftrightarrow\;\;x^{!}\subseteq y^{!}\land x^{?}\subseteq
y^{?}$

  2. 2.

$x\not\subseteq y\;\;\leftrightarrow\;\;\exists z(z\in x\land z\notin
y)\;\;\leftrightarrow\;\;x^{!}\not\subseteq y^{?}$

  3. 3.

$?(x\subseteq y)\;\;\leftrightarrow\;\;x^{!}\subseteq y^{?}$

  4. 4.

$x=y\;\;\leftrightarrow\;\;x^{!}=y^{!}\land x^{?}=y^{?}$

  5. 5.

$x\neq y\;\;\leftrightarrow\;\;\exists z((z\in x\land z\notin y)\lor(z\in
y\land z\notin x))\;\;\leftrightarrow\;\;x^{!}\not\subseteq y^{?}\lor
y^{!}\not\subseteq x^{?}$

  6. 6.

$?(x=y)\;\;\leftrightarrow\;\;x^{!}\subseteq y^{?}\land y^{!}\subseteq x^{?}$

###### Proof.

We will provide detailed proofs of 1 and 2 in order to illustrate how
reasoning within $\mathrm{BS4}$ works. The remaining proofs are left to the
reader.

  1. 1.

We have the following sequence of $\mathrm{BS4}$-provable bi-implications:

$x\subseteq y$

$\Leftrightarrow$

$\forall z\;((z\in x\to z\in y)\;\land\;({\sim}(z\in y)\to{\sim}(z\in x))$

$\stackrel{{\scriptstyle(*)}}{{\leftrightarrow}}$

$\forall z\;((!(z\in x)\to!(z\in y))\;\land\;(?(z\in x)\to?(z\in y))$

$\stackrel{{\scriptstyle(**)}}{{\Leftrightarrow}}$

$\forall z\;((z\in x^{!}\Rightarrow z\in y^{!})\;\land\;(z\in x^{?}\Rightarrow
z\in y^{?})$

$\Leftrightarrow$

$x^{!}\subseteq y^{!}\land x^{?}\subseteq y^{?}$.

Here $(*)$ is due to the truth-functional definition of the implications and
the $!$ and $?$ operators, while $(**)$ is due to the definition of
$x^{!},y^{!},x^{?},y^{?}$ and the fact that these sets are classical (so $\to$
and $\Rightarrow$ are interchangeable). The first and last strong bi-
implication is the definition of $\subseteq$.

  2. 2.

We have the following sequence of bi-implications:

${\sim}(x\subseteq y)$

$\Leftrightarrow$

${\sim}\forall z(z\in x\Rightarrow z\in y)$

$\Leftrightarrow$

$\exists z{\sim}(z\in x\Rightarrow z\in y)$

$\stackrel{{\scriptstyle(*)}}{{\leftrightarrow}}$

$\exists z(z\in x\land z\notin y)$

where $(*)$ is because we are only looking at the truth condition of
$\Rightarrow$. Further:

$\dots$

$\stackrel{{\scriptstyle(**)}}{{\leftrightarrow}}$

$\exists z(z\in x^{!}\land z\notin y^{?})$

$\Leftrightarrow$

$x^{!}\not\subseteq y^{?}$.

where $(**)$ is again due to the fact that $!$ refers to truth and $?$ to
falsity. ∎

###  4.4 Replacement

The next axiom we consider is Replacement.121212As before, we suppress mention
of parameters to simplify notation. In $\mathrm{ZFC}$ the Replacement Axiom
tells us that the image of a set under a class function is itself a set. It is
not immediately clear how to generalize a class function. As a guiding
principle we rely on the intuition that in practice, mathematicians apply
Replacement when there is a pre-determined recipe by which each element of a
given set is replaced by another element in a non-ambiguous way. We will call
such a recipe an operation:

######  Definition 4.3.

An operation is a formula $\varphi(x,y)$ such that

  1. 1.

$\varphi$ is classical, and

  2. 2.

$\forall x\exists y(\varphi(x,y)\;\land\;\forall z\;(\varphi(x,z)\to!(y=z))$.

The reason we require $\varphi$ to be classical is because the operation that
maps $x$ to $y$ is supposed to occur in a well-defined way, and we are not
interested in distinguishing between $\varphi(x,y)$ being false and
$\varphi(x,y)$ being not true. Likewise, the reason we add the “$!$” is to
make sure that the statement expressing that every input has at most one
output is a classical sentence, since we would not know how to interpret a
situation in which the statement “every input has at most one output” is both
true and false.131313One can check that this will occur, for example, with the
formula $\varphi(x,y)\;\equiv\;!(y=a)$ where $a$ is any non-classical set.

$\textbf{Replacement:}\;\;\;\boldsymbol{({\circ}\varphi\land\forall x\exists
y(\varphi(x,y)\land\forall z(\varphi(x,z)\to!(y=z)))\to}$

$\boldsymbol{\forall x\exists y\forall z(z\in y\Leftrightarrow\exists w(w\in
x\land\varphi(w,z)))}$

After adopting this axiom, we can treat an operation $\varphi$ as a class
function $F$, and use notation such as

$F[X]:=\\{y:\exists x\;(x\in X\land\varphi(x,y)\\}$

where $X$ is a set.

###  4.5 Pairing

The Pairing Axiom is normally needed to get set-theory “started”, e.g., by
allowing the definition of ordered pairs, relations, functions, and so on.
Recall the discussion in Convention 3.3 in Section 3 and that we want notation
such as $\\{u,v\\}$ to stand for the classical set whose !-extension and
?-extension contain exactly the two objects $u$ and $v$. This motivates the
following

$\textbf{Pairing:}\;\;\;\boldsymbol{\forall u\forall v\exists x\forall y(y\in
x\>\Leftrightarrow\;(!(y=u)\lor!(y=v)))}$

As discussed in Section 3, this falls in line with the intuition of an
unordered pair $\\{u,v\\}$ as a classical set. Referring to Lemma 4.2. (5) and
(6), we now see that, if we had used the definition $\\{x:x=u\lor x=v\\}$ for
the unordered pair, then the ?-extension would have been the collection of all
$x$ such that $x^{!}\subseteq u^{?}$ and $u^{!}\subseteq x^{?}$, or
$x^{!}\subseteq v^{?}$ and $v^{!}\subseteq x^{?}$. This is problematic since
there is no upper bound on the size of $x^{?}$. Indeed, in Lemma 5.5 we will
prove that if there exists at least one incomplete set, then $\\{x:x=u\lor
x=v\\}$ is a proper class.

###  4.6 Power Set

Suppose $u$ is any set and we look at $\mathscr{P}(u):=\\{x:x\subseteq u\\}$.
Referring to Lemma 4.2, we again notice that $?(x\subseteq
u)\;\;\leftrightarrow\;\;x^{!}\subseteq u^{?}$, so the ?-extension of
$\mathscr{P}(u)$ consists of sets $x$ such that $x^{!}\subseteq u^{?}$, but
with no special requirement on $x^{?}$. Again, it should be intuitively clear
that there is a proper class of possible $x$ satisfying this requirement. As
with Pairing, we instead opt for the following definition:

$\mathscr{P}^{!}(u):=\\{x:\;!(x\subseteq u)\\}$

Now $\mathscr{P}^{!}(u)$ is a classical set containing exactly those sets $x$
for which $x^{!}\subseteq u^{!}$ and $x^{?}\subseteq u^{?}$. This motivates
the axiom:

$\textbf{Power Set:}\;\;\;\boldsymbol{\forall u\exists v\forall x(x\in
v\>\Leftrightarrow\;\;!(x\subseteq u))}$

###  4.7 The remaining axioms

We will now list the remaining four axioms since they are, mostly, non-
problematic.

$\textbf{Union:}\;\;\;\boldsymbol{\forall u\exists x\forall y(y\in
x\>\Leftrightarrow\;\exists z\>(y\in z\land z\in u)}$

After adopting this axiom we can use the abbreviation $\bigcup u:=\\{x:\exists
z\>(y\in z\land z\in u)\\}$, and this coincides with Convention 3.2.

$\textbf{Infinity:}\;\;\;\boldsymbol{\exists x\;(\varnothing\in
x\;\land\forall y(y\in x\to y\cup\\{y\\}\in x)}$

This axiom, among other things, allows us to define numbers, the ordinal
$\omega$, and other transfinite ordinals.

$\textbf{Foundation:}\;\;\;\boldsymbol{\forall x(\forall y(y\in x^{!}\cup
x^{?}\to\varphi(y))\to\varphi(x))\;\;\to\;\;\forall u\varphi(u)}$

This axiom could more properly be called “set induction schema”. It allows us
to view the universe as being constructed by transfinite recursion, where each
new level consists of those $x$ for which the realm $x^{!}\cup x^{?}$ is a
subset of the previous level. See [19, Section 4.12] for details.

$\textbf{Choice:}\;\;\;\boldsymbol{\forall u(\forall x(x\in u\to\exists y(y\in
u))\;\to}$ $\hskip 113.81102pt\boldsymbol{\;\exists f({\rm
dom}(f)=u\;\land\;\forall x(x\in u\to f(x)\in x)))}$

Notice that this is the standard formulation of the axiom of choice saying
that if every element of $u$ is non-empty, then there is a choice function $f$
for $u$. Technically, we have not defined functions as sets in our theory; in
fact, we have not even properly defined relations, Cartesian products or
ordered pairs. But this can be done in a standard way after settling a few
basic issues concerning ordered pairs. The interested reader may find the
details in [19, Sections 4.8, 4.9 and Appendix A].

###  4.8 Summary

We summarize the theory we have built up.

######  Definition 4.4.

The theory $\mathrm{PZFC}$ consist of the following $\mathrm{BS4}$-axioms:

  1. 1.

$\textbf{Extensionality: }\forall x\forall y(x=y\;\Leftrightarrow\;\forall
z(z\in x\Leftrightarrow z\in y))$.

  2. 2.

$\textbf{Comprehension: }\forall u\exists x\forall y\;(y\in x\Leftrightarrow
y\in u\land\varphi(y))$.

  3. 3.

$\textbf{Classical Superset: }\forall x\>\exists C\>(x\subseteq
C\;\land\;\forall y\;{\circ}(y\in C))$.

  4. 4.

$\textbf{Replacement: }({\circ}\varphi\land\forall x\exists
y(\varphi(x,y)\land\forall z(\varphi(x,z)\to!(y=z)))\to$

$\forall x\exists y\forall z(z\in y\Leftrightarrow\exists w(w\in
x\land\varphi(w,z))).$

  5. 5.

$\textbf{Pairing: }\forall u\forall v\exists x\forall y(y\in
x\>\Leftrightarrow\;(!(y=u)\lor!(y=v)))$.

  6. 6.

$\textbf{Power Set: }\forall u\exists v\forall x(x\in
v\>\Leftrightarrow\;\;!(x\subseteq u))$.

  7. 7.

$\textbf{Union: }\forall u\exists x\forall y(y\in x\>\Leftrightarrow\;\exists
z\>(y\in z\land z\in u)$.

  8. 8.

$\textbf{Infinity: }\exists x\;(\varnothing\in x\;\land\forall y(y\in x\to
y\cup\\{y\\}\in x)$.

  9. 9.

$\textbf{Foundation: }\forall x(\forall y(y\in x^{!}\cup
x^{?}\to\varphi(y))\to\varphi(x))\;\;\to\;\;\forall u\varphi(u)$.

  10. 10.

$\textbf{Choice: }\forall u(\forall x(x\in u\to\exists y(y\in
u))\;\to\;\exists f({\rm dom}(f)=u\;\land\;\forall x(x\in u\to f(x)\in x)))$.

Further, we make a note that the theory allows us to define, with relative
ease, the following concepts needed for the standard development of
mathematics: ordered pairs, relations, functions, natural numbers, ordinals,
the cumulative hierarchy of sets, and the concept of rank. Definitions by
recursion and proofs by induction are also non-problematic. We leave out the
detailed construction of these concepts and refer the reader to [19, Chapter 4
and Appendix A].

##  5 The anti-classicality axiom and $\mathrm{BZFC}$

None of the axioms of $\mathrm{PZFC}$ guarantee the existence of an
inconsistent or incomplete set. In fact, the following should be clear:

######  Theorem 5.1.

$\mathrm{PZFC}\>+\>\forall x(x^{!}=x^{?})$ is equivalent to $\mathrm{ZFC}$.

###### Proof.

If every set is classical, then there is no distinction between ${\sim}$ and
$\lnot$, nor between $\to$ and $\Rightarrow$. Likewise, $!$ and $?$ can be
discarded. The axiom Classical Superset is trivially true. So what remains of
$\mathrm{PZFC}$ is precisely the collection of $\mathrm{ZFC}$ axioms. ∎

Since we are interested in theories with non-classical sets, we would like to
adopt an axiom postulating their existence. Now we seem to be faced with a
choice: exactly which non-classical sets do we want to postulate the existence
of? Following a conservative approach, we might want to add an axiom that says
only that some inconsistent set exists, and some incomplete set exists:

$\exists x(x^{!}\not\subseteq x^{?})\;\land\;\exists x(x^{?}\not\subseteq
x^{!})$

On the other hand, a maximality approach might lead us to postulate the
existence of as many non-classical sets as possible. The boldest statement of
this kind would be to postulate that for any classical sets $u$, $v$, there
exists a set $x$ whose !-extension is exactly $u$ and whose ?-extension is
exactly $v$

$\forall u\forall v(u\text{ and }v\text{ classical }\;\to\;\exists
x\>(x^{!}=u\land x^{?}=v)).$

An unexpected, yet surprisingly simple result now shows that in the presence
of the other $\mathrm{PZFC}$-axioms, any choice we make is equivalent, since
the weakest of them (the conservative one) already implies the strongest (the
maximizing one).

######  Theorem 5.2 ($\mathrm{PZFC}$).

Suppose there is an inconsistent and an incomplete set. Then for any classical
sets $u,v$, there is $x$ such that $x^{!}=u$ and $x^{?}=v$.

###### Proof.

From the assumption we have $a\in b\land a\notin b$ for some sets $a,b$ and
also $\lnot(c\in d\lor c\notin d)$ for some sets $c,d$. Let us introduce the
following abbreviation:

$\phi_{\mathfrak{b}}\;\;\equiv\;\;a\in b$
$\phi_{\mathfrak{n}}\;\;\equiv\;\;c\in d$

Note that $\phi_{\mathfrak{b}}$ and ${\sim}\phi_{\mathfrak{b}}$ are both true,
while $\phi_{\mathfrak{n}}$ and ${\sim}\phi_{\mathfrak{n}}$ are both not true.

Let $u$ and $v$ be classical sets and define

$x:=\\{z\in u\cup v\;\;:\;\;z\in(u\cap v)\;\lor\;(z\in(u\setminus
v)\land\phi_{\mathfrak{b}})\;\lor\;(z\in(v\setminus
u)\land\phi_{\mathfrak{n}})\\}$

Then we have:

$z\in x$

$\leftrightarrow$

$z\in(u\cap v)\;\lor\;(z\in(u\setminus
v)\land\phi_{\mathfrak{b}})\;\lor\;(z\in(v\setminus
u)\land\phi_{\mathfrak{n}})$

$\leftrightarrow$

$z\in(u\cap v)\;\lor\;z\in(u\setminus v)$

$\leftrightarrow$

$z\in u.$

And:

$z\notin x$

$\leftrightarrow$

$z\notin(u\cap v)\;\land\;(z\notin(u\setminus
v)\lor{\sim}\phi_{\mathfrak{b}})\;\land\;(z\notin(v\setminus
u)\lor{\sim}\phi_{\mathfrak{n}})$

$\leftrightarrow$

$z\notin(u\cap v)\;\land\;z\notin(v\setminus u)$

$\leftrightarrow$

$z\notin v.$

It follows that $z\in x^{!}\leftrightarrow z\in u$ and $z\in
x^{?}\leftrightarrow z\in v$. This completes the proof. ∎

######  Definition 5.3.

We let the anti-classicality axiom be the statement:

$\textbf{ACLA:}\;\;\;\boldsymbol{\exists x(x^{!}\not\subseteq
x^{?})\;\land\;\exists x(x^{?}\not\subseteq x^{!})}$

and consider the system

$\mathrm{BZFC}\;\;\equiv\;\;\mathrm{PZFC}+\mathrm{ACLA}$

This is the main axiomatic system under consideration in this paper.

######  Remark 5.4.

Some readers might be interested in a finer distinction and consider a theory
that has only incomplete but not inconsistent sets. The corresponding theory
would then be $\mathrm{PZFC}+\exists x(x^{?}\not\subseteq x^{!})+\forall
x(x^{!}\subseteq x^{?})$. A proof similar to the above would then show that
this implies that for any classical sets $u,v$ with $u\subseteq v$, there is
$x$ such that $x^{!}=u$ and $x^{?}=v$. Likewise, if one is interested in a
theory that has only inconsistent but not incomplete sets one can look at
$\mathrm{PZFC}+\exists x(x^{!}\not\subseteq x^{?})+\forall x(x^{?}\subseteq
x^{!})$. This implies that for any classical sets $u,v$ with $v\subseteq u$,
there is $x$ such that $x^{!}=u$ and $x^{?}=v$. We will briefly return to this
finer distinction in Section 9, but will not pursue it further in detail.

As a nice application of $\mathrm{ACLA}$, we can internally define truth
values in a succinct way. Let $\Omega:=\mathscr{P}^{!}(\\{\varnothing\\})$.
This is the classical set containing sets $x$ such that
$x^{!}\subseteq\\{\varnothing\\}$ and $x^{?}\subseteq\\{\varnothing\\}$. There
are four possible combinations for such $x$, and $\mathrm{ACLA}$ guarantees us
that all four of them exist and are members of $\Omega$. We can give them
names as follows:

  * •

$x=1\;\;\;\;$ if $\;\;\;\;x^{!}=x^{?}=\\{\varnothing\\}$

  * •

$x=0\;\;\;\;$ if $\;\;\;\;x^{!}=x^{?}=\varnothing$

  * •

$x=\mathfrak{n}\;\;\;\;$ if $\;\;\;\;x^{!}=\varnothing$ and
$x^{?}=\\{\varnothing\\}$

  * •

$x=\mathfrak{b}\;\;\;\;$ if $\;\;\;\;x^{!}=\\{\varnothing\\}$ and
$x^{?}=\varnothing$

Then $\Omega=\\{1,\mathfrak{b},\mathfrak{n},0\\}$ is called the set of truth
values, and for any formula $\varphi$, we can define the truth value of
$\varphi$ by:

$\llbracket\varphi\rrbracket:=\\{\varnothing:\varphi\\}\in\Omega.$

We now have that $\varnothing\in\llbracket\varphi\rrbracket$ is true precisely
if $\varphi$ is true, and false precisely if $\varphi$ is false. In other
words, for any formula $\varphi$, from the point of view of the meta-theory:

$\llbracket\;\varnothing\in\llbracket\varphi\rrbracket\;\rrbracket\;=\;\llbracket\varphi\rrbracket.$

This justifies the term “truth value” of $\varphi$ and the fact that $\Omega$
is the set of truth values.

Finally, recall that when we formulated the Pairing and Power Set axioms, we
mentioned that a careless translation of the definition would result in a
proper class. We can now make this assertion precide.

######  Lemma 5.5 ($\mathrm{BZFC}$).

For sets $u,u_{1},\dots u_{n}$, the collections $\\{y:y\subseteq u\\}$,
$\\{y:y=u\\}$ and $\\{y:y=u_{1}\lor\dots\lor y=u_{n}\\}$ are proper classes.

###### Proof.

We will only prove the first case since the others are similar. We know that
$\\{x:\lnot(x\in x)\\}$ is a proper class, and from this it easily follows
that the collection ${\mathrm{Cl}}$ of all classical sets forms a proper
class.

Suppose there is a set $X=\\{y:y\subseteq u\\}$. By Lemma 4.1 we know that
$X^{?}$ is also a set. By Lemma 4.2 (3), we know that $y\in
X^{?}\Leftrightarrow y^{!}\subseteq u^{?}$. Consider the operation

$F:\begin{array}[]{rll}X^{?}&\to&{\mathrm{Cl}}\\\ y&\mapsto&y^{?}\end{array}$

Formally, this operation is given by $\varphi(y,w)\;\equiv\;!(w=y^{?})$ which
is a classical formula and satisfies the conditions for the Replacement axiom.
Moreover, by $\mathrm{ACLA}$ the operation is surjective, i.e., for every
classical $w$ there is $y\in X^{?}$ such that $\varphi(y,w)$ holds (take $y$
with $y^{!}=u^{?}$ and $y^{?}=w$). But then $F[X^{?}]={\mathrm{Cl}}$, and
since $X^{?}$ is a set, ${\mathrm{Cl}}$ should be a set, which is a
contradiction.∎

The above argument is somewhat informal, so some readers may have wondered
what it means to says that something is a proper class, or whether a proof by
contradiction is valid in the paraconsistent setting. Formally, what we have
proven is that if a set $X$ such as above exists, then, via the Russell set,
we derive $\bot$.

##  6 A model of $\mathrm{BZFC}$

In this section we construct a natural T/F-model for $\mathrm{BZFC}$ within
classical $\mathrm{ZFC}$. Normally speaking this would yield a relative
consistency proof, i.e., a proof that if $\mathrm{ZFC}$ is consistent then
$\mathrm{BZFC}$ is consistent. Of course $\mathrm{BZFC}$ is, by design,
inconsistent, so instead we will talk of non-triviality:

######  Definition 6.1.

A $\mathrm{BS4}$-theory $\Gamma$ is called non-trivial if
$\Gamma\not\vdash_{\mathrm{BS4}}\bot$.

Since $\mathrm{BZFC}$ implies a strong maximality principle with regards to
the existence of all possible sets, this suggests a natural model in which
sets are constructed recursively, adding all possible pairs of the form
(extension, ?-extension) made from previously constructed sets, at each step.

######  Definition 6.2 ($\mathrm{ZFC}$).

By induction on ordinals define:

  * •

$W_{0}=\varnothing$

  * •

$W_{\alpha+1}:=\mathscr{P}(W_{\alpha})\times\mathscr{P}(W_{\alpha})$

  * •

$W_{\lambda}=\bigcup_{\alpha<\lambda}W_{\alpha}$ for limit $\lambda$

  * •

$\displaystyle{\mathbb{W}}:=\bigcup_{\alpha\in\textup{Ord}}W_{\alpha}.$

Define the positive and negative interpretations of $\in$ and $=$ by:

  * •

$(a,b)\in^{+}(c,d)$ iff $(a,b)\in c$

  * •

$(a,b)\in^{-}(c,d)$ iff $(a,b)\notin d$

  * •

$(a,b)=^{+}(c,d)$ iff $(a,b)=(c,d)$

  * •

$(a,b)=^{-}(c,d)$ iff $\exists z\in a\setminus d$ or $\exists z\in c\setminus
b$.

The following properties of ${\mathbb{W}}$ parallel the $V$-hierarchy and
follow immediately from the definition.

######  Lemma 6.3 ($\mathrm{ZFC}$).

  1. 1.

If $\alpha<\beta$ then $W_{\alpha}\subseteq W_{\beta}$.

  2. 2.

If $(a,b)\in W_{\alpha}$, $a^{\prime}\subseteq a,$ and $b^{\prime}\subseteq b$
then $(a^{\prime},b^{\prime})\in W_{\alpha}$.

  3. 3.

$x\in{\mathbb{W}}$ iff $x=(a,b)$ for some $a,b\subseteq{\mathbb{W}}$.

###### Proof.

Induction on the definition. ∎

Now $({\mathbb{W}},\in^{+},\in^{-},=^{+},=^{-})$ may be considered a T/F-model
in the language of set theory according to Definition 2.3, except that
${\mathbb{W}}$ is a proper class. Therefore, “${\mathbb{W}}\models\varphi$”
must be understood via relativization: for every $\varphi$ we define
$\varphi^{{\mathbb{W}},T}$ and $\varphi^{{\mathbb{W}},F}$ by syntactic
induction, generalizing from Definition 2.3 in the obvious way. For example

$(x=y)^{{\mathbb{W}},T}\;\;\;\;\;\;\equiv\;\;\;\;\;x=y$
$(x=y)^{{\mathbb{W}},F}\;\;\;\;\;\;\equiv\;\;\;\;\;x=^{-}y$ $\dots$ $(\exists
x\varphi)^{{\mathbb{W}},T}\;\;\;\;\;\;\equiv\;\;\;\;\;\exists
x\left(x\in{\mathbb{W}}\land\varphi^{{\mathbb{W}},T}\right)$ $(\exists
x\varphi)^{{\mathbb{W}},F}\;\;\;\;\;\;\equiv\;\;\;\;\;\forall
x\left(x\in{\mathbb{W}}\to\varphi^{{\mathbb{W}},F}\right)$

and so on. We leave the details to the reader. By ${\mathbb{W}}\models\varphi$
we will always mean $\varphi^{{\mathbb{W}},T}$, and for a theory $\Gamma$,
${\mathbb{W}}\models\Gamma$ means that for every $\varphi$ in $\Gamma$, there
is a proof of $\varphi^{{\mathbb{W}},T}$.

######  Theorem 6.4 ($\mathrm{ZFC}$).

${\mathbb{W}}\models\mathrm{BZFC}$.

###### Proof.

We will prove Extensionality and Comprehension in some detail and leave the
rest to the reader.

Written out in full, the relativization (Extensionality)W,T reads as follows

$\forall(a,b)\in{\mathbb{W}}\;\forall(c,d)\in{\mathbb{W}}:$
$(a,b)=^{+}(c,d)\;\;\;\;\leftrightarrow\;\;\;\;\forall
z\in{\mathbb{W}}((z\in^{+}(a,b)\leftrightarrow
z\in^{+}(c,d))\land(z\in^{-}(a,b)\leftrightarrow z\in^{-}(c,d))$ $\land$
$(a,b)=^{-}(c,d)\;\;\;\;\leftrightarrow\;\;\;\;\exists
z\in{\mathbb{W}}((z\in^{+}(a,b)\land z\in^{-}(c,d))\lor(z\in^{+}(c,d)\land
z\in^{-}(a,b))$

Assume $(a,b)$ and $(c,d)$ are arbitrary, and we show that the two
equivalences hold. For the first we have

$\forall z\in{\mathbb{W}}((z\in^{+}(a,b)\leftrightarrow
z\in^{+}(c,d))\land(z\in^{-}(a,b)\leftrightarrow z\in^{-}(c,d))$

$\stackrel{{\scriptstyle(*)}}{{\leftrightarrow}}$

$\forall z\in{\mathbb{W}}((z\in a\leftrightarrow z\in c)\land(z\notin
b\leftrightarrow z\notin d)).$

$\stackrel{{\scriptstyle(**)}}{{\leftrightarrow}}$

$\forall z((z\in a\leftrightarrow z\in c)\land(z\notin b\leftrightarrow
z\notin d))$

$\leftrightarrow$

$a=c$ and $b=d$

$\leftrightarrow$

$(a,b)=^{+}(c,d)$

where $(*)$ refers to the definition of $\in^{+}$ and $\in^{-}$, and $(**)$ is
because ${\mathbb{W}}$ is “transitive” in the sense that
$a,b,c,d\in{\mathbb{W}}$ only contain sets which are also in ${\mathbb{W}}$,

For the second equivalence we have

$\exists z\in{\mathbb{W}}((z\in^{+}(a,b)\land
z\in^{-}(c,d))\lor(z\in^{+}(c,d)\land z\in^{-}(a,b))$

$\leftrightarrow$

$\exists z((z\in a\land z\notin d)\lor(z\in c\land z\notin b))$

$\leftrightarrow$

$(a,b)=^{-}(c,d)$

Next we look at (Comprehension)W,T which is the following
statement:141414Again we suppress parameters, noting that if there are
parameters these are understood to be in ${\mathbb{W}}$.

$\forall(a,b)\in{\mathbb{W}}\;\exists(c,d)\in{\mathbb{W}}\;\forall
z\in{\mathbb{W}}\>$
$((z\in^{+}(c,d)\leftrightarrow(z\in^{+}(a,b)\land\varphi(z)^{{\mathbb{W}},T})\land(z\in^{-}(c,d)\leftrightarrow(z\in^{-}(a,b)\lor\varphi(z)^{{\mathbb{W}},F}))$

Suppose $(a,b)\in{\mathbb{W}}$ and $\varphi$ is given. Define

$c:=\\{z\in a:\varphi(z)^{{\mathbb{W}},T}\\}$ $d:=\\{z\in
b:\lnot\varphi(z)^{{\mathbb{W}},F}\\}$

Then $(c,d)\in{\mathbb{W}}$ by construction and for all $z$ we have $z\in
c\leftrightarrow(z\in a\land\varphi(z)^{{\mathbb{W}},T})$ and $z\notin
d\leftrightarrow(z\notin b\lor\varphi(z)^{{\mathbb{W}},F})$. This is exactly
the statement above as needs to be proved. ∎

######  Corollary 6.5.

If $\mathrm{ZFC}$ is consistent then $\mathrm{BZFC}$ is non-trivial.

######  Definition 6.6 ($\mathrm{ZFC}$).

For every $x\in V$, inductively define

$\check{x}:=(\\{\check{y}:y\in x\\},\;\\{\check{y}:y\in x\\}).$

Also let $\check{V}:=\\{\check{x}:x\in V\\}$.

######  Lemma 6.7 ($\mathrm{ZFC}$).

The mapping

$i:\begin{array}[]{ccl}V&\rightarrow&\check{V}\subseteq{\mathbb{W}}\\\
x&\mapsto&\check{x}\end{array}$

is an isomorphism between $(V,\in,\notin,=,\neq)$ and
$(\check{V},\in^{+},\in^{-},=^{+},=^{-})$.

###### Proof.

Easy consequence of the definitions. ∎

In view of the above, ${\mathbb{W}}$ can be viewed as a natural extension of
$V$, enriching the classical von Neumann universe with paraconsistent and
paracomplete sets.

##  7 Hereditarily classical sets.

Starting in $\mathrm{BZFC}$, we can also construct a natural model of
$\mathrm{ZFC}$: this is the class of “hereditarily classical” sets.

######  Definition 7.1 ($\mathrm{BZFC}$).

By induction on ordinals define:161616By the remark in Section 4.8, ordinals
and transfinite recursion can be carried out in $\mathrm{BZFC}$ in a manner
analogous to $\mathrm{ZFC}$.

  * •

${\textup{HCL}}_{0}=\varnothing$

  * •

${\textup{HCL}}_{\alpha+1}:=\\{X\subseteq{\textup{HCL}}_{\alpha}:X$ is
classical$\\}$

  * •

${\textup{HCL}}_{\lambda}=\bigcup_{\alpha<\lambda}{\textup{HCL}}_{\alpha}$ for
limit $\lambda$

  * •

$\displaystyle{\mathbb{HCL}}:=\bigcup_{\alpha\in\textup{Ord}}{\textup{HCL}}_{\alpha}.$

${\mathbb{HCL}}$ is a transitive proper class, and for all $x$, we have that
$x\in{\mathbb{HCL}}$ if and only if $x$ is classical and
$x\subseteq{\mathbb{HCL}}$. If $\varphi$ is a formula in the language of set
theory, then $\varphi^{\mathbb{HCL}}$ refers to the standard relativization
where quantification is replaced by quantification over ${\mathbb{HCL}}$. As
usual, ${\mathbb{HCL}}\models\Gamma$ means that for every $\varphi$ in
$\Gamma$, there is a proof of $\varphi^{\mathbb{HCL}}$.

######  Theorem 7.2 ($\mathrm{BZFC}$).

${\mathbb{HCL}}\models\mathrm{ZFC}$.

###### Proof.

It is clear that ${\mathbb{HCL}}\models$ every set is classical; so, by the
discussion in Section 5 it suffices to show that
${\mathbb{HCL}}\models\mathrm{PZFC}$. Most of the axioms are straightforward
since none of them postulate the existence of non-classical sets without
assuming the existence of non-classical sets.

We will only show (Comprehension)HCL. Suppose $u$ is a herditarily classical
set and $\varphi$ any formula. It is enough to show that $x:=\\{y\in
u:\varphi^{{\mathbb{HCL}}}(y,a_{1},\dots,a_{n})\\}$ is a hereditarily
classical set if the parameters $a_{1},\dots,a_{n}$ are hereditarily
classical.171717Here we are explicit about parameters $a_{1},\dots,a_{n}$
since otherwise $\varphi$ might fail to be a classical formula. Since
$x\subseteq u$ and $u\subseteq{\mathbb{HCL}}$ we know that
$x\subseteq{\mathbb{HCL}}$, so it remains to show that $x$ itself is
classical. But from the fact that $y,a_{1},\dots a_{n}$ are classical sets, it
follows by an easy induction that $\varphi$ is a classical formula, i.e.,
$!\varphi\leftrightarrow?\varphi$. It follows that $x^{!}=x^{?}$, so $x$ is
classical. ∎

######  Corollary 7.3.

If $\mathrm{BZFC}$ is non-trivial, then $\mathrm{ZFC}$ is consistent.

In analogy to Definition 6.6, we can now consider an embedding from the
universe of $\mathrm{BZFC}$ (which we also refer to as $V$, hopefully not
leading to confusion) to a natural copy of it within ${\mathbb{HCL}}$.

######  Definition 7.4 ($\mathrm{BZFC}$).

For every set $x$, inductively define:181818We have not formally defined the
ordered pair in $\mathrm{BZFC}$. Interested readers may consult [19, Appendix
A]. However, in this case, $\\{\hat{y}:y\in x^{!}\\}$ and $\\{\hat{y}:y\in
x^{?}\\}$ are classical sets, so we can also consider the ordered pair via the
standard $\mathrm{ZFC}$-definition.

$\hat{x}:=(\\{\hat{y}:y\in x^{!}\\},\\{\hat{y}:y\in x^{?}\\}).$

Also let $\hat{V}:=\\{\hat{x}:x\in V\\}$. For $\hat{x},\hat{y}\in\hat{V}$
define

  * •

$\hat{x}E^{+}\hat{y}$ $\leftrightarrow$ $x\in y$

  * •

$\hat{x}E^{-}\hat{y}$ $\leftrightarrow$ $x\notin y$

  * •

$\hat{x}\approx^{+}\hat{y}$ $\leftrightarrow$ $x=y$

  * •

$\hat{x}\approx^{-}\hat{y}$ $\leftrightarrow$ $x\neq y$

Now $\hat{x}$ are hereditarily classical sets, $\hat{V}$ is a proper class of
hereditarily classical sets, and $E^{+},E^{-},\approx^{+},\approx^{-}$ are
hereditarily classical, class-sized binary relations on $\hat{V}$.

######  Lemma 7.5 ($\mathrm{BZFC}$).

The mapping

$j:\begin{array}[]{ccl}V&\rightarrow&\hat{V}\subseteq{\mathbb{HCL}}\\\
x&\mapsto&\hat{x}\end{array}$

is an isomorphism between $(V,\in,\notin,=,\neq)$ and
$(\hat{V},E^{+},E^{-},\approx^{+},\approx^{-})$.

###### Proof.

Follows immediately from the definitions. ∎

##  8 Bi-interpretability

We can go further and look at the precise interaction between $\mathrm{ZFC}$
and $\mathrm{BZFC}$. Not only are the two theories bi-interpretable, but the
corresponding model constructions allow us to naturally translate between
$\mathrm{ZFC}$ and $\mathrm{BZFC}$-theorems.

Recall that in Lemma 6.7 we defined an isomorphism between $V$ and $\check{V}$
via $i:x\mapsto\check{x}$. The next result shows that $\check{V}$ is the same
thing as what ${\mathbb{W}}$ believes ${\mathbb{HCL}}$ to be. The notation
${\mathbb{HCL}}^{\mathbb{W}}$ refers to the class ${\mathbb{HCL}}$ relativized
to ${\mathbb{W}}$, defined in $\mathrm{ZFC}$.

######  Lemma 8.1 ($\mathrm{ZFC}$).

${\mathbb{HCL}}^{\mathbb{W}}=\check{V}$.

###### Proof.

To show $\supseteq$ take $\check{x}\in\check{V}$. By construction
$\check{x}=(\\{\check{y}:y\in x\\},\\{\check{y}:y\in x\\})$. Inductively, we
may assume that each $\check{y}$ appearing above is in
${\mathbb{HCL}}^{\mathbb{W}}$, therefore
${\mathbb{W}}\models\check{x}\subseteq{\mathbb{HCL}}$. Moreover, $\check{x}$
has the same !-extension as ?-extension, therefore
${\mathbb{W}}\models(\check{x}$ is classical). Together, this implies
${\mathbb{W}}\models\check{x}\in{\mathbb{HCL}}$.

To show $\subseteq$, suppose $x\in{\mathbb{HCL}}^{\mathbb{W}}$, i.e.,
$x\in{\mathbb{W}}$ and ${\mathbb{W}}\models(x$ is hereditarily classical). Let
$a,b\in{\mathbb{W}}$ be such that $x=(a,b)$. Since ${\mathbb{W}}\models x$ is
classical, in particular ${\mathbb{W}}\models x^{!}=x^{?}$, therefore $a=b$.
Moreover, ${\mathbb{W}}\models x\subseteq{\mathbb{HCL}}$ which implies that
$a\subseteq{\mathbb{HCL}}^{\mathbb{W}}$. Inductively, we may assume that every
element in $a$ is of the form $\check{z}$ for some $z\in V$. Let
$\tilde{a}:=\\{z:\check{z}\in a\\}$. Then
$x=(\\{\check{z}:z\in\tilde{a}\\},\\{\check{z}:z\in\tilde{a}\\})=(a,a)$ by
construction. But then, by definition, $x=({\tilde{a}}\check{)}$. ∎

######  Corollary 8.2.

$\mathrm{ZFC}\vdash\varphi\;\;$ iff
$\;\;\mathrm{BZFC}\vdash\left({\mathbb{HCL}}\models\varphi\right)$.

###### Proof.

Suppose $\mathrm{ZFC}\vdash\varphi$. Since
$\mathrm{BZFC}\vdash\left({\mathbb{HCL}}\models\mathrm{ZFC}\right)$, clearly
$\mathrm{BZFC}\vdash\left({\mathbb{HCL}}\models\varphi\right)$. Conversely,
suppose $\mathrm{BZFC}\vdash\left({\mathbb{HCL}}\models\varphi\right)$. By
Theorem 6.4,
$\mathrm{ZFC}\vdash\left({\mathbb{W}}\models\mathrm{BZFC}\right)$, so
$\mathrm{ZFC}\vdash\left({\mathbb{W}}\models\left({\mathbb{HCL}}\models\varphi\right)\right)$,
so $\mathrm{ZFC}\vdash({\mathbb{HCL}}^{\mathbb{W}}\models\varphi)$. But
${\mathbb{HCL}}^{\mathbb{W}}$ is $\check{V}$, which is isomorphic to $V$ by
Lemma 6.7. Therefore $\mathrm{ZFC}\vdash\varphi$. ∎

Conversely, if we start in $\mathrm{BZFC}$, look at the model
${\mathbb{HCL}}$, and apply Definition 6.2 to obtain ${\mathbb{W}}$
relativized to ${\mathbb{HCL}}$, we obtain the natural copy of the
$\mathrm{BZFC}$-universe $V$ under the embedding $\hat{x}$, as defined in
Definition 7.4.

######  Lemma 8.3 ($\mathrm{BZFC}$).

${\mathbb{W}}^{\mathbb{HCL}}=\hat{V}$.

###### Proof.

Suppose $\hat{x}\in\hat{V}$. Then $\hat{x}=(\\{\hat{y}:y\in
x^{!}\\},\\{\hat{y}:y\in x^{?}\\})$, and since every $\hat{y}$ appearing here
is in $\hat{V}$, inductively we can assume that it is also in
${\mathbb{W}}^{\mathbb{HCL}}$. By definition $\hat{x}$ is hereditarily
classical, and since the ordered pair is classical, we have
${\mathbb{HCL}}\models(\hat{x}=(a,b)$ and $a,b\subseteq{\mathbb{W}})$. By
Lemma 6.3 (3) applied in ${\mathbb{HCL}}$, this means
${\mathbb{HCL}}\models\hat{x}\in{\mathbb{W}}$.

Conversely, suppose $w\in{\mathbb{W}}^{\mathbb{HCL}}$. Again by Lemma 6.3 (3)
we know that ${\mathbb{HCL}}\models(w=(u,v)$ and $u,v\subseteq{\mathbb{W}})$.
Then $u,v\subseteq{\mathbb{W}}^{\mathbb{HCL}}$ so, inductively, we have
$u,v\subseteq\hat{V}$. Therefore, let $\tilde{u}=\\{y:\hat{y}\in u\\}$ and
$\tilde{v}=\\{y:\hat{y}\in v\\}$. Then $\tilde{u}$ and $\tilde{v}$ are
classical sets (because $u,v$ are), so by $\mathrm{ACLA}$ there exists a set
$x$ such that $x^{!}=\tilde{u}$ and $x^{?}=\tilde{v}$. Then we have

$\hat{x}\;=\;(\\{\hat{y}:y\in x^{!}\\},\\{\hat{y}:y\in
x^{?}\\})\;=\;(\\{\hat{y}:y\in\tilde{u}\\},\\{\hat{y}:y\in\tilde{v}\\})\;=\;(u,v)\;=\;w$

This shows that $w\in\hat{V}$. ∎

######  Corollary 8.4.

$\mathrm{BZFC}\vdash\varphi\;\;$ iff
$\;\;\mathrm{ZFC}\vdash\left({\mathbb{W}}\models\varphi\right)$.

###### Proof.

Suppose $\mathrm{BZFC}\vdash\varphi$. Since
$\mathrm{ZFC}\vdash\left({\mathbb{W}}\models\mathrm{BZFC}\right)$, clearly
$\mathrm{ZFC}\vdash\left({\mathbb{W}}\models\varphi\right)$. Conversely,
suppose $\mathrm{ZFC}\vdash\left({\mathbb{W}}\models\varphi\right)$. By
Theorem 7.2,
$\mathrm{BZFC}\vdash\left({\mathbb{HCL}}\models\mathrm{ZFC}\right)$, so
$\mathrm{BZFC}\vdash\left({\mathbb{HCL}}\models\left({\mathbb{W}}\models\varphi\right)\right)$,
so
$\mathrm{BZFC}\vdash\left({\mathbb{W}}^{\mathbb{HCL}}\models\varphi\right)$.
But ${\mathbb{W}}^{\mathbb{HCL}}$ is isomorphic to $V$, so
$\mathrm{BZFC}\vdash\varphi$. ∎

The philosophical significance of these results is that classical
$\mathrm{ZFC}$ and our theory $\mathrm{BZFC}$ are not at odds with each other,
but can be viewed as complementing each other in a natural way. If our
philosophical position favours the existence of paracomplete and
paraconsistent sets, we can view $\mathrm{BZFC}$ as describing a universe that
is an enlargement of the class ${\mathbb{HCL}}$ of hereditarily classical
sets. $\mathrm{ZFC}$ can then be viewed as the theory of ${\mathbb{HCL}}$, and
all of classical mathematics as taking place within ${\mathbb{HCL}}$. If we
are only interested in classical mathematics, we can stay within
${\mathbb{HCL}}$, but whenever we encounters a phenomenon that is better
described by paracomplete or paraconsistent sets, we can switch to
$\mathrm{BZFC}$ and take full advantage of the anti-classicality axiom.

On the other hand, if we are determined to preserve a classical meta-theory,
then we can view $\mathrm{BZFC}$ as the theory of the T/F-model ${\mathbb{W}}$
and all of paraconsistent and paracomplete set theory, as layed out in this
paper, as formal statements in ${\mathbb{W}}$. All of these statements are
ultimately provable in $\mathrm{ZFC}$.

##  9 Tarski semantics in $\mathrm{BZFC}$

A discussion that frequently arises in the philosophy of logic is the extent
to which the meta-theory affects the formal theory under consideration. For
example, one may argue that excluded middle is a tautology in classical logic
only because excluded middle is covertly assumed in the meta-theory:

$\mathcal{M}\models\varphi\lor\lnot\varphi\;\;\;\;\Leftrightarrow\;\;\;\;\mathcal{M}\models\varphi\text{
or }\mathcal{M}\not\models\varphi$

Likewise, in classical logic $\varphi\land\lnot\varphi$ can never be satisfied
by a model, because $\mathcal{M}\models\varphi\land\lnot\varphi$ would lead to
$\mathcal{M}\models\varphi$ and $\mathcal{M}\not\models\varphi$, which is
false in the meta-theory.

Non-classical logics are usually set up by considering other (non-Tarski)
semantics, so that the formal system in question may exhibit various levels of
non-classicality while the meta-theory remains classical. This is the case,
for example, with Kripke semantics for intuitionistic logic, and with our own
T/F-models for $\mathrm{BS4}$ from Section 2.

But we could approach the question differently: what is the logic generated by
considering standard Tarski semantics, but set up within a non-classical meta-
theory? The purpose of this section is to show that, indeed, Tarski semantics
in $\mathrm{BZFC}$ give rise to the logic $\mathrm{BS4}$, i.e.,
$\mathrm{BZFC}$ proves that $\mathrm{BS4}$ is sound and complete with respect
to _classical_ Tarski semantics. This result makes concrete use of the anti-
classicality axiom; in fact, we shall see that the logic generated by Tarski
semantics precisely reflects the level of non-classicality in the meta-theory.

In this section, we work in $\mathrm{BZFC}$ or $\mathrm{PZFC}$. For clarity,
we will refer to models defined below as Tarski models and the semantics as
Tarski semantics, to keep them apart from T/F-models and T/F-semantics. We
will also be explicit with using the notation $\models$ to refer to the Tarski
satisfaction relation, and $\models^{T}$ and $\models^{F}$ to refer to the
T/F-satisfaction relations.

######  Definition 9.1 ($\mathrm{PZFC}$).

The language of first order logic is assumed to be coded by classical sets. A
Tarski model $\mathcal{M}$ consists of a classical set $M$ as a domain, and
(not necessarily classical) interpretations for all constant and relation
symbols. For simplicity, assume there are no function symbols. Inductively
define:

  1. 1.

$\mathcal{M}\models(t=s)[a,b]\;\;\;\Leftrightarrow\;\;\;a=b$.

  2. 2.

$\mathcal{M}\models
R(t_{1},\dots,t_{n})[a_{1},\dots,a_{n}]\;\;\;\Leftrightarrow\;\;\;R^{\mathcal{M}}(a_{1},\dots
a_{n})$.

  3. 3.

$\mathcal{M}\models{\sim}\varphi\;\;\;\Leftrightarrow\;\;\;\mathcal{M}\not\models\varphi$.191919Here
$\mathcal{M}\not\models\varphi$ is an abbreviation for
${\sim}(\mathcal{M}\models\varphi)$.

  4. 4.

$\mathcal{M}\models\varphi\land\psi\;\;\;\Leftrightarrow\;\;\;\mathcal{M}\models\varphi$
and $\mathcal{M}\models\psi$.

  5. 5.

$\mathcal{M}\models\varphi\lor\psi\;\;\;\Leftrightarrow\;\;\;\mathcal{M}\models\varphi$
or $\mathcal{M}\models\psi$.

  6. 6.

$\mathcal{M}\models\varphi\to\psi\;\;\;\Leftrightarrow\;\;\;$
$(\mathcal{M}\models\varphi\;\;\to\;\;\mathcal{M}\models\psi)$.

  7. 7.

$\mathcal{M}\models\varphi\leftrightarrow\psi\;\;\;\Leftrightarrow\;\;\;$
($\mathcal{M}\models\varphi\;\;\leftrightarrow\;\;\mathcal{M}\models\psi)$.

  8. 8.

$\mathcal{M}\models\exists
x\varphi(x)\;\;\;\Leftrightarrow\;\;\;\mathcal{M}\models\varphi[a]$ for some
$a\in M$.

  9. 9.

$\mathcal{M}\models\forall
x\varphi(x)\;\;\;\Leftrightarrow\;\;\;\mathcal{M}\models\varphi[a]$ for all
$a\in M$.

  10. 10.

$\mathcal{M}\models\bot\;\;\;\Leftrightarrow\;\;\;\bot$.

This definition should be understood in the framework of $\mathrm{PZFC}$, with
all equivalences as strong implications. Note that while $M$ is a classical
set, the relation-interpretations $R^{\mathcal{M}}$ are not necessarily
classical. For example, it could happen that $R^{\mathcal{M}}(a)$ is both true
and false, in which case we have $\mathcal{M}\models R(x)[a]$ and
$\mathcal{M}\not\models R(x)[a]$, and subsequently
$\mathcal{M}\models(R(x)\land{\sim}R(x))[a]$.

######  Remark 9.2.

The reader may easily verify that the defined connectives are also translated
the way we would expect, namely:

$\mathcal{M}\models\lnot\varphi\;\;\;\Leftrightarrow\;\;\;\lnot(\mathcal{M}\models\varphi)$
$\mathcal{M}\models\;!\varphi\;\;\;\Leftrightarrow\;\;\;\;!(\mathcal{M}\models\varphi)$
$\mathcal{M}\models\;?\varphi\;\;\;\Leftrightarrow\;\;\;\;?(\mathcal{M}\models\varphi).$

Had we, for example, chosen $\lnot$ as the primitive connective in
$\mathrm{BS4}$ instead of $\bot$, then Definition 9.1 would have given rise to
the same logic.

Linguistically, it is useful to distinguish truth in a Tarski model from
satisfaction by a Tarski model. We say “$\mathcal{M}$ satisfies $\varphi$” to
express “$\mathcal{M}\models\varphi$” and “$\varphi$ is true in $M$” to
express $!(\mathcal{M}\models\varphi)$ (which is the same as
“$\mathcal{M}\models\;!\varphi$”). Satisfaction captures the entire truth
value of $\varphi$ in $\mathcal{M}$, and we can use the notation concerning
truth values from Section 5 to define the truth value of $\varphi$ in a Tarski
model $\mathcal{M}$:

$\llbracket\varphi\rrbracket_{\mathcal{M}}:=\\{\varnothing:\mathcal{M}\models\varphi\\}$

######  Definition 9.3 (PZFC).

For a set of formulas $\Sigma$ and a formula $\varphi$, the Tarski semantic
consequence relation is defined by $\Sigma\models\varphi$ if for all Tarski
models $\mathcal{M}$,

$\mathcal{M}\models\Sigma\;\to\;\mathcal{M}\models\varphi.$

######  Theorem 9.4 ($\mathrm{BZFC}$).

$\mathrm{BS4}$ is sound and complete with respect to Tarski semantics:

$\Sigma\models\varphi\;\;\leftrightarrow\;\;\Sigma\vdash_{\mathrm{BS4}}\varphi.$

######  Remark 9.5.

We should note here that the bi-implication is not a strong one, i.e.,
soundness and completeness only talks about truth in a model, not satisfaction
by the model. Indeed, note that $\vdash_{\mathrm{BS4}}$ is a classical
relation, while the Tarski-consequence relation $\models$ is not. For example,
take any $\varphi$ such that some model
$\mathcal{N}\models\varphi\land{\sim}\varphi$, and consider the classical
excluded middle $\varphi\lor\lnot\varphi$. Then for every $\mathcal{M}$ we
have $\mathcal{M}\models\varphi\lor\lnot\varphi$, but one can verify that
$\mathcal{N}\not\models\varphi\lor\lnot\varphi$. This means that
“$\varphi\lor\lnot\varphi$” both is and is not a tautology according to Tarski
semantics.

We will now prove Theorem 9.4. We could proceed by repeating the standard
soundness and completeness proof within $\mathrm{BZFC}$, but here we will take
a short-cut by recalling the fact that $\mathrm{BS4}$ is sound and complete
with respect to T/F-semantics (Lemma 2.7), and showing how T/F-models can be
“simulated” by Tarski models and vice versa, which seems to be an interesting
phenomenon in its own right.

First we adapt Definition 2.3 to $\mathrm{PZFC}$:

######  Definition 9.6 ($\mathrm{PZFC}$).

A T/F-model is defined as in Definition 2.3, with the added condition that the
domain $M$, all interpretations $(R^{\mathcal{M}})^{+}$ and
$(R^{\mathcal{M}})^{-}$ are classical subsets of $M^{n}$, and $=^{+}$ and
$=^{-}$ are classical subsets of $M\times M$. Moreover, it is required that
for $a,b\in M$ we have $a=^{+}b\;\leftrightarrow\;\;!(a=b).$202020In other
words, $=^{+}$ is a classical relation such that $a=^{+}b$ is true precisely
when $a=b$ is true, and false precisely when $a=b$ is not true. On the other
hand $=^{-}$ is a classical and symmetric binary relation, but need not have
anything to do with the meta-theoretic $a\neq b$.

######  Lemma 9.7 ($\mathrm{PZFC}$).

$\mathrm{BS4}$ is sound and complete with respect to T/F-semantics.

###### Proof.

Since all relevant sets and relations are classical, the original proof of
Lemma 2.7 can be repeated inside $\mathrm{PZFC}$, yielding the desired result.
We leave out the details here. ∎

The above Lemma essentially restates what we already knew about $\mathrm{BS4}$
when we considered it inside a classical meta-theory. Now the trick is
“simulate” T/F-models by Tarski models and vice versa.

######  Lemma 9.8 ($\mathrm{PZFC}$).

For every Tarski model $\mathcal{M}$, there exists a T/F-model
$\mathcal{M}^{\pm}$ such that for every $\varphi$:

$\mathcal{M}\models\varphi\;\;\leftrightarrow\;\;\mathcal{M}^{\pm}\models^{T}\varphi$
$\mathcal{M}\not\models\varphi\;\;\leftrightarrow\;\;\mathcal{M}^{\pm}\models^{F}\varphi$

###### Proof.

Let $\mathcal{M}^{\pm}$ have the same domain as $\mathcal{M}$. For every
relation symbol $R$ define classical relations $(R^{\mathcal{M}^{\pm}})^{+}$
and $(R^{\mathcal{M}^{\pm}})^{-}$ (including equality)

$(R^{\mathcal{M}^{\pm}})^{+}:=\\{(a_{1},\dots a_{n})\in
M^{n}\;:\;!R(a_{1},\dots,a_{n})\\}$
$(R^{\mathcal{M}^{\pm}})^{-}:=\\{(a_{1},\dots a_{n})\in
M^{n}\;:\;\lnot?R(a_{1},\dots,a_{n})\\}$

This definition makes sure that we have

$\mathcal{M}\models R[a_{1}\dots
a_{n}]\;\;\leftrightarrow\;\;\mathcal{M}^{\pm}\models^{T}R[a_{1}\dots a_{n}]$
$\mathcal{M}\not\models R[a_{1}\dots
a_{n}]\;\;\leftrightarrow\;\;\mathcal{M}^{\pm}\models^{F}R[a_{1}\dots a_{n}]$

An induction on the complexity of $\varphi$ then shows that the two
equivalences hold for all sentences. To exhibit an example:

$\mathcal{M}\models{\sim}\varphi\;\Leftrightarrow\;\mathcal{M}\not\models\varphi\;\stackrel{{\scriptstyle\rm
IH}}{{\leftrightarrow}}\;\mathcal{M}^{\pm}\models^{F}\varphi\;\leftrightarrow\;\mathcal{M}^{\pm}\models^{T}{\sim}\varphi$
$\mathcal{M}\not\models{\sim}\varphi\;\Leftrightarrow\;\mathcal{M}\models\varphi\;\stackrel{{\scriptstyle\rm
IH}}{{\leftrightarrow}}\;\mathcal{M}^{\pm}\models^{T}\varphi\;\leftrightarrow\;\mathcal{M}^{\pm}\models^{F}{\sim}\varphi.$

We leave the details to the reader. ∎

######  Lemma 9.9 ($\mathrm{BZFC}$).

For every T/F-model $\mathcal{N}$, there exists a Tarski model
$\mathcal{N}^{4}$ such that for every $\varphi$:

$\mathcal{N}\models^{T}\varphi\;\;\leftrightarrow\;\;\mathcal{N}^{4}\models\varphi$
$\mathcal{N}\models^{F}\varphi\;\;\leftrightarrow\;\;\mathcal{N}^{4}\not\models\varphi$

###### Proof.

Here we first need to take care of the equality relation, since the negative
relation $=^{-}$ of $\mathcal{N}$ is not a priori related to the meta-
theoretic $\neq$ relation for sets. We define a non-classical equivalence
relation $\equiv$ on $N$, as follows, appealing to the Anti-Classicality
Axiom:212121This is a specific case of a non-classical equivalence relation;
for more details, see [19, Section 4.8].

$a\equiv b\;\leftrightarrow\;a=b$ $a\not\equiv b\;\leftrightarrow\;a=^{-}b$

For every $a\in N$, let $[a]:=\\{b\in N:a\equiv b\\}$. This is the
$\equiv$-equivalence class of $a$, but note that we have
$a\in[b]\;\leftrightarrow\;a=b$ and $a\notin[b]\;\leftrightarrow\;a=^{-}b$. In
particular, we could have both $a\in[b]$ and $a\notin[b]$.

######  Claim 9.10.

For all $a,b\in N$ we have

$[a]=[b]\leftrightarrow a=b$ $[a]\neq[b]\leftrightarrow a=^{-}b.$

###### Proof.

If $a=b$ then clearly $[a]=[b]$. Conversely, if $[a]=[b]$ then for all $z$ we
have $z\in[a]\leftrightarrow z\in[b]$; but clearly $a\in[a]$, therefore
$a\in[b]$, so $a=b$.

Now suppose $a=^{-}b$. By definition $a\not\equiv b$ so, again by definition,
$a\notin[b]$. But then we have $a\in[a]$ but $a\notin[b]$, so (by
Extensionality) we have $[a]\neq[b]$. Conversely, suppose $[a]\neq[b]$. Then
there exists a $z\in[a]$ such that $z\notin[b]$ (or vice versa). Then $z=a$
and $z=^{-}b$, but then also $a=^{-}b$ (or vice versa). ∎(Claim)

We let the domain of $\mathcal{N}^{4}$ consist of the $\equiv$-equivalence
classes of $\mathcal{N}$, i.e., $N^{4}=\\{[a]:a\in N\\}$. Notice that we have

$\mathcal{N}\models^{T}(t=s)[a,b]\;\leftrightarrow\;a=b\;\leftrightarrow\;[a]=[b]\;\leftrightarrow\;\mathcal{N}^{4}\models(t=s)[[a],[b]]$
$\mathcal{N}\models^{F}(t=s)[a,b]\;\leftrightarrow\;a=^{-}b\;\leftrightarrow\;[a]\neq[b]\;\leftrightarrow\;\mathcal{N}^{4}\not\models(t=s)[[a],[b]]$

For every relation symbol $R$, define the interpretation $R^{\mathcal{N}^{4}}$
by:

$\;\;R^{\mathcal{N}^{4}}([a_{1}]\dots[a_{n}])\;\leftrightarrow\;(R^{\mathcal{N}})^{+}(a_{1}\dots
a_{n})$
${\sim}R^{\mathcal{N}^{4}}([a_{1}]\dots[a_{n}])\;\leftrightarrow\;(R^{\mathcal{N}})^{-}(a_{1}\dots
a_{n})$

which is again possible by appealing to the Anti-Classicality Axiom. Also note
that this is well-defined by the usual arguments.

Finally, we leave it to the reader to verify, by induction on the complexity
of $\varphi$, that for all $a_{1},\dots,a_{n}\in N$ we have

$\mathcal{N}\models^{T}\varphi[a_{1}\dots
a_{n}]\;\;\leftrightarrow\;\;\mathcal{N}^{4}\models\varphi[[a_{1}]\dots[a_{n}]]$
$\mathcal{N}\models^{F}\varphi[a_{1}\dots
a_{n}]\;\;\leftrightarrow\;\;\mathcal{N}^{4}\not\models\varphi[[a_{1}]\dots[a_{n}]]$

In particular this is true for all sentences $\varphi$, completing the proof.∎

###### Proof of Theorem 9.4 $(\mathrm{BZFC})$.

By Lemma 9.7, $\mathrm{BS4}$ is sound and complete with respect to
T/F-semantics. But by Lemmas 9.8 and 9.9, T/F-models can be replaced by
Tarski-models and vice versa. Thus T/F-semantics are equivalent to Tarski-
semantics, which completes the proof. ∎

Notice that while Lemma 9.8 only required $\mathrm{PZFC}$, in Lemma 9.9 we
really used $\mathrm{BZFC}$ in an essential way. Clearly, if all sets are
classical, then $\mathrm{BS4}$ is not complete with respect to Tarski
semantics (e.g., $(\varphi\land{\sim}\varphi)\to\bot$ is true in all models
but not $\mathrm{BS4}$-provable).

Indeed, as the reader will probably have guessed, it turns out that the logic
that is sound and complete with respect to Tarski semantics is the one
reflecting the precise level of non-classicality in the ambient meta-theory.
To make this more precise, we briefly return to Remark 5.4: recall that if one
is interested in a set theory which has only inconsistent but not incomplete
sets, or only incomplete but not inconsistent sets, one can consider two
fragments of the Anti-Classicality Axiom:

  * •

$\boldsymbol{\mathrm{ACLA}_{\rm cons}:}\boldsymbol{\;\;\forall
x(x^{!}\subseteq x^{?})\land\exists x(x^{?}\not\subseteq x^{!})}$

(all sets are consistent, but there is an incomplete set).

  * •

$\boldsymbol{\mathrm{ACLA}_{\rm comp}:\;\;\forall x(x^{?}\subseteq
x^{!})\land\exists x(x^{!}\not\subseteq x^{?})}$

(all sets are complete, but there is an inconsistent set).

We can now look at three-valued logics which arise if we adapt Definitions
2.2–2.4 to deal with only incompleteness or only inconsistency.

######  Definition 9.11 (PZFC).

  * •

K3→ is the logic corresponding to T/F-models $\mathcal{M}$ such that, for all
$R$ (including equality)
$(R^{\mathcal{M}})^{+}\cap(R^{\mathcal{M}})^{-}=\varnothing$.

  * •

LFI1 is the logic corresponding to T/F-models $\mathcal{M}$ such that, for all
$R$ (including equality) $(R^{\mathcal{M}})^{+}\cup(R^{\mathcal{M}})^{-}=M$
(the whole domain).

The reason for adopting the names K3→ and LFI1 is that these are essentially
the logics that appeared in [9] and [12], respectively.222222These papers only
considered a propositional version, but the essence is the same.

The following theorem, which tells us exactly which logic is sound and
complete with respect to Tarski semantics, provably in PFZC, follows by
methods similar to the above.We leave the details to the reader ($\vdash_{\rm
FOL}$ refers to classical logic).

######  Theorem 9.12 (PZFC).

  1. 1.

$\mathrm{ACLA}\;\leftrightarrow\;(\Sigma\models\varphi\;\;\leftrightarrow\;\;\Sigma\vdash_{\>\mathrm{BS4}}\varphi).$

  2. 2.

$\mathrm{ACLA}_{\rm
cons}\;\leftrightarrow\;(\Sigma\models\varphi\;\;\leftrightarrow\;\;\Sigma\vdash_{\>{\rm
K3}^{\to}}\varphi).$

  3. 3.

$\mathrm{ACLA}_{\rm
comp}\;\leftrightarrow\;(\Sigma\models\varphi\;\;\leftrightarrow\;\;\Sigma\vdash_{\>\rm
LFI1}\varphi).$

  4. 4.

$\forall
x(x^{!}=x^{?})\;\leftrightarrow\;(\Sigma\models\varphi\;\;\leftrightarrow\;\;\Sigma\vdash_{\>\rm
FOL}\varphi).$

  5. 5.

Exactly one of the above four options holds.

If we restrict attention to formulas that do not contain implications or
$\bot$, we obtain similar results for much more familiar systems, namely the
ones usually referred to as K3, LP and FDE (the “$\to$”- and “$\bot$”-free
fragments of K3→, LFI1, and $\mathrm{BS4}$, respectively, see [14, 21, 3]).

######  Theorem 9.13 (PZFC).

Suppose $\Sigma$ and $\varphi$ do not contain “$\to$” or “$\bot$”. Then:

  1. 1.

$\mathrm{ACLA}\;\leftrightarrow\;(\Sigma\models\varphi\;\;\leftrightarrow\;\;\Sigma\vdash_{\>\rm
FDE}\varphi).$

  2. 2.

$\mathrm{ACLA}_{\rm
cons}\;\leftrightarrow\;(\Sigma\models\varphi\;\;\leftrightarrow\;\;\Sigma\vdash_{\>{\rm
K3}}\varphi).$

  3. 3.

$\mathrm{ACLA}_{\rm
comp}\;\leftrightarrow\;(\Sigma\models\varphi\;\;\leftrightarrow\;\;\Sigma\vdash_{\>\rm
LP}\varphi).$

  4. 4.

$\forall
x(x^{!}=x^{?})\;\leftrightarrow\;(\Sigma\models\varphi\;\;\leftrightarrow\;\;\Sigma\vdash_{\>\rm
FOL}\varphi).$

  5. 5.

Exactly one of the above four options holds.

##  10 Conclusion

We conclude by reflecting on and discussing our results, as well as outlining
some future research directions.

While other authors have presented formalizations of paraconsistent and
paracomplete set theory, we believe that our approach establishes a more
complete and fully developed theory than any previous attempts. The system
$\mathrm{BZFC}$ has clear intuitive underpinnings making it easy to reason
about paraconsistent and paracomplete phenomena informally, as well as a well-
defined ontology of non-classical sets allowing us to construct models and
reason about them from a classical perspective if desired. Moreover, our
approach (based in part on the careful analysis of the axioms in Section 4)
seems to overcome many obstacles previous authors were faced with. For
instance, in the approach of Carnielli and Coniglio [8], most of the axioms
are translated using the native implications $\to$ and $\leftrightarrow$
instead of the strong implications. As a result, the authors struggle with
providing a coherent model theory.

The non-classicality axiom $\mathrm{ACLA}$ and Theorem 5.2 have likewise, to
our knowledge, not appeared anywhere previously. A proper understanding of
this axiom and its consequences was vital for the study of Tarski semantics in
$\mathrm{BZFC}$, as we have done in Section 9.4.

Finally, we feel that the bi-interpretability results from Sections 7 and 8
are extremely helpful, as mathematicians are free to switch between viewing
$\mathrm{BZFC}$ as the theory of a particular structure within $\mathrm{ZFC}$,
or viewing $\mathrm{ZFC}$ as the theory of a particular structure within
$\mathrm{BZFC}$.

A legitimate concern may be: what is the overall motivation for studying
paraconsistent and paracomplete set theory, and $\mathrm{BZFC}$ in particular?

We can say with certainty that $\mathrm{BZFC}$ does not help to avoid
Russell’s paradox. As mentioned, we do not think that Russell’s paradox is
something that should be avoided. Nevertheless, there are other interesting
“contradictions” in set theory and mathematics, such as Kunen’s inconsistency
[15] which puts an upper bound on the hierarchy of large cardinals. It is not
inconceivable that $\mathrm{BZFC}$ may help to shed new light on this and
related phenomena.

We also feel that the results on Tarski semantics in Section 9.4, and to a
lesser extent the bi-interpretability results, may lead to new insights in the
philosophy of mathematics and logic, such as formal theories of truth.

On a more down-to-earth level, applications of $\mathrm{BZFC}$ are conceivable
in computer science, for example in the study of databases or structures with
incomplete or inconsistent information. Say, we want an automated system to
derive logical consequences based on data in a large database. Presumably,
this system should not be able to derive any sentence whatsoever merely from
the fact that $R(a)\land{\sim}R(a)$ holds, which could be due to a wrong entry
in the database.

Finally, an answer to the above concern may be that there are applications of
$\mathrm{BZFC}$ that we do not know yet. Peter Aczel’s non-well-founded set
theory [2] was initially instigated out of curiosity, but has subsequently
found applications in reasoning about circular phenomena in computer science.
The Axiom of Determinacy was initially introduced in [17] as a “…theory which
seems very interesting although its consistency is problematic”, but
eventually led to some of the biggest breakthroughs in descriptive set theory,
large cardinals and inner model theory.

Above all, with this paper we hope to instigate more research in the area of
paraconsistent mathematics, dragging it out of the realm of speculative
attempts into a more mainstream part of serious set theory. Some suggestions
for future research are listed below.

  1. 1.

Algebraic approach. The logic $\mathrm{BS4}$ and set theory in $\mathrm{BS4}$
can also be approached from an algebraic point of view, via so-called twist
algebras. This can even be used to study an analogue of Boolean-valued models
(closely related to forcing over classical models of $\mathrm{ZFC}$) in the
$\mathrm{PZFC}$\- or $\mathrm{BZFC}$-context. A large part of this has already
been done, see [19, Chapter 3 and Chapter 8], but there are more things that
can be studied.

  2. 2.

Computability theory. One natural application of $\mathrm{BZFC}$ comes from
computability theory. Let us say that a Turing machine $M$ _computes_ a set
$A\subseteq\mathbb{N}$ if for all $n$:

     * •

$n\in A\;\leftrightarrow\;M$ halts on input $n$ and outputs some non-$0$
value.

     * •

$n\notin A\;\leftrightarrow\;M$ halts on input $n$ and outputs $0$.

Moreover, let us say that $M$ _recognizes_ a set $A\subseteq\mathbb{N}$ if for
all $n$:

     * •

$n\in A\;\leftrightarrow\;M$ halts on input $n$ and outputs some non-$0$
value.

In classical mathematics, every Turing machine recognizes a set, but not every
Turing machine computes a set (since it may not halt on some input). Thus, one
cannot use sets $A\subseteq\mathbb{N}$ to represent decisions of a machine.

Let us revisit the situation in BZFC (or even
$\text{PZFC}+\text{ACLA}_{\text{cons}}$). Using the same definition as above,
it follows from Theorem 5.2 that every Turing machine computes a set. If a
given machine does not halt on some input $n$, it just means that the machine
computes an incomplete set $A$ (for which $\lnot(n\in A\lor n\notin A))$. In
particular, the decision process of a machine can be completely described by
subsets of $\mathbb{N}$.

  3. 3.

Cardinal arithmetic. Finally, we will need a new notion of _cardinality_
together with new type of _cardinal numbers_ to describe the size of our non-
classical sets. It is clear that this notion should capture the structure of
non-classical sets, i.e., it should capture the size of the $!$-extensions,
$?$-extensions, and the overlap, in one go. We expect that this will lead to a
rich theory of cardinals and cardinal arithmetic.

Acknowledgments

The authors would like to thank Benno van den Berg, Luca Incurvati, Benedikt
Löwe, Hitoshi Omori, Andrew Tedder and Giorgio Venturi for insightful
conversations, helpful suggestions and ideas.

## References

  * [1] Peter Aczel.  The type theoretic interpretation of constructive set theory.  In Logic Colloquium ’77 (Proc. Conf., Wrocław, 1977), volume 96 of Studies in Logic and the Foundations of Mathematics, pages 55–66. North-Holland, Amsterdam-New York, 1978.
  * [2] Peter Aczel.  Non-well-founded sets, volume 14 of CSLI Lecture Notes.  Stanford University, Center for the Study of Language and Information, Stanford, CA, 1988.  With a foreword by Jon Barwise [K. Jon Barwise].
  * [3] F. G. Asenjo.  A calculus of antinomies.  Notre Dame J. Formal Logic, 7:103–105, 1966.
  * [4] Arnon Avron.  Natural $3$-valued logics—characterization and proof theory.  J. Symbolic Logic, 56(1):276–294, 1991.
  * [5] Diderik Batens, Kristof De Clercq, and Natasha Kurtonina.  Embedding and interpolation for some paralogics. The propositional case.  Rep. Math. Logic, (33):29–44, 1999.
  * [6] Nuel D. Belnap.  How a computer should think.  In New essays on Belnap-Dunn logic, volume 418 of Synth. Libr., pages 35–53. Springer, Cham, [2019] ©2019.
  * [7] Nuel D. Belnap.  A useful four-valued logic.  In New essays on Belnap-Dunn logic, volume 418 of Synth. Libr., pages 55–76. Springer, Cham, [2019] ©2019.
  * [8] Walter Carnielli and Marcelo E. Coniglio.  Paraconsistent set theory by predicating on consistency.  J. Logic Comput., 26(1):97–116, 2016.
  * [9] Walter Carnielli, Marcelo E. Coniglio, and João Marcos.  Logics of Formal Inconsistency, pages 1–93.  Springer Netherlands, Dordrecht, 2007.
  * [10] J. Michael Dunn.  Intuitive semantics for first-degree entailments and ‘coupled trees’.  Philos. Studies, 29(3):149–168, 1976.
  * [11] Harvey Friedman.  Set theoretic foundations for constructive analysis.  Ann. of Math. (2), 105(1):1–28, 1977.
  * [12] Allen P. Hazen and Francis Jeffry Pelletier.  K3, ł 3,LP, RM3, A3, FDE, M: how to make many-valued logics work for you.  In New essays on Belnap-Dunn logic, volume 418 of Synth. Libr., pages 155–190. Springer, Cham, [2019] ©2019.
  * [13] Roland Hinnion.  About the coexistence of “classical sets” with “non-classical” ones: a survey.  Number 11-12, pages 79–90. 2003.  Flemish-Polish Workshops II–IV and varia.
  * [14] S. C. Kleene.  On notation for ordinal numbers.  Journal of Symbolic Logic, 3(4):150?155, 1938.
  * [15] Kenneth Kunen.  Elementary embeddings and infinitary combinatorics.  J. Symbolic Logic, 36:407–413, 1971.
  * [16] Thierry Libert.  Models for a paraconsistent set theory.  J. Appl. Log., 3(1):15–41, 2005.
  * [17] Jan Mycielski and H. Steinhaus.  A mathematical axiom contradicting the axiom of choice.  Bull. Acad. Polon. Sci. Sér. Sci. Math. Astronom. Phys., 10:1–3, 1962.
  * [18] John Myhill.  Constructive set theory.  J. Symbolic Logic, 40(3):347–382, 1975.
  * [19] Hrafn Valtýr Oddsson.  Paradefinite Zermelo-Fraenkel set theory: A theory of inconsistent and incomplete sets.  Master’s thesis, Universiteit van Amsterdam, 2021.  ILLC Publication MoL-2021-27.
  * [20] Hitoshi Omori and Toshiharu Waragai.  Some observations on the systems LFI1 and LFI1.  In 22nd International Workshop on Database and Expert Systems Applications, pages 320–324, 2011.
  * [21] Graham Priest.  The logic of paradox.  J. Philos. Logic, 8(2):219–241, 1979.
  * [22] Helena Rasiowa.  An algebraic approach to non-classical logics.  Studies in Logic and the Foundations of Mathematics, Vol. 78. North-Holland Publishing Co., Amsterdam-London; American Elsevier Publishing Co., Inc., New York, 1974.
  * [23] Katsuhiko Sano and Hitoshi Omori.  An expansion of first-order Belnap-Dunn logic.  Log. J. IGPL, 22(3):458–481, 2014.