Topological Semantics for da Costa Paraconsistent Logics $C_\omega$ and $C^{*}_\omega$

Abstract

In this work, we consider a well-known and well-studied system of paraconsistent logic which is due to Newton da Costa, and present a topological semantics for it.

1 Introduction

In a paraconsistent logic, contradictions do not entail everything. Namely, in a paraconsistent logic, there are some formula $\varphi , \psi$ such that $\{ \varphi , \lnot \varphi \} \not \vdash \psi$ for a logical consequence relation $\vdash$. In this work, we will focus on a well-known and well-studied paraconsistent logic, which is due to Newton da Costa, and present a topological semantics for it.

Da Costa’s hierarchical systems $C_n$ and $C_n^{*}$ are one of the earliest examples of paraconsistent logic [7]. Da Costa systems $C_n$ where $n < \omega$ are consistent and finitely trivializable. Yet, for the limit ordinal $\omega$, it is possible to obtain a logic $C_\omega$ which is not finitely trivializable [8]. In this work, we focus on $C_\omega$ and its first-order cousin $C^{*}_\omega$ both of which are paraconsistent.

Da Costa systems are not unfamiliar. As Priest remarked, the logic $C_\omega$ can be thought of as the positive intuitionistic logic with dualized negation to give truth value gluts [21]. We define $C_\omega$ with the following postulates [7, 8].

• 1. $\varphi \rightarrow (\psi \rightarrow \varphi )$

• 2. $(\varphi \rightarrow \psi ) \rightarrow ((\varphi \rightarrow (\psi \rightarrow \chi )) \rightarrow (\varphi \rightarrow \chi ))$

• 3. $\varphi \wedge \psi \rightarrow \varphi$

• 4. $\varphi \wedge \psi \rightarrow \psi$

• 5. $\varphi \rightarrow (\psi \rightarrow \varphi \wedge \psi )$

• 6. $\varphi \rightarrow \varphi \vee \psi$

• 7. $\psi \rightarrow \varphi \vee \psi$

• 8. $(\varphi \rightarrow \chi ) \rightarrow ((\psi \rightarrow \chi )\rightarrow (\varphi \vee \psi \rightarrow \chi ))$

• 9. $\varphi \vee \lnot \varphi$

• 10. $\lnot \lnot \varphi \rightarrow \varphi$

The rule of inference that we need is modus ponens: $\varphi , \varphi \rightarrow \psi \therefore \psi$.

Based on this axiomatization, Baaz gave a Kripke-type semantics for $C_\omega$ [3]. Baaz’s $C_\omega$-Kripke model is a tuple $M = \langle W, \le , V, T \rangle$ where W is a nonempty set, $\le$ is a partial order on W, and V is a valuation that returns a subset of W for every propositional variable in the language. We will call the members of W as possible worlds or states. By accessible states from $w \in W$, we will mean the set $\{ v: wRv \}$. The additional component T is a function defined from possible worlds to the sets of negated propositional forms. The imposed condition on T is the monotonicity: $w \le v$ implies $T(w) \subseteq T(v)$. Monotonicity condition resembles the hereditary condition of intuitionistic logic. The valuation respects the monotonicity and is assumed to return upsets. In this context, an upset U is a subset of W such that if $w \in U$ and $w \le v$, then $v \in U$.

Also note that the relation $\le$ is a partial order rendering the frame $\langle W, \le \rangle$, an $\mathbf {S4}$-frame. The fact that the frame of Baaz’s model is $\mathbf {S4}$ and will be central in our topological investigations later.

One of the most interesting properties of da Costa systems is the principle of nonsubstitution for negated formulas. For instance, even if p and $p \wedge p$ are logically equivalent, i.e., $p \equiv p \wedge p$, we do not necessarily have that $\lnot p \equiv \lnot (p \wedge p)$ in da Costa systems, where $\equiv$ denotes logical equivalence. In Baaz’s construction, the function T returns a set of formulas which are negated at that possible world. Yet, for a possible world w, the set T(w) is not necessarily a theory as it need not be closed under logical equivalence. In short, at w, we can have $\lnot p \in T(w)$, but this does not imply that $\lnot (p \wedge p) \in T(w)$. Monotonicity of T, on the other hand, reflects the intuitionistic side of da Costa systems. In the partially ordered Kripkean frame for $C_\omega$, children nodes have the same formulas as their parents and possibly more under T.

Baaz gave a Kripkean semantics for $C_\omega$ as follows [3]. But first, let us set up some notation. We put $\lnot ^0 \varphi \equiv \varphi$ and $\lnot ^{n+1} \varphi \equiv \lnot (\lnot ^n \varphi )$ for a formula $\varphi$ which does not include a negation sign in the front.

$w \models p$	iff	for all v such that $w \le v$, $v \models p$ for atomic p
$w \models \varphi \wedge \psi$	iff	$w \models \varphi$ and $w \models \psi$
$w \models \varphi \vee \psi$	iff	$w \models \varphi$ or $w \models \psi$
$w \models \varphi \supset \psi$	iff	for all v such that $w \le v$, $v \models \varphi$ implies $v \models \psi$
$w \models \lnot ^1 \varphi$	iff	$\lnot ^1 \varphi \in T(w)$ or $\exists v$.$v \le w$ and $v \not \models \varphi$
$w \models \lnot ^{n+2} \varphi$	iff	$\lnot ^{n+2} \varphi \in T(w)$ and $w \models \lnot ^n \varphi$, or
		$\exists v$.$v \le w$ and $v \not \models \lnot ^{n+1} \varphi$
$w \models \varphi _1, \dots , \varphi _n \rightarrow$	iff	$\forall v$.$w \le v$, $w \models \varphi _1, \dots , w \models \varphi _n$ imply
$\qquad \psi _1, \dots , \psi _n$		$v \models \psi _1$ or ...or $v \models \psi _n$

Let us now briefly comment on the semantics. First of all, the above semantics admits the hereditary condition for propositional variables. The truth of propositional variables persists throughout the accessible states. This is an interesting property that resembles what is commonly known as the hereditary condition of intuitionistic logic. Another similarity between da Costa systems and the intuitionistic logic is the way the semantics of implication is defined. Perhaps the most interesting and distinguishing part of the above semantics is the semantics of negation. A negated formula is true at a state w if it is in T(w) or there is a predecessor state at which the formula does not hold. It is important to underline that the function T renders the negation as a nonfunctional operator. This is another way of saying that substitution principle for negated formulas does not hold in da Costa systems. Finally, in the syntax of the operator $\rightarrow$, we can very well have the empty set as the antecedent. The statement $\emptyset \rightarrow p, q$ will be shortened as $\rightarrow p, q$.

