{'fraction_non_alphanumeric': 0.05821950070654734, 'fraction_numerical': 0.007395195478097033, 'mean_word_length': 3.9066327709729607, 'pattern_counts': {'":': 0, '<': 1, '<?xml version=': 0, '>': 1, '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}}
On Strongly First-Order Dependencies

We prove that the expressive power of first-order logic with team semantics plus contradictory negation does not rise beyond that of first-order logic (with respect to sentences), and that the totality atoms of arity k +1 are not definable in terms of the totality atoms of arity k. We furthermore prove that all first-order nullary and unary dependencies are strongly first order, in the sense that they do not increase the expressive power of first order logic if added to it.


Introduction
In the last few years, team semantics [14,18] has proved itself to be a very powerful theoretical framework for the study of dependency notions and their interaction; and, furthermore, some intriguing potential applications of team semantics in the areas of belief representation [6,8], social choice and physics [2] and database theory [15] have been noticed.
As a natural generalization of Tarski's semantics to the case of multiple assignments, team semantics allows to extend first-order logic in novel ways, in particular by adding to it dependency atoms that specify complex patterns of dependence and independence between variables; and much of the research in the area so far has been dedicated to the comparison of the logics thus obtained.
Many of these logics are much stronger than first-order logic itself -for instance, dependence logic is as expressive as the existential fragment of second-order logic [18], and inclusion logic is as expressive as greatest fixed point logic [11] -but this needs not be the case. Indeed, as shown in [9], many nontrivial dependency notions, such as for instance the negations of functional dependence, inclusion, exclusion, and conditional independence, are strongly first-order in the sense that they do not increase the expressive power of first-order logic if added to it. The totality atoms, which assert that a certain tuple of variables takes all possible values in a team, are an especially interesting example of a strongly first-order dependency, and in this work we will study them in some depth.
It is important to emphasize here that these strongly first-order dependencies, despite not increasing the expressive power of first-order logic sentences, cannot be disposed of: even though every sentence containing them (but not other, stronger dependencies) is logically equivalent to some first-order sentence, the satisfaction conditions of formulas containing them are not in general equivalent to the satisfaction conditions of any first-order formula with respect to team semantics. This disparity between the behaviour of formulas and that of sentences is one of the most intriguing phenomena of team semantics.
The study of team semantics (and, in particular, of strongly first-order dependencies) can thus be seen as an attempt to investigate the nature of the boundary between first-and second-order logic; and, from a more practical point of view, dependencies which are strongly first-order are eminently treatable in that they do not increase the complexity of the logic.
The purpose of this work is to further investigate the properties of strongly firstorder dependencies and -more in general -of team semantics-based extensions of first-order logic whose expressive power is no greater than that of first-order logic proper. In Section 3 we will investigate the effect of adding the contradictory negation operator to extensions of first-order logic by strongly first-order operator; then in Section 4 we will develop a hierarchy theorem for totality atoms, and in Sections 5 and 6 we will study dependency atoms of arity 0 or 1.

Preliminaries
In this section we will briefly recall some fundamental definitions, as well as some results that we will need to use later in this work.

Definition 1 (Team).
Let M be a first order model with domain M and let V be a set of variables. A team X over M with domain Dom(X) = V is a set of assignments s : V → M.
Given such a team X and a tuple v of variables in Dom(X), we write X(v) for the relation {s(v) : s ∈ X}; and given a first-order formula θ , we write (X ↾ θ ) for the team {s ∈ X : M |= s θ } obtained by taking only the assignments of X which satisfy θ (according to Tarski's semantics).
For the purposes of this work, we will only consider the so-called lax version of team semantics, and we will only work with formula in negation normal form: Let M be a first order model, let X be a team over it, and let φ (v) be a first order formula in negation normal form and with free variables in v ⊆ Dom(X). We say that X satisfies φ (v) in M, and we write M |= X φ (v), if and only if this can be deduced from the following rules: However, team semantics allows us to extend first-order logic in novel ways, for instance by operators such as the intuitionistic implication [1]  TS-con: or totality [2]: More in general, all these atoms (and many more besides) can be seen as special cases of the following definition ( [17]): Definition 3 (Dependency Notion). Let k ∈ N. A k-ary dependency notion D is a class, closed under isomorphisms, of models over the signature {R}, where R is a k-ary relation symbol. For all models M, all teams X, and all tuples v of variables in the domain of X, Given a family D of dependency notions, we will write FO(D) for the logic obtained by adding all D ∈ D to the language of first-order logic. We will indicate with =(·) the family of all constancy dependencies =(v) of all arities, with =(·, ·) the family of all functional dependency atoms =(v, w) of all arities, and with All the family of all totality atoms All(w) of all arities; and when necessary, we will indicate the arities as a subscript -for instance, =(·) 1 represents the unary constancy atoms =(v) where v is a single variable, and =(·, ·) 2,2 represents the functional dependency atoms of the form =(v 1 v 2 , w 1 w 2 ).
The following notion of definability is of central importance for the study of team semantics: Definition 4 (Definability). Let D be a k-ary dependency notion and let D be a class of dependency notions. Then we say that D is definable through D if there exists a formula θ (v) ∈ FO(D) over the empty vocabulary, for all models M and teams X whose domain contains v.
What about totality dependencies? We will address this question in Section 4. All dependencies that we mentioned so far are first-order in the following sense: It is easy to see that if D is first-order then M |= X Dv ⇔ (M, X(v)) |= D * ; but owing to the higher-order nature of team semantics (and in particular, to the second-order quantification implicit in its rules for disjunctions and existential quantifiers) it does not follow from this that these dependencies do not increase the expressive power of first-order logic. For instance, the FO(=(·, ·) 1,1 )-sentence is true in a model M if and only if it is infinite, even though =(·, ·) 1,1 is first-order and corresponds to the sentence ∀xyy ′ (Rxy ∧ Rxy ′ → y = y ′ ). Therefore, the question arises of whether there exist interesting dependency notions for which this is not the case. More formally, one may ask if there exist nontrivial dependencies which are strongly first-order in the following sense: In [9], a positive answer was found for the above question.
As a consequence, it was shown that -for instance -all the following dependencies are strongly first-order for all arities of v and w, as is any set containing them (and the constancy atoms =(·)): The last two dependencies are not upwards-closed, but as shown in [9] they are definable in terms of constancy atoms and first-order, upwards-closed dependencies. We conclude this section by mentioning a few shorthands and results that we will need to use in the rest of this work:

Proposition 2.
For all models M and teams X, M |= X ⊤; and furthermore, M |= X ⊥ if and only if X = / 0.

Proof. Obvious.
Definition 9 (Dual Negation). Let φ be a first-order formula in negation normal form. Then we write ¬φ as a shorthand for the formula thus obtained: It is not difficult to see, by structural induction on φ , that Definition 10 (φ ↾ θ ). Let D be any class of dependencies, let φ ∈ FO(D) and let θ ∈ FO. Then we write φ ↾ θ as a shorthand for

Proposition 4 ([9]
). Let D be any class of dependencies, let φ ∈ FO(D) and let θ ∈ FO. Then for all suitable models M and teams X,

Definition 11 (Flattening). Let D be any class of dependencies and let φ ∈ FO(NE).
Then we define its flattening φ f as the first-order formula obtained by substituting all atoms Dv in it with ⊤.

Lemma 3 ([9]). Let D be a class of dependencies (not necessarily first-order or upwards-closed) and let φ (v) be a FO(=(·), D) formula. Then φ (v) is equivalent
to some formula of the form ∃w(=(w) ∧ ψ(w, v)), where ψ ∈ FO(D) contains the exactly the same instances of D-atoms (for all D ∈ D) that φ does, and in the same number.
The following simple result -which allows us to add, essentially for free, the classical disjunction ⊔ to our language -will also be of some use in the rest of this work:

Proposition 5. Let D be any class of dependencies and let
Proof. It suffices to show that the ⊔ connective commutes with all other connectives: In the first case we have that M |= X ∃vψ, and in the second case we have that M |= X ∃vθ ; so in either case M |= X (∃vψ) ⊔ (∃vθ ).

Corollary 1. Let D be a strongly first-order class of dependencies. Then every sentence of FO(D, ⊔) is equivalent to some sentence of FO.
Proof. Let φ ∈ FO(D, ⊔). As per the above results, we may assume that φ is of the form i ψ i , where all ψ i are FO(D)-sentences, and hence equivalent to first-order

On the Contradictory Negation
It is known from [19] that team logic FO(=(·, ·), ∼), that is, the logic obtained by adding the contradictory negation and functional dependency conditions (of all arities) to the language of first-order logic, is as expressive as second-order logic over sentences; and, furthermore, in [16] it was shown that all second-order properties of teams correspond to the satisfaction conditions of team logic sentences.
But what if we add the contradictory negation to weaker extensions of first-order logic? Or, for that matter, what if we consider FO(∼), that is, the logic obtained by adding only the contradictory negation to the language of first-order logic?
In this section, we will prove that Thus, the contradictory negation alone does not suffice to bring the expressive power of our logic beyond that of first-order logic, but as soon as we add even simple strongly first-order dependencies such as constancy or non-constancy we obtain the full expressive power of second-order logic. Proof. Consider the formula It is easy to check that Equation (1) is logically equivalent to =(v, w), as required. In what follows, we will prove that this logic is not more expressive than first-order logic over sentences; indeed, it is equivalent to FO(NE, ⊔).
Proof. We proceed by structural induction on φ .
Conversely, suppose that M |= X NE ↾ (¬φ ). Then the set X ↾ (¬φ ) is not empty, and therefore there exists some s ∈ X which satisfies ¬φ according to Tarski's semantics, and finally M |= X φ . 2. ∼ NE is easily seen to be equivalent to ⊥, which is true only in the empty team. 3. Suppose that φ is of the form (ψ ∨ θ ). Then ∼ φ is logically equivalent to Indeed, suppose that M |= X ∼ (ψ ∨ θ ). Then it is not the case that X = Y ∪ Z for two Y , Z such that M |= Y ψ and M |= Z θ . In particular, take Y = X ↾ ψ f and

5.
Suppose that φ is of the form (∃vψ). Then ∼ φ is logically equivalent to  (3). 6. Suppose that φ is of the form (∀vψ). Then ∼ φ is logically equivalent to ∀v ∼ ψ: We are now equipped to prove the main result of this section: . Then ∼ φ is equivalent to some formula in FO(NE, ⊔).
Proof. By Proposition 5, we may assume that φ is of the form n i=1 ψ i , where each ψ i is in FO(NE). Thus, ∼ φ is logically equivalent to n i=1 (∼ ψ i ); and by the above lemma, if ψ i is in FO(NE) then ∼ ψ i is in FO(NE, ⊔), as required.
The two following corollaries then follow at once:

Proposition 6. FO(NE, ⊔) ⊆ FO(∼).
Proof. It suffices to show that the nonemptiness atom and the classical disjunction are definable in FO(∼). As for the former, observe that M |= X ∼ ⊥ if an only if X is nonempty; and for the latter, observe that φ ⊔ ψ is logically equivalent to ∼ ((∼ φ ) ∧ (∼ ψ)).
Putting everything together, we have that

Theorem 4. FO(∼) = FO(NE, ⊔).
Finally, we need to prove that every sentence of FO(NE, ⊔) is equivalent to some first-order sentence. But this is immediate: Theorem 5. Let φ ∈ FO(NE, ⊔) be a sentence. Then φ is logically equivalent to some φ ′ ∈ FO.
Proof. By Proposition 5 we may assume that φ is of the form n i=1 ψ i , where each ψ i is a sentence in FO(NE). But then by Theorem 2, each ψ i is equivalent to some first-order sentence ψ ′ i , and thus φ is equivalent to the first-order sentence n i=1 ψ ′ i .

Arity Hierarchies for Totality Atoms
In this section we will investigate the properties of the k-ary totality atoms All k , and we we establish a strict arity hierarchy for them.
Let us begin by generalizing a notion from [9]: for all finite models M and all teams X.
Proof. The proof is by induction, and mirrors the analogous proof from [9].
1. If φ is a first order literal then it is 0-bounded (since the empty team satisfies it), as required. 2. If φ is an atom Dx then the statement follows at once from the definitions of boundedness. 3. Let φ be a disjunction ψ 1 ∨ ψ 2 then ν φ = ν ψ 1 + ν ψ 2 . Suppose now that M |= X ψ 1 ∨ ψ 2 : then X = X 1 ∪ X 2 for two X 1 and X 2 such that M |= X 1 ψ 1 and M |= X 2 ψ 2 .
This implies that there exist Y 1 ⊆ X 1 , Y 2 ⊆ X 2 such that M |= Y 1 ψ 1 and M |= Y 2 ψ 2 , |Y 1 | ≤ ν ψ 1 (|M|) and |Y 2 | ≤ ν ψ 2 (|M|). But then Y = Y 1 ∪Y 2 satisfies ψ 1 ∨ ψ 2 and has at most ν ψ 1 (|M|) + ν ψ 2 (|M|) elements. 4. If φ is a conjunction ψ 1 ∧ ψ 2 then, again, ν φ = ν ψ 1 + ν ψ 2 . Suppose that M |= X ψ 1 ∧ ψ 2 : then M |= X ψ 1 and M |= X ψ 2 , and therefore by Lemma 1 M |= X ψ f 1 and M |= X ψ f 2 ; and, by induction hypothesis, there exist Y 1 , Proof. By Proposition 5, we can assume that φ is of the form n i=1 ψ i , where all ψ i are in FO(=(·), D). Furthermore, by Lemma 3 we can assume that every ψ i is of the Proof. Suppose that φ (v) ∈ FO(=(·), D, ⊔) defines All k ′ . Then, since all dependencies in D are |M| k -bounded, we have at once that φ is q|M| k -bounded for some q ∈ N. Now let n ∈ N be such that n k ′ > qn k , let M be a model in the empty signature with n elements, let v be a tuple of k ′ variables, and let X = { / 0}[M/v]. Then M |= X All k ′ v, and therefore M |= X φ (v). But then there must be a Y ⊆ X, |Y | ≤ qn k , such that M |= Y φ (v); and this is not possible, because for such a Y we would have that M |= Y All k ′ x.
In particular, it follows at once from this that All k+1 is not definable in FO(= (·), All k , ⊔). On the other hand if k ′ < k the operator All k ′ v is easily seen to be definable as ∀w(All k vw); therefore Corollary 6. For all k ∈ N, FO(=(·), All k , ⊔) FO(=(·), All k+1 , ⊔) (and all these logics are equivalent to first-order logic over sentences).

0-ary Dependencies: Escaping the Empty Team
As a limit case of the notion of dependency, we have that Whenever X is nonempty it follows at once from Proposition 1 that M |= X [φ ] if and only if M |= X φ ; but since M |= / 0 φ for all first-order sentences φ , in first-order logic with team semantics we have no way of verifying whether a given first-order sentence is true of our model when we are considering satisfiability with respect to the empty team. Therefore, we will add this [·] operator to our language. It is easy to see that adding it to a strongly first-order extension of first-order logic does not break the property of being strongly first-order:

Proposition 8. Let D be any family of dependencies, and let φ ∈ FO(D, [·]). Then φ is logically equivalent to some sentence of the form i
Proof. The proof is by induction on φ , and it is entirely straightforward. We report only the case of disjunction: • For all first-order sentences θ i , θ ′ j and all FO(D) formulas ψ 1 , ψ 2 we have that ; and since M |= Y ψ and M |= Z θ , we also have that M |= X ψ ∨ θ , and so in conclusion Therefore we have the following result: Proof. We may assume that φ is on the form i [θ i ] ∧ ψ, where ψ is a FO(D)sentence. Now since D is strongly first-order, ψ is equivalent to some first-order ψ ′ ; and since { / 0} is nonempty, we can take φ ′ = i θ i ∧ ψ.

Unary Dependencies
We will now consider the case of unary dependencies, that is, of dependence atoms of arity one. As we will see, all first-order unary dependencies are strongly firstorder and definable in FO(=(·), [·], All 1 , ⊔).
In order to prove this we will make use of the following standard result: Proposition 10. For all k ∈ N, all variables v, all models M and all nonempty teams X whose domain contains v, Proof.
Proof. Let D be a unary first-order dependency and let v be a first-order variable. By definition, M |= X Dv if and only if (M, X(v)) |= D * (P), where D * (P) is a firstorder formula in the vocabulary {P} (P unary). But then D * (P) is equivalent to a Boolean combination of sentences of the form ∃ =k xPx and ∃ =k x¬Pk; and thus, we may assume that D * (P) is of the form i j θ i j , where each θ i j is ∃ =k xPx, ∃ =k x¬Px, or a negation of a formula of this kind. But then Dv is logically equivalent to Finally, we need to show that every sentence of FO(=(·), [·], All 1 , ⊔) is equivalent to some first-order sentence. But this is straightforward: ) be a sentence. Then φ is logically equivalent to some first-order sentence.
Proof. By Proposition 5, φ is equivalent to some sentence of the form ⊔ i ψ i , for ψ i ∈ FO(=(·), All 1 , [·]). Observe further that all expressions [θ ] which occur in our formulas are such that θ is a first-order sentence over the empty vocabulary; and therefore, these expressions are trivially upwards-closed first-order dependencies, since for any fixed model they either hold in all teams or in none of them. 3 Then by Theorem 2 and Proposition 9 every such sentence is equivalent to some first-order sentence ψ ′ i and thus φ is equivalent to i ψ ′ i .
Putting everything together, we have that

Conclusion
Much of the team semantics research has so far focused on formalisms which are greatly more expressive than first-order logic. However, the study of weaker extensions of first-order logic, which do not rise above it insofar as the definability of classes of models is concerned, promises to be also of significant value: not only this investigation offers an opportunity of examining the nature of the boundary between first-and second-order logic, but it also provides us with (comparatively) computationally "safe" classes of dependencies and operators to use in applications. This work builds on the results of [9] and can only be an initial attempt of making sense of the wealth of these "weak" extensions of first-order logic with team semantics. Much of course remains to be done; but a few distinctive characteristics of this line of investigation may be gleaned already.
• The totality atoms All k seem to have a role of particular relevance in the theory of strongly first-order dependencies. It remains to be seen whether this role will be preserved by the further developments of the theory; but in any case, the fact that these atoms are the "maximally unbounded" (in the sense of Definition 12) ones for their arities is certainly suggestive, as is the existence of a strict definability hierarchy based on their arities and the fact that all monadic first-order dependencies are definable in terms of the All 1 atom. • The logic FO(∼) = FO(NE, ⊔), as the simplest extension of first-order logic with team semantics which is closed under contradictory negation, is also an item of particular interest. As we saw, it suffices to add to it comparatively harmless dependencies such as constancy atoms to obtain the full expressive power of second-order logic; thus, despite its simplicity, this logics appears to be a natural "stopping point" in the family of dependency-based extensions of first-order logic, deserving of a more in-depth study of its properties. • When working with classes of strongly first-order dependencies, different choices of connectives and operators emerge to the foreground. In particular, the role of the classical disjunction φ ⊔ψ in the study of dependence logic and its extensions has been relatively marginal so far; but nonetheless, this connective proved itself of fundamental importance for many of the results of this work. More in general, it appears now that a fully satisfactory account of dependencies and definability cannot be developed if not by integrating it with a general theory of operators and uniform definability in team semantics. The work of [4,5,17] on generalized quantifiers in team semantics seems to be the most natural starting point for such an enterprise; in particular, it would be worthwhile to be able to characterize general families of dependencies and operators which do not increase the expressive power of first-order logic (wrt sentences).