{'fraction_non_alphanumeric': 0.05843551454817693, 'fraction_numerical': 0.011492857431912914, 'mean_word_length': 3.7541362062331665, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 5, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Leibniz's law and paraconsistent models of ZFC

In this paper, we present full models for some Paraconsistent Set Theories (PSTs). These models are built over Fidel semantics where they are specific first-order structures in the sense of Model Theory. These structures are known as F-structures in the literature and they are not algebras in the universal algebra sense. We demonstrate how is possible to present paraconsistent models for ZFC for any of PSTs studied in this paper, by adapting the proofs given on the celebrated John Lane Bell's books; in general, we adapt the proofs in the mentioned book throughout the work.


Introduction
Paraconsistency is the study of logic systems having a negation ¬ which is not explosive; that is, there exist formulas α and β in the language of the logic such that β is not derivable from the contradictory set {α, ¬α}. These systems are typically called non-trivial systems and in this note we will work with this notion of paraconsistency which is the most accepted for the logicians.
In the 1950's, Nelson logic (even also called N3), was formulated by Nelson and Markov as a result of certain philosophical objections to the intuitionistic negation. The criticism concerned its disadvantageous non-constructive property, namely that the derivability of the formula ¬(α∧ β) in an intuitionistic propositional calculus does not imply that at least one of the formulas ¬α, ¬β is derivable. A paraconsistent version of Nelson logic was first introduced in [1], where the authors observed that the weaker system obtained from Nelson logic by deleting the axiom schema α → (¬α → β) could be used to reason under inconsistency without incurring in a trivial logic. Semantics for this paraconsistent version of Nelson logic have been studied by Odintsov in [19], who calls the logic N4, in terms of what is known in the literature as Fidel structures and twist-structures.
On the other hand, the C-systems C n (c < ω) and C ω are among the best-known contributions of da Costa and his collaborators. In particular, for C n is possible to define a new operator • where it plays a role of recovering the classical theorems. These logics are known as Logics of Formal Inconsistency, see for instance [10,16]. Both C n (n < ω) and C ω are nonalgebrizable logics with Blok-Pigozzi method, see [18]. This was one of the reasons why these systems remained without semantics for several years. For every C n , bi-valuation semantics was first presented by da Costa and Alves exhibiting a soundness and completeness Theorem, [9]. On the other hand, Fidel presented semantics for both C n (c < ω) and C ω through introducing an algebraic-relational structures that would bear his name; this idea was in fact based on a generalization of Lindenbaum-Tarski process, [12]. Recently, Fidel semantics for a first-order logic was presented in [13]; moreover, it was displayed the relation with da Costa and Alves's bi-valuation semantics through a Representation Theorem. Other paraconsistent logics which are not algebraizable were introduced recently by means of degree-preserving construction in the paper [10,11,14].
On the other hand, since both C n and N4 can be axiomatized as an extension of the intuitionistic positive caculus; we can present F -structures for them based on Boolean and Heyting algebras.
Going to the central issue of this paper, recall that Boolean-valued models were introduced with the intention to simply the Forcing method by Vopȇnka. Afterwards, Scott, Solovay and Vopȇnka in 1965 proposed to present models for Zermelo-Fraenkel Set Theory (ZF); an excellent exposition of the theory can be found in the Bell's book, [4]. This idea allowed obtaining models for Intuitionistic version of Zermelo-Fraenkel Set Theory through working Heyting-valued models, [5]. Using Boolean-valued models, it is possible to see that the axiom of Choice is validated over them; i.e., it is commonly said that Boolean-valued mode are models ZFC.
In this paper, we construct F -structures valued models as adapting the machinery developed to Boolean and Heyting case. With these new structures, we are able to prove that every axiom of ZF is validated over them; besides, we discuss the central rôle of Leibniz law in the proof. These facts allow us to consider paraconistent set theories over both (paraconsistent) Nelson's and da Costa's logics, using the propositional axioms for first-order formulas and set-theoretic axioms of Zermelo-Fraenkel. Moreover, we built bi-valuation valued models and prove that they are good enough to get paraconsistent model of ZFC.

Preliminaries
To present these logics, we first display some notation useful for the rest of the paper. For a given logic X, let us consider the signature Σ = {∧, ∨, →, ¬} for X, and the language Fm, or set of formulas, over the denumerable set of variable V ar. In the following, we will consider several logics under the same signature Σ and X represents any of them. Recall now that the intuitionistic positive caculus (Int + ) may be axiomatize by the following schemas and and the rule Modus Ponens: Paraconsistent Nelson's logic, N4, is defined as an extension of Int + adding the following schemas: Axioms To define the logic N3 , we only add the following axiom schema to N4 The logic C ω is defined through adding the followings schemas to Int + (C1) α ∨ ¬α, Now, the logic C 1 is defined by adding to the axioms set of C ω and the following axiom schemas: The notion of derivation of a formula α on any logic X is defined as usual. We say that α is derivable from Γ in X, denoted by Γ ⊢ α, if there exists a derivation of α from Γ in X. If Γ = ∅ we denote ⊢ α; in this case, we say that α is a theorem of X.

F -structures for N4
Now, recall that an algebra A = A, ∨, ∧, →, 0, 1 is said to be a Heyting algebra if the reduct A, ∨, ∧, 0, 1 is a bounded distributive lattice and for any a, b ∈ A the value of a → b is a pseudocomplement of a with respect to b; i.e., the greatest element of the set {z ∈ A : a ∧ c ≤ b}. As a more general case, we say that B = B, ∨, ∧, →, 1 is a generalized Heyting algebra if B, ∨, ∧, 1 is a distributive lattice with the greatest element 1 and → is defied as Heyting case. This last class of algebras is called Relatively pseudo-complemented lattices in [20,Chapter IV] and Implicative Lattices in [19].
Recall that a F -structure for N4 is a system A, {N x } x∈A where A is a generalized Heyting algebra and {N x } x∈A is a family of sets of A such that the following conditions hold: (i) for any x ∈ A, N x = ∅, (ii) for any x, y ∈ A, x ′ ∈ N x and y ′ ∈ N y , the following relations hold x ′ ∨ y ′ ∈ N x∧y and For the sake of simplicity, we will write sometimes A, N instead of A, {N x } x∈A . Besides, we call the F -structures for N4 by N4-structures. As example of N4-structure, we can take a generalized Heyting algebra A and the set N s x = A for every x ∈ A. The structure A, {N s x } x∈A will be said to be a saturated one; these saturated structures are essential to prove the Adequacy Theorem.
For a given set of formulas Γ in N4, we will consider the binary relation between formulas as follows: Bearing in mind the positive axioms of N4, (A1) to (A8), we have that ≡ Γ is a congruence with respect to the connectives ∨, ∧ and →. With |α| Γ we denote the class of α under ≡ Γ and L N4 denotes the set of all classes. We can define the operations ∨, ∧ and → on L N4 as follows: |α#β| Γ = |α#β| Γ with # ∈ {∧, ∨, →}. Thus, it is clear that L N4 , ∧, ∨, →, 1 is a generalized Heyting algebra with the greatest element 1 = |α → α| Γ . To extend the latter algebra to N4structure, let us define the set N |α| for each formula α as follows: It is not hard to see that L N4 , {N |α| Γ } α∈Fm is a N4-structure that we will call Lindenbaum structure.
Besides, we say that a function v : Fm → A, {N x } x∈A is a N4-valuation if the following conditions hold: It is not hard to see that if we take a N4-valuation for atomic formulas, it works well on formulas with more complexity as we can see in [19]. For us, a formula α will be semantically valid from Γ if for every N4-structure and every valuation v on the structure, the condition v(β) = 1 for every β ∈ Γ implies v(α) = 1. In this case, we denote Γ α.
We may define a semantics consequence relation as follow: Γ α iff for every valuation v, if v(Γ) = {1}, then v(α) = 1. Thus, a strong version of soundness and completeness Theorem for C 1 with respect to this semantics was proven in [9,Lemma 8]. It is worth mentioning that it is not hard to see that, taking into account to conditions (bv1) to( bv3), every bi-valuation v : Fm → {0, 1} can be seen as homomorphism from Fm into 2, where 2 is a two-element Boolean algebra. Conversely, every homomorphism from Fm into 2 that verifies (bv4) to (vb5) is a bi-valuation.

F -structures for C 1
It is possible to present other kind of semantics for C 1 through F -structures, see, for instance, [18]. Recall that a F -structure for A is a Boolean algebra and {N x , O x } x∈A is a family of sets of A such that the following conditions hold: (iii) for every x ∈ A and every y ∈ N x , there is z ∈ O x such that x ∧ y ∧ z = 0.
As on the case of N4, we write A, N, O instead of A, {N x } x∈A , {O x } x∈A . We will next consider the set of formulas L C 1 and taking again (A1) to (A8), we have that ≡ Γ is a congruence with respect to the connectives ∨, ∧ and →. With |α| Γ where ≡ Γ is defined as N4 case. Analogously to the case N4, we have that Besides, we say that a function v : Fm → A, {N x } x∈A is a C 1 -valuation if the following conditions hold: For us, a formula α will be semantically valid if every C 1 -structure A, N, O and every valuation v on the structure, then condition v(α) = 1 holds; and in this case, we denote α.
Clearly, it is possible to prove a strong version of the last Theorem in a similar way that was done in [18, Section 6] for non-algebraizable extensions of C ω .

F -structures for C ω
Recall that a F -structure for C ω ( C ω -structure) is a system A, {N x } x∈A where A is a Boolean algebra and {N x } x∈A is a family of sets of A such that the following conditions hold: Besides, we say that a function v : A formula α is said to semantically consequence from Γ if every C ω -structure A, N and every valuation v on the structure, then condition v(α) = 1 holds; and in this case, we denote α. Moreover, we write Γ α if every C ω -structure A, N and every valuation v on the structure, the condition v(β) = 1 for every β ∈ Γ implies v(α) = 1.

Zermelo-Fraenkel Set Theory
In this part of the paper, we will present Paraconsistent Set Theories build over paraconsistent propositional logic expressing its axioms on a suitable first-order version for Set Theory. We start by considering any logic X over the first-order signature Θ ω which contains an equality predicate ≈ and a binary predicate ∈. The system ZF X is the first-order system obtained from the logic X over Θ ω by adding the following set-theoretic axiom schemas: The set satisfying this axiom is, by extensionality, unique and we refer to it with notation ∅.
From union and pairing and extensionality, we can note by y + the unique set y ∪ {y}.
These axioms are typically used to define Zermelo-Fraenkel Set Theory (for short ZF), see [4]. In this paper, we will focus on the task of presenting models for ZF N4 , ZF N3 , ZF C 1 and ZF Cω .
Bell proved that (AC) implies Law of Excluded Middle (LEM) then (AC) does not hold on Intuitionistic Zermelo Fraenkel set theory where (AC) is very weaker, [3,5]. The same occurs on ZF N4 (ZF N3 ) because N4 (N3) does not hold LEM. In contrast, the systems ZF C 1 and ZF Cω are compatible on LEM.

Leibniz's law and its models
In this section, we shall analyze the minimal conditions for models constructed over a Heyting (or Boole) algebra that we need to prove that several Zermelo-Fraenkel's set-theoretic axioms are valid in these models. Now, we fix a model of set theory V and a completed Heyting algebra A. Let us construct a universe of names by transfinite recursion: The class V A is called the algebraic-valued model over A. Let us observe that we only need the set A in order to define V ξ A,N . By L ∈ , we denote the first-order language of set theory which consists of only the propositional connectives {→, ∧, ∨} and two binary predicates ∈ and ≈. We can expand this language by adding all the elements of V A,N ; the expanded language we will denote L A,N . For this construction of models we also have Induction principles as the Boolean and Intuitionistic case, [4]. Now, we shall consider a minimal requirement for defining value of truth of formulas in order to prove some of set-theoretic axioms of ZF are valid. Now, for a given completed Heyting algebra A, the mapping [[·]] A : L A → A is defined as follow: ] is called the truth-value of the sentence ϕ in the language L A in the algebraic-valued model over A. Besides, the condition (HV3) is know as Leibniz's law. This condition will be used in the rest of the section.

Lemma 3.2 For a given complete Heyting algebra
We will adopt the following notation, for every formula ϕ(x) and every u ∈ V A,N : ∃x ∈ uϕ(x) = ∃x(x ∈ u ∧ ϕ(x)) and ∀x ∈ uϕ(x) = ∀x(x ∈ u → ϕ(x)). Now, we recall that for a given Heyting algebra A we have the following properties hold: Thus, we have the following Lemma 3.3 Let A be a complete Heyting algebra, for every formula ϕ(x) and every On the other hand, Form the latter and (P1), we can conclude that

Definition 3.4 Let A be a complete Heyting algebra. Given collection of sets {u
The following result is known as Mixing Lemma and its proof is exactly the same for intuitionistic case because it is an assertion about positive formulas.
Proof. Since A is a set, then the collection X = {[[ψ(u)]] A : u ∈ V A } is also a set. By the Axiom of Choice, there is an ordinal α and a set {u ζ : which completes the proof. Now, given a complete Heyting A ′ of A, we have the associated models V A ′ and V A . Then, it is easy to see that On the other hand, we say that a formula ψ is restricted if all quantifiers are of the form ∃y ∈ x or ∀y ∈ x, then we have Lemma 3.7 For any complete Heyting algebra A ′ of A and any restricted negation-free formula Next, we are going to consider the Boolean algebra 2 = ({0, 1}, ∧, ∨, ¬, 0, 1) and the natural mapping· : V A → V 2 defined byû = { v, 1 : v ∈ u}. This is well defined by recursion on v ∈ dom(u). Then, we have the following lemma holds: (iv) for any formula negation-free formula ψ(x 1 , · · · , x n ) and any x 1 , · · · , x n ∈ V, we have ψ(x 1 , · · · , x n ) ↔ V 2 ψ(x 1 , · · · ,x n ). Moreover for any restricted negation-free formula The proof of the last theorem is the same for intuitionistic case because we consider restricted negation-free formulas and it will be used to prove the validity of axiom Infinity.

Validating axioms
As for now, we are going to prove the validity of several set-theoretical axioms of ZF. Therefore, let us consider a fix model V A . Then:

Pairing
Let u, v ∈ V A and consider the function

Union
Given u ∈ V A and consider that function

Separation
Given u ∈ V A and suppose dom(w) = dom(u) and w( Besides,

Collection
Given u ∈ V A and x ∈ dom(u) there exists by Axiom of Choice some ordinal α x such that

Paraconsistent Nelson's Set Theory
Now, we construct the class V A,N of N4-structure-valued model over A, N following the methodology developed for Heyting-valued models. By L ∈ , we denote the first-order language of set theory which consists of the propositional connectives {→, ∧, ∨, ¬} of the N4 and two binary predicates ∈ and ≈. We can expand this language by adding all the elements of V A,N ; the expanded language we will denote L A,N . Now, we will define a valuation by induction on the complexity of a closed formula in L A,N . Then, for a given complete and saturated N4-structure A, N , the mapping [[·]] A,N : L A,N → A, N is defined as follows: The following fact can be checked by induction on the structure of formulas.
In the following Theorem, we will consider a complete and saturated N4-structure A, N , then A is indeed a complete Heyting algebra. Moreover, for every formula ψ, we have that [[ψ]] A,N belongs to A. From the latter and taking into account the proofs displayed on Section 3.1, we have proven this Theorem: Thus, (Extensionality) is held. Now, assume u ∈ V A,N and suppose w a function such that dom(w) = {f : dom(u) → A : f function} and w(x) = [[∀y ∈ x(y ∈ u)]] A,N . Therefore, On the other hand, given v ∈ V A,N and consider the function a such that dom(a) = dom(u) and Since a(y) ≤ [[y ∈ u]] A,N for every y ∈ dom(a) then we have [[∀y ∈ a(y ∈ u)]] A,N = 1. Now by construction we have that a ∈ dom(w) and so, It is clear that we can be translated the proof on ZF N4 to the case of ZF N3 . So, we have the following Corollary:

Leibniz's law and Paraconsistent Set Theory ZF N4
In the next, we will present some remarks for the Paraconsistent Set Theory ZF N4 . From the condition (N4-8) allows us to prove Leibniz law and this plays a fundamental role in the proof of Theorems 4.4 and 4.5, we will a display an example where the law does not hold. Let us start by considering the following three-element-chain Heyting algebra with a special negation, H ¬ 3 , give by Table 1  let ψ(x) be the formula "w ∈ x" where x is a free variable.
, and therefore the Leibniz s law is not verified. This fact leads to the impossibility to prove the validity of at least one axiom of ZF for formulas with negation; indeed, if we take the formula φ(x) := ¬ψ(x), then it is not hard to see that the axiom "Separation" is not valid. It is clear that the matrix H ¬ 3 , {1} validate all axioms of N4 Now, we will present the study of the formula given above, but now using a saturated N4- 1 2 , 1} and → is given in Table 1. Now, let's now consider the model V N 3 and w ∈ V N 3 , and let ψ(x) be the formula "w ∈ x" where x is a free variable. Then, we have the following possibilities: . Thus, the model V N 3 verifies Leibniz's law and it is a paraconsistent model. We do not know which is the real value of the valuation of any formula with negation but we will know that it is the right one.

Bi-valuation valued models for C 1 Paraconsistent Set Theory
Now, we construct the class V 2 of bi-valuation valued model following Section 3 but now using the Boolean algebra 2. By L ∈ , we denote the first-order language of set theory which consists of the propositional connectives {→, ∧, ∨, ¬} of the C 1 and two binary predicates ∈ and ≈. Recall that C 1 has a non-primitive connective • and we want to consider formulas with this connective on ZF C 1 . Let us now expand this language by adding all the elements of V 2 ; the expanded language we will denote L 2 . We will now define a valuation by induction on the complexity of a closed formula in L 2 . Then, the mapping [[·]] 2 : L 2 → 2 is defined as follows: [[ϕ]] 2 is called the truth-value of the sentence ϕ in the language L 2 in the bi-valuation valued mode over 2. Now, we say that a sentence ϕ in the language L 2 is said to be valid in V 2 , which is denoted by The following Lemma will be used in the rest of section, an the proof is the same to the Boolean case as we will see: The following properties true in V 2 : Proof.
Then, if ψ is the form ¬φ or •φ, then applying (BV8) we have the condition (vi) holds.
Lemma 5.2 Let φ(x) be a formula such that V 2 ∃xφ(x). Then, (ii) If ψ(x) is a formula such that for any u ∈ V 2 , the condition V 2 φ(u) implies V 2 ψ(u), Proof. (i): Applying Theorem 3.6 to the Boolean algebra 2, we obtain that there is On the other hand, applying Mixing Lemma (Lemma 3.5) for the Form the latter and (iv) Next, we will define the notion of core of a element of V 2 .
Lemma 5.4 Any u ∈ V 2 has a core.

Proof.
Let us consider a  2 , by Lemma 5.1 (iv). So, x ∈ C as desired.
Corollary 5.5 Suppose that u ∈ V 2 is such that V 2 u = ∅ and let v be a core for u. Then for any Proof. It immediately follows from Lemma 5.2 and taking φ(x):= "x ∈ u".
In order to prove that the Axiom of Choice is true in V 2 , it is enough to verify the settheoretically equivalent principle Zorn's Lemma. Recall now that a partially ordered set X is said to be inductive if every chain in X has upper bounds. Zorn's Lemma states that any non-empty inductive partially ordered set has a maximal element.

Lemma 5.6 Zorn's Lemma is true in
Proof. Let x, ≤ x ∈ V 2 where x is a set and ≤ x an ordered relation on x. Let us now suppose the formula φ(x) is given by "(x, ≤ x ) is a non-empty inductive partially ordered set" and the formula ψ(x) given by "(x, ≤ x ) has a maximal element".
From Lemma 5.2(ii), we only prove that: there is u ∈ V 2 such that the condition V 2 φ(u) implies V 2 ψ(u). Indeed, let us suppose y is a core for x and take the relation ≤ y on y defined by "z ≤ y z ′ iff [[z ≤ X z ′ ]] = 1" for z, z ′ ∈ y. It is not hard to see that ≤ y is partial ordering on y. We will prove that every chain in y has upper bound in it. Indeed, let C a chain in y and take C ′ = { c, 1 : c ∈ C}. Then, it is clear that V 2 C ′ is a chain in x. From the latter and Theorem 3.6 applyied to 2, we have that there is u ∈ V 2 such that V 2 u is a upper bound for C ′ in x. Taking w ∈ y such that [[w ≈ u]] 2 = 1. Thus, w is an upper bound for C in y. For every Therefore, x ≤ y w and then y is inductive. By Zorn's Lemma in V 2 , y has maximal element c. We claim [[c ∈ x]] 2 = 1 and V 2 c is a maximal element of x. Indeed, let us take t ∈ V 2 and apply Corollary 5.5, there is z ∈ y such that  It is clear that for all u ∈ V 2 and every formula φ(x), we can always take [[¬ψ(u)]] 2 = 1 and [[•ψ(u)]] 2 = 0, it is possible to see that Leibniz law is hold. These conditions work perfectly for induction over the complexity of the formula; and more interestingly, V 2 is paraconsistent. To see this, it is enough to take the formula φ(x) := x ≈ x. So, V 2 is a paraconsistent of ZFC.
6 F -structure valued models for C 1 Paraconsistent Set Theory In this section, we will construct the class V A,N,O of C 1 -structure valued model over A, N, O following the methodology developed for Heyting-valued models. By L ∈ , we denote the firstorder language of set theory which consists of the propositional connectives {→, ∧, ∨, ¬} of the C 1 and two binary predicates ∈ and ≈. As it was done in Section 5, we will consider formulas with •. But clearly, taking the language {→, ∧, ∨, ¬} for our system, it works perfectly with formulas with • because •α = ¬(α ∧ ¬α). We can expand this language by adding all the elements of V A,N ; the expanded language we will denote L A,N,O . Now, we will define a valuation by induction on the complexity of a closed formula in L The following Lemma can be proved in a similar way to Lemma 5.1 of Section 5. Taking in mind the proofs of Section 5, particularly, Lemmas 5.2 and 5.4, Collary 5.5 and Lemma 5.6. Now, replacing 2 for an every C 1 -structure A, N, O , we have proved the following Theorem: Al the proofs given in this section can be adapted easily to the context of da Costa's C n and the Logics of Formal Inconsistency, [6].
6.1 F -structure valued models for ZF Cω Under the same consideration to C 1 , we can present the F -structure valued models for ZF Cω . But now the mapping [[·]] A,N : L A,N → A, N is defined from (C 1 -1) to (C 1 -4), (C 1 -7) and (C 1 -8). Then, the following Theorem can be proved analogously to Corollary 4.6: In the book [3, pag. 70], it was presented a proof that Zorn's Lemma is valid on every Heyting-valued models. The form of the this Lemma, which is taken in this book, is in fact is stronger version but still strong enough to prove (AC). Adapting the proofs for intuitionistic case and using Leibniz's law, we have proved the following Lemma.

Conclusions and future works
The problem of independence of Continuum Hypothesis (HC) from ZF Cω can be treated using Boolean-valued models. It is clear that Boolean-valued models validate the axioms of C ω ; and, the independence problem is one of the meta-theory of the system. So, the classical proof could be used to see that (HC) is independent of ZF Cω . The paraconsistent view of these affairs will be part of our future investigation; moreover, we are interested developing a technique obtain a paraconsistent forcing.. In particular, we will interested on paraconsistent set theories where Boolean-valued models are not models of these theories.
On the other hand, in this note we have presented some paraconsistent set theories where the models validate Choice Axiom (CA). In this setting, we think the problem of the independence in different PSTs is very interesting.