Using the proof theory of (propositional) intuitionistic logic and Gentzen style calculus, Baaz showed the soundness, completeness, and decidability of this system [3]. We will henceforth denote this system as $KC_\omega$.

2 Topological Models $TC_\omega$

In this section, we give a topological semantics for da Costa’s system $C_\omega$, and call our formalism as $TC_\omega$. The topological semantics precedes the Kripke semantics, and was first presented in early 1920s [12]. The major developments in the field of topological semantics for (modal) logics have been initiated by J.C.C. McKinsey and Alfred Tarski in 1940s in a series of papers [14–16].

A topology $\sigma$ is a collection of subsets of a set S that satisfies the following conditions. The empty set and S are in $\sigma$, and $\sigma$ is closed under arbitrary unions and finite intersections. The elements of $\sigma$ are called opens. Complement of an open set is called a closed set. A topological space is defined as the tuple $(S, \sigma )$. For a given set U, the interior operator $\mathsf {Int}$ returns the largest open set contained in U whereas the closure operator $\mathsf {Clo}$ returns the smallest closed set that contains U. For a set U, we define the boundary of U as $\mathsf {Clo}(U) - \mathsf {Int}(U)$, and denote it as $\partial (U)$. Therefore, by definition, closed sets include their boundary whereas open sets do not.

In the classical modal case, McKinsey and Tarski associated the modal operator $\Box$ with the topological interior operator (and, dually $\Diamond$ with the closure operator), and observed that the interior and closure operators behave as $\mathbf {S4}$ modalities (normal, reflexive, and transitive). The well-known McKinsey–Tarski result showed that $\mathbf {S4}$ is the modal logic of topological spaces, in fact, of any metric, separable, dense-in-itself space. This result has been extended to various other nonclassical logics, and the topological semantics for intuitionistic and some paraconsistent logics have also been given [4, 13, 17].

In this section, we first give a topological semantics for $C_\omega$ based on the Kripkean semantics, and then we discuss various topological notions that relate topological spaces and $TC_\omega$.

2.1 Topological Semantics

The language of $TC_\omega$ is the language of propositional logic with the usual Boolean conjunction, disjunction, and implication, and we will allow iterated negations. We denote the closure of a set X by $\mathsf {Clo}(X)$. If a set $\{ x \}$ is a singleton, we write $\mathsf {Clo}(x)$ instead of $\mathsf {Clo}(\{x\})$ provided no confusion arises. Also note that in this case $\mathsf {Clo}(x)$ is the intersection of all closed sets containing x.

The language of $TC_\omega$ is built using a countable set of propositional variables which we denote by $\mathbf {P}$. Now, we start with defining $TC_\omega$ models.

Definition 19.2.1

A $TC_\omega$ model M is a tuple $M = \langle S, \sigma , V, N \rangle$ where S is a nonempty set, $\sigma$ is an Alexandroff topology on S, $V: \mathbf {P} \rightarrow \wp (S)$ is a valuation function, and N is a (full) function which takes possible worlds $s \in S$ as inputs and returns sets of negated propositional forms (possibly empty) in such a way that $w \in \mathsf {Clo}(v)$ implies $N(w) \subseteq N(v)$.

Here, we resort to the standard translation between topological models and Kripke frames. Given a topological space, we put $w \le v$ for $w \in \mathsf {Clo}(v)$ to obtain a partially ordered tree, which produces the Kripke frame. Conversely, given a Kripke frame with a partial order, we consider the upward closed (or dually, downward closed) branches of the tree as open sets (dually, closed sets) to construct a topology. The topology we obtain from a given Kripke frame is an Alexandroff topology which is closed under arbitrary intersections. In other words, since the Baaz’s frames are already $\mathbf {S4}$, the topology we obtain (after translating the given $\mathbf {S4}$ frame) is an Alexandroff topology. We refer the reader to [23] for a detailed treatment of the subject from a modal logical perspective.

Interestingly, the fact that we obtain Alexandroff spaces in $TC_\omega$ raises the question of handling non-Alexandroff spaces in the topological models of $C_\omega$. This is a very interesting question in-self, and can help us identify a variety of formalisms that are weaker than $C_\omega$. In order not to digress from our current focus, we leave it for a future work.

Now, we give the semantics of $TC_\omega$ as follows. We abbreviate $\lnot ^0 \varphi := \varphi$, and $\lnot ^{n+1} \varphi := \lnot (\lnot ^n \varphi )$ for a $\varphi$ which does not include a negation sign in the front. Similarly, we assume that the valuation function V returns closed sets [4].

$w \models p$	iff	$\forall v$.$w \in \mathsf {Clo}(v)$, $v \models p$ for atomic p
	iff	$w \in V(p)$
$w \models \varphi \wedge \psi$	iff	$w \models \varphi$ and $w \models \psi$
$w \models \varphi \vee \psi$	iff	$w \models \varphi$ or $w \models \psi$
$w \models \varphi \supset \psi$	iff	$\forall v$.$w \in \mathsf {Clo}(v)$, $v \models \varphi$ implies $v \models \psi$
$w \models \lnot ^1 \varphi$	iff	$\lnot ^1 \varphi \in N(w)$ or $\exists v$.$v \in \mathsf {Clo}(w)$ and $v \not \models \varphi$
$w \models \lnot ^{n+2} \varphi$	iff	$\lnot ^{n+2} \varphi \in N(w)$ and $w \models \lnot ^n \varphi$    or
		$\exists v$.$v \in \mathsf {Clo}(w)$ and $v \not \models \lnot ^{n+1} \varphi$
$w \models \varphi _1, \dots , \varphi _n \rightarrow$	iff	$\forall v$.$w \in \mathsf {Clo}(v)$, $v \models \varphi _1, \dots , v \models \varphi _n$ imply
$\qquad \psi _1, \dots , \psi _n$		$v \models \psi _1$ or ...or $v \models \psi _n$

Following the usual representation, we denote the extension of a formula $\varphi$ in a model M by $[\varphi ]^M$, and define it as follows $[\varphi ]^M : = \{ w : M, w \models \varphi \}$.

Now we can discuss the satisfiability problem (SAT) and its complexity in logic $C_\omega$ and $KC_\omega$. First of all, note that the complexity of SAT for basic modal logic is known to be PSPACE-complete. In Kripkean frames, searching for a satisfying assignment may not be efficient timewise, but it uses the space efficiently yielding a PSPACE-complete complexity. This procedure can be thought of as searching the branches of a Kripke model (which is a tree or a forest) starting from the root. Once you are done with one branch, you do not need to remember it, thus you can reuse the same space. And, the extent of the tree you need to search, i.e., the depth, solely depends on the length of the formula. Therefore, the given formula determines the space you need to check. In $KC_\omega$, the only issue is checking the satisfiability for negation. However, a careful examination shows that it has a rather immediate solution. The case for $\lnot ^1$ requires two operations: check whether a given $\lnot ^1$ is in the image set of T at the given state, and check if there exists a state that is accessible from the current state with the desired condition. The latter part is PSPACE considering the standard modal argument for SAT. The prior part is also polynomial—it is a sequential check for membership. Moreover, one can easily construct a polynomial transformation from modal SAT with topological semantics to $KC_\omega$ satisfiability yielding the fact that SAT for $KC_\omega$ is also PSPACE. Considering $\lnot ^n$ as a nested (intuitionistic) modality, one can come up with the obvious translation giving the PSPACE-completeness of the satisfiability problem for $KC_\omega$. In order to show the complexity of $TC_\omega$, we need to reduce it to $KC_\omega$. Yet, we already saw how to obtain a topological model given a Kripke model, and this translation reduces $KC_\omega$ to $TC_\omega$.

Now, based on the above-mentioned argument, and the efficient model transformations between topological spaces and Kripke frames which we discussed earlier, it is immediate to observe that SAT for $TC_\omega$ is also PSPACE-complete.

Theorem 19.2.2

The satisfiability problem for both $KC_\omega$ and $TC_\omega$ is PSPACE-complete.

Corollary 19.2.3

Both $KC_\omega$ and $TC_\omega$ are decidable.

In his work, Baaz gave several results using Kripke semantics [3]. Here, we observe that they hold in $TC_\omega$ as well. Our aim is to clarify the use of topological concepts in $TC_\omega$, and make sure that the function N works as expected. The following results will also exemplify the behavior of negation in $TC_\omega$.

Proposition 19.2.4

$w \models \varphi$ iff for all v such that $w \in \mathsf {Clo}(v)$, we have $v \models \varphi$.

Proof

The proof is by induction on the length of the formula. The only interesting case is the negation. We assume $\varphi \equiv \lnot ^1 \psi$. Then, let us suppose $w \models \lnot ^1 \psi$. By definition, either $\lnot ^1 \psi \in N(w)$ or there exists a x such that $x \in \mathsf {Clo}(w)$ and $x \not \models \psi$. Now, let v be such that $w \in \mathsf {Clo}(v)$. Then, by the definition of N, we observe $N(w) \subseteq N(v)$. Thus, $\lnot ^1 \psi \in N(v)$. On the other hand, $w \in \mathsf {Clo}(v)$ implies that $\mathsf {Clo}(w) \subseteq \mathsf {Clo}(v)$. Therefore, $w \in \mathsf {Clo}(w) \subseteq \mathsf {Clo}(v)$ with $v \not \models \psi$. Then, we have either $\lnot ^1 \psi \in N(w)$ or there exists x such that $x \in \mathsf {Clo}(v)$ with $x \not \models \psi$. Thus, $v \models \lnot ^1 \psi$.

The cases for $\lnot ^{n+1}$ are similar using the induction hypothesis. $\square$

Proposition 19.2.5

$w \not \models \varphi$ implies that there is no $v \in \mathsf {Clo}(w)$ such that $v \not \models \lnot \varphi$.

Proof

Let $w \not \models \varphi$. Toward a contradiction, we assume that there is a $v \in \mathsf {Clo}(w)$ with $v \not \models \lnot \varphi$. On the other hand, by Proposition 19.2.4, $v \not \models \lnot \varphi$ means that for all w such that $v \in \mathsf {Clo}(w)$, we have $w \not \models \lnot \varphi$. Thus, we conclude $w \not \models \varphi$ and $w\not \models \lnot \varphi$. Contradiction. $\square$

Proposition 19.2.6

$w \models \lnot \lnot \varphi \rightarrow \varphi$.

Proof

We will show that $w \not \models \varphi$ implies $w \not \models \lnot \lnot \varphi$. Let $w \not \models \varphi$. Then, by Proposition 19.2.5, there is no $v \in \mathsf {Clo}(w)$ with $v \not \models \lnot \varphi$. Then, by definition of $\lnot ^2$, we conclude that $w \not \models \lnot \lnot \varphi$. $\square$

Substitution principle for negated formulas $\lnot \varphi \leftrightarrow \lnot (\varphi \wedge \varphi )$ does not hold in $KC_\omega$. Next, we observe that it does not hold in $TC_\omega$ as well.

Proposition 19.2.7

$\lnot \varphi \leftrightarrow \lnot (\varphi \wedge \varphi )$ is not valid.

Proof

Let us take a state w such that $\mathsf {Clo}(w) \subseteq [\varphi ]$ and $\lnot \varphi \in N(w)$. Thus, $w \models \lnot \varphi$. We now stipulate further that $\lnot (\varphi \wedge \varphi ) \not \in N(w)$ to get a countermodel. $\square$

Proposition 19.2.8

$w \models \rightarrow \varphi , \lnot \varphi$.

Proof

We recall that $\rightarrow \varphi _1, \dots , \varphi _n$ means that $\varphi _1 \vee \dots \vee \varphi _n$ holds. Then, the result follows from the axiomatization of $C_\omega$. $\square$

For the completeness of our arguments in this work, we now present the semantical counterpart of cut elimination. The proof is a straightforward manipulation of formulas, hence, we skip it.

Proposition 19.2.9

$w \models \Pi \rightarrow \Gamma , \varphi$ and $w \models \varphi , \Delta \rightarrow \Lambda$ imply $w \models \Pi , \Delta \rightarrow \Gamma , \Lambda$.

We now state the soundness theorem without a proof.

Theorem 19.2.10

$\vdash \varphi \rightarrow \psi$ implies $\models \varphi \rightarrow \psi$.

Baaz used Gentzen style sequent calculus to show the completeness of his system. He then concluded that if $\Pi \rightarrow \Gamma$ is not provable without cuts, there is a $KC_\omega$-Kripke model $M = \langle W, \le , v, T \rangle$ such that $0 \in W$ and $0 \not \models \Pi ' \rightarrow \Gamma '$ where $\Pi ' \equiv \Pi , \Delta$ and $\Gamma ' \equiv \Gamma , \Psi$. Namely, $M \not \models \Pi \rightarrow \Gamma$. Here, 0 is the lowest top sequent in the reduction tree of $\Pi \rightarrow \Gamma$.

Now, in order to show the completeness of our system $TC_\omega$, we will resort to the model translation which we mentioned earlier. Given a $KC_\omega$ model $M = \langle W, \le ~, v, T \rangle$, we can construct a $TC_\omega$ model $M' = \langle S, \sigma , V, N \rangle$ as follows. Let $S : = W$, and $V : = v$. Now, we need to define the topology $\sigma$, and the open and closed sets in $\sigma$. Define closed sets as the upsets, and observe that $v \in \mathsf {Clo}(w)$ whenever $v \le w$. For a tree model, it is easy to observe that the closed sets we defined produces an Alexandroff topology, as we already observed. Furthermore, we put $N(w) := T(w)$. Therefore, given a $TC_\omega$ model, we can effectively convert it to $KC_\omega$ which is known to be complete. This is the immediate method to show the completeness of $TC_\omega$. Alternatively, we can start with the logic $TC_\omega$, and give a topological completeness proof. This is what we achieve next.

For the completeness of $TC_\omega$, we use maximal nontrivial sets of formulas. A set X is called trivial if every formula in the language is deducible from X, otherwise it is called nontrivial. A nontrivial set X is called a maximal nontrivial set if $\varphi \notin X$, then $X \cup \{ \varphi \}$ is trivial, for an arbitrary formula $\varphi$.

We start by observing the following:

Proposition 19.2.11

If $\Gamma$ is a maximal nontrivial set of formulas, then we have $\Gamma \vdash \varphi$ iff $\varphi \in \Gamma$.

Using canonical sets, we construct the canonical $TC_\omega$ model $\langle S', \sigma ', V', N' \rangle$. Let us first start with the canonical topological space. The canonical topological space is the pair $\langle S', \sigma ' \rangle$ where $S'$ is the set of all maximal nontrivial sets, and $\sigma '$ is the set generated by the basis $B = \{ \widehat{\lnot \varphi } : \text { any formula } \varphi \}$ where we define $\widehat{\varphi }:= \{ s' \in S' : \varphi \in s' \}$. Here, our construction is very similar to the classical case: instead of (classical) modal formula, we use negated formulas in the construction of the canonical model (and its topology). The reason for this choice is the fact that in $TC_\omega$ negated formulas resort to the closure operator—similar to the modal operators in the classical case.

In order to show that B is a basis for the topology $\sigma '$, we need to show that

• 1. For any $U, U' \in B$ and any $x \in U \cap U'$, there is $U_x \in B$ such that $x \in U_x \subseteq U \cap U'$,

• 2. For any $x \in S'$, there is $U \in B$ with $x \in U$.

For the first item, we observe that $\lnot \widehat{\varphi \wedge \chi } = \widehat{\lnot \varphi } \wedge \widehat{\lnot \chi }$. Therefore, $U \cap U' \in B$ which argues for finite intersection.

For the second item, we observe that $\lnot \bot \in x$ for any maximal consistent set x in the canonical $TC_\omega$. Therefore, for any $x \in S'$, there is a $\widehat{\lnot \bot } \in B$ that includes x.

This argument shows that B is a basis for the topology of the canonical model.

Now, the valuation $V'$ is defined in the standard way: $V'(p) : = \{ s' \in S' : p \in s' \}$. Similarly, we define $N'$ from $S'$ to sets of formulas, and put, $N'(s') \subseteq N'(t')$ if $s' \in \mathsf {Clo}(t')$ for $s', t' \in S'$. Additionally, we impose that $N'(s') \subseteq s'$ to handle the negated formula correctly. Another way of looking at it is to include $N'(s')$ into $s'$ in the construction of the maximal nontrivial set $s'$. Therefore, we close maximally consistent sets under logical connectives and also under the $N'$ function. This simply reflects how the negation is defined in $TC_\omega$.

The truth of classical Booleans are defined as usual in the canonical models. For negation, we put the following.

$$s' \models \lnot ^1 \varphi \text { iff } \lnot ^1 \varphi \in N'(s') \text { or } \exists t' \in \mathsf {Clo}(s') \text { such that } t' \not \models \varphi $$

For the truth lemma, we only need to observe that, $s' \models \varphi$ if and only if $\varphi \in s'$.

The standard Boolean cases are immediate. So, let us take $\varphi = \lnot ^1 \psi$ for some $\psi$. For “truth to membership” direction, if $\lnot ^1 \psi \in N'(s')$, then we are done as $N'(s') \subseteq s'$. Otherwise, we need to find a $t'$ in $\textsf {Clo}(s')$ which does not satisfy $\psi$. Since the topology $\sigma$ is constructed using a basis with opens, we can select $t'$ from the boundary $\partial (s')$ which is not in the interior of the extension, but in the closure of the extension by definition.

For instance, if the space is discrete and the boundary is empty, then we can take any point from $s'$ as each subset of the space is clopen (both closed and open) so that $\mathsf {Clo}(s') = s' = \mathsf {Int}(s')$. Therefore, let us here argue assuming that the boundary is not empty (if it is, we still know what to do as described above).

Take such a $t' \in \partial (s')$ such that $t' \not \models \psi$. Then, by the induction hypothesis, $\psi \notin t'$. The set $t'$ is maximal and nontrivial, so $\lnot ^1 \psi \in t'$. Recall that $t' \in \mathsf {Clo}(s')$, thus $\lnot ^1 \psi \in \mathsf {Clo}(s')$.

This was the direction from “truth to membership”. The direction from “membership to truth” is similar using some properties of closure operators, so we skip it. Similarly, we leave the case $\varphi = \lnot ^{n+2} \psi$ to the reader as it only requires an inductive proof.

After establishing the truth lemma, we have the following completeness result.

Theorem 19.2.12

For any set of formulas $\Sigma$ in $TC_\omega$, if $\Sigma \models \varphi$ then, $\Sigma \vdash \varphi$.

Proof

Assume $\Sigma \not \vdash \varphi$. Then, $\Sigma \cup \{ \lnot \varphi \}$ is nontrivial, and can be extended to a maximal nontrivial set $\Sigma '$. By the truth lemma, $\Sigma ' \models \lnot \varphi$ yielding $\Sigma ' \not \models \varphi$. This is the countermodel we were looking for. $\square$

So far, we have showed that Baaz’s results in $KC_\omega$ can be carried over to $TC_\omega$ without much difficulty. This is achieved relatively easily as a consequence of the immediate and effective translation between $KC_\omega$ and $TC_\omega$, and the similarity between the classical modalities and the da Costa negation operator. Such similarities between classical modalities and paraconsistent operators were also addressed in some other work [5, 6].

2.2 Further Results

In this section, we reconsider $TC_\omega$ models in various topological spaces, and investigate how topological properties and $TC_\omega$ models interact. Here, our focus will be separation axioms, regular spaces, and connected spaces. The main motivation behind choosing these structures is the fact that the semantics of the negation operator in $TC_\omega$ deals with the closure (and then indirectly, with the boundary) of the sets. Thus, topological notions that are relevant to the boundary become our main subject in this section.

We also remind the reader that our treatment is by no mean exhaustive. Various other topological, mereotopological, and geometrical notions can further be investigated within the framework of da Costa logics or paraconsistent logics in general. Nevertheless, in this work, we confine ourselves to the aforementioned issues, and leave the rest for future work.

2.2.1 Separation Axioms

Let us first recall some of the well-known separation axioms for topological spaces. Two points are called topologically indistinguishable if both have the same neighborhoods. They are topologically distinguishable if they are not topologically indistinguishable. Indiscrete space (trivial topology) is perhaps the simplest example where any two points are topologically indistinguishable. Moreover, two points are separated if each of the points has a neighborhood which is distinct from the other’s neighborhoods. Two points x, y are distinct if $x \ne y$.

Separation axioms present an interesting perspective to analyze paraconsistent models. Traditionally, paraconsistent logics are known as the logics with truth value gluts as opposed to intuitionistic logics which have truth value gaps. Theory of truth value gluts suggests that some propositions can have multiple (including inconsistent) truth values. Topological models then identifies the superimposed truth values with the intersection of sets that denote the truth and falsity of logical formulas. Separation axioms become relevant when we want to separate the superimposed truth values in order to render the model and the formulas consistent.

Let us now define the separation axioms that we need. A topological space is called

• $\mathbf {T_0}$ if any two distinct points in it are topologically distinguishable,

• $\mathbf {T_1}$ if any two distinct points in it are separated,

• $\mathbf {R_0}$ if any two topologically distinguishable points are separable,

• $\mathbf {T_2}$ if any two distinct points in it are separated by neighborhoods,

• if any two distinct points in it are separated by closed neighborhoods.

While discussing the semantics of $TC_\omega$ above, we made use of the relation $w \in \mathsf {Clo}(v)$ quite often. This relation is called the specialization order: $w \le v$ if and only if $w \in \mathsf {Clo}(v)$. It is a partial order if and only if the space is $\mathbf {T_0}$. In this case, if the relation $\le$ is symmetric, then the space we obtain is $\mathbf {R_0}$. Throughout the paper, we will call a model a $\mathbf {T_x}$-model if its topological space is a $\mathbf {T_x}$ space for

We do not force $TC_\omega$ models to be $\mathbf {T_1}$ models or even $\mathbf {R_0}$ models. Then the natural question is the following: Can we have $TC_\omega$ models which are not even $\mathbf {T_0}$ or $\mathbf {T_1}$?

Proposition 19.2.13

Given a $KC_\omega$ model M, the $TC_\omega$ model $M'$ obtained from M is $\mathbf {T_0}$.

Proof

Given a $KC_\omega$ model M, the specialization order that we defined above, generates a $TC_\omega$ model $M'$. In this case, the topology we obtain in $M'$ is an Alexandroff topology as the specialization order of the Alexandroff topology is precisely the partial order that comes from the Kripke model. Therefore, since the specialization order is a preorder, the space we obtain is $\mathbf {T_0}$, so is $M'$. $\square$

In Proposition 19.2.13, the model $M'$ is proved to be $\mathbf {T_0}$. Therefore, it is worthwhile to note that $M'$ is not necessarily $\mathbf {T_1}$. Alexandroff spaces are $\mathbf {T_1}$ if only if they are discrete—each s having a neighborhood of $\{ s \}$ only [1].

Now, we focus on spaces as the closed sets and closure operator play a central role in paraconsistent semantics. Our main theorem is the following:

Theorem 19.2.14

Let $M = \langle S, \sigma , V, N \rangle$ be a $TC_\omega$ model which admits true contradictions, then N cannot be empty.

Proof

In $TC_\omega$ (and similarly in $KC_\omega$) models, N (or T) function tracks the negated formulas in an ad hoc way. In this fashion, nonemptiness of N means that the model cannot have superimposition of truth values which can produce inconsistencies. Intuitively, this is because of the assumption of the separation axiom. Let us now see the proof.

Let $M = \langle S, \sigma , V, N \rangle$ be a $TC_\omega$ model. Assume N is empty. Let w be a state where we have a true contradiction $\varphi \wedge \lnot \varphi$ for some $\varphi$. Thus, $w \models \varphi$, and moreover, since N is empty, there is $v \in \mathsf {Clo}(w)$ such that $v \not \models \varphi$. Since we are in a space, w and v must be separable. However, since $v \in \mathsf {Clo}(w)$, it means that v is in the intersection of all closed sets in $\sigma$ containing w. Thus, they are not separable by closed neighborhoods. Contradiction. Thus, N cannot be empty, and such a point v cannot exist in a space that admit true contradictions. $\square$

The contrapositive of Theorem 19.2.14 can also be useful, let us specify it here.

Proposition 19.2.15

Let $M = \langle S, \sigma , V, N \rangle$ be a $TC_\omega$ space with true contradictions. If N is empty, then M cannot be

In order to see the correctness of the above proposition in an example, we will construct the following model. Now, under the assumption that N is empty, let us consider a formula $\varphi$ and its negation $\lnot \varphi$. Then, we choose $w, w'$ in a way that $w \in [\varphi ]$ and $w' \in [\lnot \varphi ]$, and also that the only closed sets around w and $w'$ will be $[\varphi ]$ and $[\lnot \varphi ]$, respectively. Let $S = \{ 1, 2, 3 \}$, and $\sigma = \{ \emptyset , S, \{1, 2\}, \{2, 3\}, \{2 \} \}$. Let $[\varphi ] = \{1, 2\}$, and $[\lnot \varphi ] =\{ 2, 3\}$. (Consider the formula $\varphi \wedge \lnot \varphi$ at 2.) Then, observe that the points 1 and 3 are not separable by closed sets. Thus, this model cannot be However, if N was not empty, in an ad hoc way, we would have defined the truth of negated formula $\lnot \varphi$ in a way to overcome this issue by letting $N(2) = \{ \lnot \varphi \}$.

Mortensen, in an earlier paper, investigated the connection between similar separation axioms and paraconsistent theories where he made several observations about discrete spaces, and $\mathbf {T_1}$ and $\mathbf {T_2}$ spaces [19].

Moreover, similar connections can be made between paraconsistent logics, topological semantics, and the topological properties of connectedness and continuity. We refer the reader to [4] where such properties are studied in detail.

2.2.2 Regular Spaces

Regular (open) sets are the sets which are equal to the interior of their closure. They play an important role not only in topology but also in mereotopology where the relationship between parts and the whole is investigated [20].

Even if we do not dwell on it further in this paper, it is important to underline that the algebra of closed sets and the topological models for paraconsistent logic do have the same algebraic structure, they both are co-Heyting algebras. Co-Heyting algebras are duals of Heyting algebras which were first proposed as the algebraic counterpart of intuitionistic logics. Some region-based logics, on the other hand, utilize both Heyting and co-Heyting algebras [18, 22]. From an algebraic perspective, we observe that regular sets play an important role in paraconsistency. Now we will consider the matter from a model theoretical perspective, and focus on $TC_\omega$. We start with definitions.

Definition 19.2.16

Let $\langle S, \sigma \rangle$ be a topology. A subset $X \subseteq S$ is called a regular open set if X is equal to the interior of its closure, namely if $X = \mathsf {Int}(\mathsf {Clo}(X))$. Similarly, a subset $Y \subseteq S$ is called a regular closed set if Y is equal to the closure of its interior, namely if $Y = \mathsf {Clo}(\mathsf {Int}(Y))$. We call a space regular open (closed) if all the open sets (or dually, closed sets) are regular. A model is regular open (closed) if its topological space is regular open (closed).

For example, regular open sets in the standard topology of $\mathbb {R}^2$ are the open sets with no “holes” or “cracks”. Also note that the complement of a regular open is a regular closed and vice versa.

We now observe the following:

Proposition 19.2.17

Let $M = \langle S, \sigma , V, N \rangle$ be a $TC_\omega$ model with discrete topology $\sigma$. If $N=\emptyset$, then we have $w \models \lnot \varphi$ if and only if $w \not \models \varphi$, for all $w \in S$ and for all $\varphi$.

Proof

It is a well-known fact that in a discrete topology every subset is closed (or open dually). In this proof, similar to our earlier remarks for the same issue (such as in the proof of Theorem 19.2.14), we assume that N is empty. Let us see the proof now.

First, we assume that N is empty. Then, let us suppose, for an arbitrary $w \in S$, an arbitrary formula $\varphi$, we have $w \models \lnot \varphi$. Then, by definition, considering the discrete topology and the emptiness of N, we have $w \not \models \varphi$. Converse direction is also similar, and we leave it to the reader. $\square$

Clearly, the converse of the above statement is not necessarily true, as it is very much possible to add “redundant” elements to N to make it nonempty.

2.2.3 Connectedness

A topological space is called connected if it cannot be written as the disjoint union of two open sets. We define connected component as the maximal connected subset of a given space. Moreover, in a connected topological space $\langle S, \sigma \rangle$, the only subsets with empty boundary are S and $\emptyset$. This fact, together with the semantics of the negation, plays an important role in $TC_\omega$.

Proposition 19.2.18

Let $M = \langle S, \sigma , V, N \rangle$ be a $TC_\omega$ model that admits a true contradiction whose extension is in the topology. If the space is disconnected and $|M| > 1$, then N cannot be empty.

Proof

Proof follows from the fact that in disconnected spaces, there are sets with empty boundary other than S itself and the empty set. So, we briefly mention the proof idea here. Let a contradiction $\varphi \wedge \lnot \varphi$ satisfied in the model. Then, in this case, the positive $\varphi$ and negative $\varphi$ conjuncts of the contradiction will lie in the different connected components. However, if N is empty, it means that the extensions of each conjunct is connected via the boundary—which creates the contradiction as the space is assumed to be disconnected. $\square$

Again, the contrapositive of the above theorem can help clarify the matter.

Proposition 19.2.19

If N is empty, and M admits true contradictions whose extensions are in the topology, then M cannot be disconnected.

3 Topological First-Order Models $TC^{*}_{\omega }$

The logic $C_\omega$ can be extended to first-order level by introducing quantifiers, and the resulting first-order da Costa logic is called $C^{*}_\omega$ [7]. In his work, Baaz considered only the propositional case for $KC_\omega$, and did not take the next step to introduce a Kripke semantics for $C^{*}_\omega$. Priest, later on presented a Kripke semantics and tableaux style completeness for first-order da Costa logic [21]. Here, we introduce a topological semantics for $C^{*}_\omega$, and call our system $TC^{*}_\omega$.

First, let us set a piece of notation. For a formula $\varphi$, we abbreviate $\varphi ^{\circ } := \lnot (\varphi \wedge \lnot \varphi )$. Moreover, we let, $\varphi ^{(1)} : = \varphi ^{\circ }$, $\varphi ^{(n)} : = \varphi ^{(n-1)} \wedge (\varphi ^{(n-1)})^{\circ }$ for $2 \le n \le \omega$. We will often abuse the notation, and write $\varphi ^n$ instead of $\varphi ^{(n)}$ for easy reading.

Let us now start with introducing the axioms for $C^{*}_\omega$. The axioms of $C^{*}_\omega$ are the axioms of $C_\omega$ together with the following additional axioms [7].

• 1. $\forall x F(x) \rightarrow F(y)$.

• 2. $F(y) \rightarrow \exists x F(x)$.

• 3. $\forall x (F(x))^{(n)} \rightarrow (\forall x F(x))^{(n)}$ for $n \le \omega$.

• 4. $\forall x (F(x))^{(n)} \rightarrow (\exists x F(x))^{(n)}$ for $n \le \omega$.

• 5. Given F and $F'$, if either one is obtained from the other by replacing bound variables or by suppressing vacuous quantification (without confusion of variables), then $F \leftrightarrow F'$ is an axiom.

The rules of inference are modus ponens, $\varphi \rightarrow F(x) \therefore \varphi \rightarrow \forall x F(x)$, and $F(x) \rightarrow \varphi \therefore \exists x F(x) \rightarrow \varphi$. Based on the given axiomatization, $C^{*}_n$ is finitely trivializable for $n < \omega$ while $C^{*}_\omega$ is not. Also, it is important to note that $C^{*}_0$ is the classical first-order logic.

Our goal now is to give a topological semantics for $C^{*}_\omega$. In order to achieve this, we will make use of denotational semantics akin to Awodey and Kishida’s work on topological first-order classical modal logic. In their work, they used sheaves to express the quantification domain of predicated modal formulas [2]. Their semantics is elegant, and simply explains how we should read predication in a natural way in the case of topological modal models. The use of denotational semantics will also be helpful for $TC^{*}_\omega$ as it presents a quite natural way to handle the non-truth functional behavior of the negation.

We start by introducing $TC^{*}_\omega$ models, and the related denotational interpretation function.

Definition 19.3.1

A first-order topological da Costa model $TC^{*}_\omega$ is given as the tuple $\langle S, D, | \cdot |, N^*, \sigma \rangle$ where S is a nonempty set with topology $\sigma$ on it, $\emptyset \ne D \subseteq S$ is called the domain of individuals, $|\cdot |$ is a denotational interpretation function that assigns denotations in S to formulas, and $N^*$ is the extension of the propositional negation function N to the first-order case defined over S.

Let us now give a brief explanation of $TC^*_{\omega }$ models here. The denotational interpretation function $| \cdot |$ takes formulas (with or without free variables), and returns individuals from S. Domain D, on the other hand, is given to precise the quantification. Similar to first-order classical modal logic, we use the domain set in the definition of the semantics of the quantifiers [11]. Here, we take D as a subset of S, so that we can make use of the topology $\sigma$ defined on S for the objects in the domain. Alternatively, domain D and the topological space S can be taken as disjoint, and there can be defined a homeomorphic map from D to S [2]. Nevertheless, for simplicity, we choose the former. Finally, the function $N^*$ is similar in purpose to the propositional N, and makes the semantics for negation non-truth functional, which we need in da Costa systems.

For variables $x_1, \dots , x_n$ of appropriate arity n in the formula F, the vector $\overline{x}$ is the function that maps all free variables in F to some objects. We denote the denotational interpretation of F with $\overline{x}$ by $| \overline{x}; F |$, which is a tuple in $S^n$. For the formulas with different arity for free variables, we simply adjust the arity of the function $\overline{x}$ for each of its occurrence. The complement of $| \overline{x}; F |$ will be denoted by $| \overline{x}; F |^c$. By a slight abuse of the notation, $|\overline{x}; N^*|$ will denote set of denotations of the formulas returned by $N^*$. Therefore, $|\overline{x}; N^*| : = \bigcup _{F \in N^*} |\overline{x}; F|$.

The variable assignment is denoted by v. The function v assigns objects of the model to the variables present in a logical term, and this construction is a familiar one from first-order logic matching individual atoms with objects in the model. For a formula F, by a slight abuse of notation, v(F) will denote the objects assigned to the variables of F. Moreover, we also define terms following the standard construction in first-order logic.

As we have remarked earlier, da Costa negation, in both propositional and first-order cases, is not truth functional. Note that there are, however, some paraconsistent logics with topological semantics where negation behaves truth functionally [13]. In such systems, the extension of each and every propositional variable is associated with a closed set while this condition is not a requirement in the topological semantics for classical modal logics. The reason for this is that in classical modal logics, only modal formulas are forced to have open or closed extensions. Propositional formulas do not necessarily have such extensions in classical case. Then, the negation in paraconsistent logics with topological semantics is defined as the closure of the complement [13]. The reason for this is quite immediate. While attempting to take the negation of a given formula, the usual way is to consider the set theoretical complement of the extension of the given formula. However, the complement of a closed set (which is the extension of the given formula) may not be closed, thus, may not be in the topology since the topology in question is a closed set topology. Therefore, in order to maintain the closed set topological structure, negation needs to be defined in that way to produce a closed set.

This idea, however, does not work in da Costa logics. For instance, assume that we endorse the aforementioned definition of negation for $TC_\omega ^*$. Namely, consider the following definition for the denotational interpretation of the negated formula $\lnot F$ with respect to variables $\overline{x}$: $| \overline{x}; \lnot F | = \mathsf {Clo}( S^n - |\overline{x}; F |)$.

A closer inspection immediately reveals that the above semantics for negation is indeed truth functional. In order to see the failure of this definition within the context of $TC^*_{\omega }$, consider the logically equivalent formulas $\lnot p$ and $\lnot (p \wedge p)$. Based on the proposed semantics, the denotations of $\lnot p$ and $\lnot (p \wedge p)$ are necessarily the same. However, in da Costa systems, recall that the extensions of both $\lnot p$ and $\lnot (p \wedge p)$ are not necessarily identical. Therefore, the proposed (standard) topological semantics for paraconsistency does not work for da Costa systems.

Here, we suggest a working topological semantics for $C_\omega ^*$.

• $| \overline{x}; c | \in S$ for a constant c,

• $| \overline{x}; F | \subseteq S^n$ for a n-place predicate F,

  In particular, take an atomic sentence $F(t_1, \dots , t_n)$ with terms $t_i$ for $1 \le i \le n$. If $d_1, \dots , d_n$ are the evaluation of the terms $t_1, \dots , t_n$ under the variable assignment v, then we have the following in S: $|\overline{t}; F(t_1, \dots , t_n)| = v(F)(v(t_1), \dots v(t_n))$,

• $| \overline{x}; F \wedge G | = | \overline{x}; F | \cap |\overline{x}; G |$,

• $| \overline{x}; F \vee G | = | \overline{x}; F | \cup |\overline{x}; G |$,

• $| \overline{x}; \lnot F | = |\overline{x}; N^*| \cup \mathsf {Clo}(| \overline{x}; F |^c)$,

• $| \overline{x}; \exists y F | = \bigcup _{d \in D} |\overline{d}, d; F|$ where $\overline{d} \in D^n$,

• $| \overline{x}; \forall y F | = \bigcap _{d \in D} |\overline{d}, d; F|$ where $\overline{d} \in D^n$.

We can furthermore define the truth in a $TC^*_{\omega }$ model M. We say that a formula $F(\overline{x})$ is true in the denotational interpretation $| \cdot |$, if $|\overline{x}; F| = S$.

Let us now explicate the given semantics a bit further. The denotational semantics for the negation ensures that the negated denotation is among the formulas determined by $N^*$ function. So, $|\overline{x}; N^*|$ can be thought of as the collection of the denotations of the formulas returned by $N^*$. The closure operator $\mathsf {Clo}$ in the definition functions as the classical (or standard) part of the semantics. Similarly, the denotational semantics for the quantifier varies over the objects in the domain even though the denotation of the formula in question will eventually be in S.

As an illustration, let us consider the denotational semantics of the formula $\exists y (\lnot F \wedge F)$ with a variable x.

$$\begin{aligned} |x; \exists y (\lnot F \wedge F)|&= \bigcup _{d \in D} |d, d'; (\lnot F \wedge F)| \\&= \bigcup _{d \in D} \{ |d, d'; \lnot F| \cap |d,d'; F| \} \\&= \bigcup _{d \in D} \{ ( |d, d'; N^*| \cup \mathsf {Clo}(|d, d'; F|^c )) \cap |d,d'; F| \} \\&= \bigcup _{d \in D} \{ (|d, d'; N^*| \cap |d,d'; F|) \cup \partial (|d, d'; F|) \} \end{aligned}$$

where $\partial (\cdot )$ is the topological boundary operator. In this example, the individuals $d \in D$ which exist and satisfy the contradictory formula $F \wedge \lnot F$ lie in the boundary of the denotation of F, or in the intersection of the denotation of F and the denotation of the formulas returned by $N^*$.

Also, it is worth noting that quantified De Morgan’s laws are not valid in da Costa systems—even if the set theoretical De Morgan’s laws hold [9]. As an illustration, we consider the following classical first-order logical equality $\forall x Fx \leftrightarrow \lnot \exists x \lnot F x$. Let us first see the denotation of $\lnot \exists x \lnot F x$.

$$\begin{aligned} |x; \lnot \exists x \lnot Fx |&= |d; N^*| \cup \mathsf {Clo}(|d; \exists x \lnot Fx|^c)\\&= |d; N^*| \cup \mathsf {Clo}((\cup _{d \in D} |d; \lnot F |)^c)\\&= |d; N^*| \cup \mathsf {Clo}((\cup _{d \in D} (|d;N^*| \cup \mathsf {Clo}( |d; F |)^c))^c)\\ \end{aligned}$$

Therefore, if $|d; N^*|$ is not empty, we cannot generally obtain $\bigcap _{d \in D} |d; F|$, which is the denotation of $\forall x F x$. Other quantified De Morgan laws can be given similar arguments [10].

Soundness of the axioms of $TC^{*}_\omega$ with respect to the given semantics above is a straightforward symbolic manipulation. However, we will still consider some of the axioms which are unique to da Costa systems, and show their soundness.

Now, as the first case, we take the following formula as an instantiation of the axiom scheme (3) with $n=1$.

$$\forall x F^1 x \rightarrow (\forall x Fx)^{1}$$

In order to have an idea of what to expect, let us first note the following logical equalities.

$$\forall x F^1 x = \forall x F^\circ x = \forall x \lnot (F x \wedge \lnot F x)$$

and

$$(\forall x Fx)^1 = (\forall x Fx)^\circ = \lnot (\forall x Fx \wedge \lnot \forall x Fx).$$

So let us now assume, $\forall x F^1 x$, which is equivalent to $\forall x . \lnot (F x \wedge \lnot F x)$. Then, we have the following:

$$\begin{aligned} |x; \forall x . F^1 x|&= |x; \forall x . \lnot (F x \wedge \lnot F x)|\\&= \bigcap _{d \in D} |d; \lnot (Fx \wedge \lnot Fx)|\\ {}&= \bigcap _{d \in D} \{ |d; N^*| \cup \mathsf {Clo}(|d; Fx \wedge \lnot Fx|^c) \} \\&= \bigcap _{d \in D} \{ |d; N^*| \cup \mathsf {Clo}((|d; Fx| \cap |d; \lnot Fx|)^c) \} \\&= \bigcap _{d \in D} \{ |d; N^*| \cup \mathsf {Clo}((|d; Fx| \cap (|d; N^*| \cup \mathsf {Clo}(|d; Fx|^c)))^c) \} \\&= \bigcap _{d \in D} \{ |d; N^*| \cup \mathsf {Clo}((|d; Fx| \cap |d; N^*|) \cup (|d; Fx| \cap \mathsf {Clo}(|d; Fx|^c)))^c) \} \\&\text { (as intersection operation commutes with closure operator)} \\&= \bigcap _{d \in D} |d; N^*| \cup \cap _{d \in D} \mathsf {Clo}(|d; Fx| \cap |d; N^*|)^c \cup (|d; Fx| \cap \mathsf {Clo}(|d; Fx|^c))^c)) \\&= \bigcap _{d \in D} |d; N^*| \cup \mathsf {Clo}(\cap _{d \in D}|d; Fx| \cap |d; N^*|)^c \cup \cap _{d \in D} (|d; Fx| \cap \mathsf {Clo}(|d; Fx|^c))^c)) \\&\text { (as the interior of a set is its subset)} \\&\subseteq |d; N^*| \cup \mathsf {Clo}(\cap _{d \in D}|d; Fx| )^c \cup (\cap _{d \in D} (|d; Fx| \cap \mathsf {Clo}(|d; Fx|^c))^c)) \\&\subseteq |d; N^*| \cup \mathsf {Clo}(\cap _{d \in D}|d; Fx| )^c \cup ((|d; Fx| \cap \mathsf {Clo}\cap _{d \in D}(|d; Fx|^c))^c)) \\&\subseteq |d; N^*| \cup \mathsf {Clo}(\cap _{d \in D}|d; Fx| \cap ((|d; Fx| \cap \mathsf {Clo}\cap _{d \in D}(|d; Fx|^c))) \\&\subseteq \lnot (\forall x F x \wedge \lnot \forall x F x) \\ {}&\subseteq (\forall x F x)^1 \end{aligned}$$

Thus, we obtain $\forall x F^1 x \rightarrow (\forall x Fx)^{1}$.

As the second case, let us take the axiom scheme (4) instantiated with $n=1$. Thus, we consider the following implication,

$$\forall x F^1 x \rightarrow (\exists x Fx)^1$$

Now, below is what follows from the above statement.

$$\begin{aligned} |x; \forall x . F^1 x|&= |x; \forall x . \lnot (F x \wedge \lnot F x)|\\&= \bigcap _{d \in D} \{ | d; N^* | \cup \mathsf {Clo}(|d; Fx \wedge \lnot Fx|^c) \} \\&= \bigcap _{d \in D} \{ |d; N^*| \cup \mathsf {Clo}(|d; Fx| \cap |d; \lnot Fx|)^c \} \\&= \bigcap _{d \in D} \{ |d; N^*| \cup \mathsf {Clo}(|d; Fx|^c \cup |d; \lnot Fx|^c) \} \\&= \bigcap _{d \in D} \{ |d; N^*| \cup \mathsf {Clo}(|d; Fx|^c \cup (|d; N^*|\cup \mathsf {Clo}(|d; Fx|^c))^c)) \}\\&= \bigcap _{d \in D} \{ |d; N^*| \cup \mathsf {Clo}(|d; Fx|^c \cup (|d; N^*|^c \cap \mathsf {Int}(|d; Fx|))) \}\\&\subseteq \bigcap _{d \in D} |d; N^*| \cup \mathsf {Clo}(\cap _{d \in D} |d; Fx|^c \cup (\cap _{d \in D} |d; N^*|^c \cap \mathsf {Int}(\cap _{d \in D}|d; Fx|)))\\&\subseteq |d; N^*| \cup \mathsf {Clo}(\cap _{d \in D}|d; Fx|^c \cup (|d;N^*|^c \cap \mathsf {Int}(\cup _{d \in D} |d;F|)))\\&\text {by set theoretical De Morgan's Laws} \\&\subseteq |d; N^*| \cup \mathsf {Clo}(\cup _{d \in D}|d; Fx| \cap (|d;N^*| \cup \mathsf {Clo}(\cup _{d \in D} |d;F|^c)^c))\\&\subseteq |d; N^*| \cup \mathsf {Clo}((\exists x F x \wedge \lnot \exists x F x)^c)\\&\subseteq \lnot (\exists x F x \wedge \lnot \exists x F x) \\&\subseteq (\exists x F x)^1 \end{aligned}$$

Finally, we obtain $\forall x F^1 x \rightarrow (\exists x Fx)^1$.

The remaining axioms can also be given rather straightforward arguments for their soundness, thus we leave them to the reader.

$$ * $$

This was soundness. However, we still do not have a completeness result (or lack thereof) for $TC^{*}_\omega$. We leave it for further work.