Generalised quantifiers, which include Henkin's branching quantifiers, have been introduced by Mostowski and Lindström and developed as a substantial topic application of logic, especially model theory, to linguistics with work by Barwise, Cooper, Keenan. In this paper, we mainly study the proof theory of some non-standard quantifiers as second order formulae. Our first example is the usual pair of first order quantifiers (for all / there exists) when individuals are viewed as individual concepts handled by second order deductive rules. Our second example is the study of a second order translation of the simplest branching quantifier: “A member of each team and a member of each board of directors know each other”, for which we propose a second order treatment.
(C. Retoré)
CEUR
arguments that are predicates. This fits in well with the logico-functional view of quantification
in Montague semantics [
.
The paper is organised as follows.
We first provide a reminder on second order logic, because this topic is not so common. Next, we present a second order view of usual first order quantification as second order quantification over individual concepts — and show the two formulations are proved to be equivalent provided the individual concepts are standard (i.e. they may not be empty, as opposed to some Kripke and Muskens variants). Then, after a quick presentation of generalised quantifiers, we study the simplest branching quantifier as a second order construction, and we propose direct rules for this quantifier.
We briefly remind the reader with basic facts about second order logic, following [ 12, Chapter
5], and one may also refer to the survey [
A second-order language is based on a first-order language (the first three items in the list below), and extended with an infinitely enumerable set of predicate variables, each of them endowed with an arity (the last item in this list).
• an infinite enumerable set of first order (a.k.a. individual) variables • a set of constants , with in ( is often enumerable, but this is not required); 1 • an enumerable (or finite) set of predicate constants with in ℕ each of them with an arity (as in a first order language) – a predicate constant with arity 0 is a proposition; • an enumerable set of predicate variables in ℕ each of them with an arity – a , with in ℕ predicate variable with arity 0 is a propositional variable.
Second order formulae are defined “as expected”: an atomic formula is ( 1, … , ) with a predicate constant or a predicate variable of arity and the being first order terms (here ifrst order variables or first order constants since we have no functions). Les us call the set of atomic formulae . Then the set of second order formulae ℱ is defined by ℱ =∶∶ | ¬ℱ | ℱ ∧ ℱ | ℱ ∨ ℱ | ℱ → ℱ | ∀
ℱ | ∃ ℱ | ∀ ℱ | ∃ ℱ where stands for an individual variable while stands for a predicate variable of arity . The formula ⇔ is just a short-hand for ( → ) ∧ ( → ) . 1The first order language may also include an enumerable set of first order functions, but an -ary function in the
Although we shall not always write the superscript in ∀ and ∃ , beware that there are diferent pairs of second order quantifiers ( the variable or are bound by the closest ∀, ∃, ∀ , ∃ — if any — above them in the
∃ /∀ ), one pair for each arity. The occurrences of formula tree.
We use natural deduction with standard rules as can be found in [
The proof rules for second order quantifiers, namely the introduction and elimination rules of ∀ and ∃ are as expected, they are similar to the rules for first order quantifiers, mutatis mutandi: ⋅ ⋅ ⋅ ∀ [ ] [ , ( 1, … , ) ∶= ( 1, … , )]
(∀ ) ∃ [ ] [ [ ]]
⋅ ⋅ ⋅
(∃ ) ⋅ ⋅ ⋅
[ ] ∀ [ ]
(∀ ) ⋅ ⋅ ⋅ ∃ [ ] [ , ( 1, … , ) ∶= ( 1, … , )]
(∃ ) where 1. [ ] stands for a formula in which the predicate variable may occur (but that is not mandatory, as for first order quantification).
formula stands for the formula obtained by replacing 2. There should be no free occurrence of in the hypotheses of the introduction rule (∀ ) nor in the elimination rule (∃ ) — as in the first order ∀ and ∃ introduction rules.
3. The obscure notation2 [ , ( 1, … , ) ∶= ( 1, … , )] requires some explanation. This
• the th occurrence , of which is applied to terms ( 1, … , ) • with a formula with free variables applied to the very same terms ( 1, … , ) with the requirement that no originally free variable in ( 1, … , ) becomes bound after the application of to ( 1, … , ).
Here is an example: let (, ) = (, ) ∧ ( , ) mind the second subscript of 12,• which indicates the occurrence number (there are two occurrences of the predicate variable 12 in [ 12]. Then [ 1, ∶= ( 1, … , )] is 2 , let [ 1 ] = 12,1(, ) ∧ 2 12,2(, ) – 2This point is often under explained in the literature. (, )) ∧ ( (, ) ∧ (, ))
. From the definition and the example, it is unsurprising that
second order unification is undecidable [
cancelled during the (∃ ) number .
Some remarks: 1. this proof system can derive the comprehension axiom: ∃ ∀ 1 … [ ( 1, … , ) ↔ ( 1, … , )] 2. equality can be defined à la Leibnitz: = ∶ ∀ there is no need to use ⇔ in this definition) ∀2 2 3. being equal to is a property ( ) ∶ ∀ 1 1
[ 1() → 1( ) ]. 4. the Dedekind finiteness, “any injective function is surjective” is definable: ((∀∀ ∀( (, ) ∧ (, ) → = )) ∧ (∀∀ ∀( ( , ) ∧ (, ) → = ))) 1 1
[ 1() → 1( ) ] (because of negation →(∀ ∃ (, )) propositional quantifier ∀0 is impressive.
Finally, using implication →, first order ∀, and propositional second order ∀0 one can define false, ⊥, negation ¬, the propositional connective ∧, ∨, first order existential quantification ∃. Adding ∀ to →, ∀, one can also define ∃ . Thus, the expressive power of second order
We here follow [
A second order model consists in a first order model, i.e. with a domain , endowed with a set of sets of tuples of length for each ∈ ℕ in order to interpret predicate variables of arity : they may vary in a fixed subset ( ∃ ∀ 1 ⋯ ∀ [( 1, … , ) ↔
( 1, … , )] where the -ary predicate variable ); for this structure to define a model, it must enjoy the comprehension axiom scheme does not of ( ) which is not necessarily the full powerset appear in — in other words the subsets of
must include the interpretations of the formulae with free variables. The comprehension axiom scheme is derivable from the existential introduction rule given above. is (
By definition, a second-order model is said to be standard (or full) whenever the subset
) for any arity . Standard models satisfy the comprehension scheme. They do match
intuition: a predicate variable of arity varies in all possible subsets of . However, neither
completeness nor compactness hold when only standard models are considered — indeed second
order logic can express the finiteness of the domain , see e.g. [
Second order logic may be encoded in first order logic: predicate variables are viewed as individual constants interpreted in a domain (that also contains standard individuals), and some additional predicate constants of arity + 1 are needed to mimic the application of a predicate variable of arity to terms. Then a second order formula is provable within second order logic whenever its first order translation is provable in first order logic. So applying first order completeness theorem one gets that a second order formula is provable in second order logic if and only if it is true in all second order models (including the non standard ones). As a consequence of completeness, compactness holds, so one can have a model with at least elements for each integer , which is Dedekind finite.
Individual concepts view an individual as a formula [] with a single free variable such that there is a single individual satisfying the formula [] .3 This can be said in second order logic: a formula [] with a single free variable is said to be an individual concept whenever there is at most one individual such that [] and at least one such that [] — so it makes exactly one such that [] . That the concept is an individual concept can actually be expressed in second order logic, where the ”=” symbol refers to usual equality (with its usual rules: reflexivity, symmetry, transivity, substition etc. noted ”=” in the proofs):4 () ∶= (∀∀ [() ∧ ( ) → = ]) ∧ ∃ ()
Individual concepts are close to Montague semantics and Leibnitz identity (where an
individual is identified with the set of all properties it enjoys) [
The simplest quantifiers one can try to view as a second order construction are clearly the usual
ifrst order quantifiers ∀, ∃. So let us compare the second order quantification over individual
concepts to usual quantification.
3This notion of concept is somehow related to concepts in description logics, and the individual concepts that we
use correspond to individual names cf. e.g. [
Proof. Let us first observe that there is a simple formal proof without assumption that ( ) i.e. that “being equal to ” (cf. section 2 item 3) is an individual concept, ( ) ∶ = ∶ ∀1 1 ( 1() → 1( )) , and let us call this proof , because we are going to use it several times: ∶ [y = x ∧ z = x] y = x ∧E y = z y = x ∧ z = x → y = z → I
∀1I ∀z(y = x ∧ z = x → y = z)
∀1I ∀y∀z(y = x ∧ z = x → y = z) :=
C(Ex) [y = x ∧ z = x] z = x ∧E x = z symetrie meaqmmSTESSF
a) Assuming ∀ ↓() one can prove ∀ (( ) → ( ))
Preuve. [∀xϕ ↓(x)]
[C(X )] ∀x∀y(X (x) ∧ X (y) → x = y) ∧ ∃xX (x)
∃xX (x) ∀xϕ ↓(x) ∧ X (x)
ϕ ↓(x) ∃YC(Y ) ∧Y (x) ∧ ϕ (Y ) :=
X (x) ∧I ∧E b) AssDuamnisncge∀tte((p )re→uv(e )o)n de´duiot ne candperove ∀ car↓()e.tIn tshoentpdroesofcboenlcoewp,tswienduisveid uels : the proof that (_) = "_ = " (that is, “being equal to ”) is an individual concept. ∀1E [∀X (C(X ) → ϕ (X ))]
C(Ex) → ϕ (Ex) ϕ (Ex)
∀E → E ∧I 2. a) Assnuemifnogn∀c t(io)n qouniesciagnnpifiroeve“∀est(e(´ g)a→l a` x↑”(. )Ic)i on obtient E x [C(X)] ∀x∀y(X(x) ∧ X(y) → x = y) ∧ ∃x X(x) ∃xX(x) := ∧E X(x) [X(x)] 1
∃ E
X(x) ∧ψ (x) 1 ∃x(X(x) ∧ψ (x)) :∃= I
ψ ↑(X)
C(X) → ψ ↑(X) ∀X(C(X) → ψ ↑(X) → I ∀2I [∀xψ (x)] 1 ψ (x) ∀ E ∧I b) Finally assuming ∀ (( ) →
↑( ) ) one can prove: ∀ () δ . . .
.
C(Ex) [∀X (C(X ) → ψ ↑(X )]
C(Ex) → ψ ↑(Ex) ψ ↑(Ex) ∃yEx(y) ∧ ψ (y)
Ex(y) ∧ ψ (y) := y = x ∧ ψ (y)
ψ (x) 1 ∀xψ (x) ∀ I ∧E := ∃1E
∀2E → E 3.3. First Order Existential Quantification as Existential Quantification Over
As for the universal quantification, we have: Proposition 2. First order existential quantification and second order quantification over individual concepts are equivalent: 1. when is a property of individual concepts, one has ∃ ↓() ⇔ ∃ (( ) ∧ ( )) ↓() ∶= ∃ (( )∧ () ∧ ( )) . 2. when is a property of individuals, one has ∃ () ⇔ ∃ (( ) ∧ ∃( () ∧ ()) ↑( ) ) where ↑( ) ∶= Proof. At point 2.a) we will also use the proof of ( ) from the proof of proposition 1. 1. ∃ ↓() ⇔ ∃ (( ) ∧ ( )) a) Let us prove ∃ (( ) ∧ ( ))
Preuve.
where ↓() ∶= ∃ (( )∧ () ∧ ( )
under the assumption ∃ ↓() . [∃xϕ ↓(x)] ∃X(C(X)[ϕ∧↓X(x(x)]) ∧ϕ (X)) :=
∃X(C(X) ∧ϕ (X)) ∃1E ∃X(C(X) ∧ϕ (X)) [C(X) ∧ X(x) ∧ϕ (X)]
C(X) ∧E [C(X) ∧ X(x) ∧ϕ (X)]
ϕ (X) ∃2I C(X) ∧ϕ (X) ∃2E b) NoEwnsuleitteuosnpsroouvheai∃te pr↓ouveruln’idmeprlitchaetioanssiunmveprsteio:ns’∃il(( ) ∧ (c)o)ncept in. dWiviedufirsetl qnueied () y a un , , i.e. the three following proofs : where ∧E ∶ ∶
X (x) and the proof we are looking for is:
CC(α(....XX)) ∧ XXγ((....xx)) ∧I ϕ (β....X )
C(X ) ∧ X (x) ∧ ϕ (X ) ∧∃I2I ∃X (C(X ) ∧ X (x) ∧ ϕ (X )) :=
∃ϕxϕ↓(↓x()x) ∃1I 2. ∃ () ⇔ ∃ (( ) ∧ ↑( ) ) where ↑( ) ∶= ∃( () ∧ ()) a) Let us prove ∃ (( ) ∧ ↑( ) ) under the assumption ∃ () – is the proof of tildisefineeidciinltahepprerouovf eof prvopuopsiotiuonr le1.lemme 2 pour de´duire C ( )
x = x [∃xψ (x)] [ψ (x)] δ.... Ex(Ex)x(x) ∧ ψ (xψ)(x) ∧1I δ.... CC((EExx)) ∧ ∃∃yy((EExx((yy))∧∧ψψ((yy)))) :∃∧=II C(Ex) ψ ↑(Ex) ∧I ∃CX((ECx()X∧)ψ∧↑ψ(E↑(xX) ) ∃2I ∃1E b) Lee.t us prove ∃ () under the assumption ∃ (( ) ∧ ↑( ) ) [∃X (C(X ) ∧ ψ ↑(X ))] [C(X ) ∧ ψ ↑(x)]
∃2E C(X ) ∧ ψ ↑(X )
ψ ↑(X ) ∃x(X (x) ∧ ψ (x)) ∧E :=
ψ (x) 1 ∃xψ (x) ∃ I [X (x) ∧ ψ (x)] ψ (x) ∃1E ∧E
When individual concepts are possibly empty the second order formula expressing that is an individual concept is ( ) = ∀∀ ( ∧ → = ) — the ∃ () left out of our initial definition of individual concepts.
Regarding universal quantification, ∀ ( ( ) → ( )) still entails ∀ ↓() , but ∀ ↓() does not entail ∀ ( ( ) → ( )) anymore. This is logical: when all individual concepts have a property be they empty or not, all individuals enjoy the corresponding first order property. The converse does not hold: when all individuals enjoy a property, all the non empty concepts enjoy the property, but why should the empty individual concept enjoy this property as well?
Of course regarding existential quantification, that’s the opposite. ∃ () entails ∃ ( ( ) ∧ ( ))) but ∃ ( ( ) ∧ ( )) does not entail ∃ () . When an individual enjoys a property, so does the corresponding individual concept. But when a possibly empty individual concept enjoys a property, it does not entail that an individual enjoys this property, because this individual concept might be an empty individual concept.
So the second order view of usual quantification does not fit in well with possibly empty
individual concepts.
4. A Reminder on Generalised and Branching Quantifiers
This reminder mainly relies on the presentation given by Peters and Westerståhl [22], one may
also consult the survey [
Given integers 1, ..., , a quantifier of type ⟨ 1, ..., ⟩ can be viewed as a function endowing each domain with a -ary relation such that if ( 1, ..., ) ∈ , then for all in between 1 and , is a -ary relation over elements of . Let us give some examples.
The usual quantifiers ∀ and ∃ can be then expressed as simple type ⟨1⟩ quantifiers : ∃ = { ⊆ , ≠ ∅} and ∀ = { ⊆ , = } . Thus, the existential quantifier is in every domain the unary relation which holds true for all non-empty predicates, and the universal quantifier is the relation which holds true only for the whole domain .
Some generalised quantifiers have an equivalent formulation in usual first-order logic, such as the quantifier “at least two”: (∃≥2) = { ⊆ , || ≥ 2} which can be expressed with the following first-order formula: ∃∃ [ ≠ ] . However this is not always the case. Take for example the type ⟨1, 1⟩ quantifier expressing that most are : Most (, ) ⟺ |∩| > |−| which notably cannot be expressed as a first-order formula.
It is worth noting that universal and existential quantification on individual concepts as we presented in Section 3 can also be formulated in terms of generalised quantifiers. To say that all (resp. some) individual concepts satisfy a property is in fact a second-order statement about the predicates (“to be an individual concept”) and . Hence the second order view of first order quantification that we presented in the previous section can be expressed as generalised quantifiers ∀ and ∃ with type ⟨1, 1⟩: ∀ (, ) ⟺ ⊂ ∃ (, ) ⟺ ∩ ≠ ∅
Among generalised quantifiers, branching quantifiers are of particular interest, both for logic and linguistics. Initially introduced by Henkin [23] and much later on studied by Hintikka [24] — independently of generalised quantifiers — branching quantification is a generalisation of classical quantification that allows the expression of independence between some existentially quantified variable and some previously universally quantified variables. This cannot be expressed within usual quantification because quantifiers are supposed to be linearly ordered. The simplest example of such a non-first-order quantifier is the following Henkin quantifier where, as the notation suggests, ′ only depends on , while ′, only depends on . ∀∃ ′
As proven by Ehrenfeucht (in Henkin [23]), this construction has no first-order equivalent. Notably, it cannot be expressed with a linear quantifier prefix such as ∀∃ ′∀ ∃ ′ or ∀∀ ∃ ′∃ ′, since there would be unwanted dependencies between ′ and , and ′ and .
Although not initially introduced as such, branching quantifiers can in fact be seen as specific generalised quantifiers. Indeed, the (in)dependencies between variables can be expressed using Skolem functions, e.g. the Henkin quantifier above can be written as follows: ∃ ∃∀∀ (, (), , ( )) = { ⊆
4 | ∃ ∃∀∀ (, (), , ( )) ∈ } This in turn allows us to translate it as a generalised quantifier, for example here as the type ⟨4⟩ quantifier: 5. Second Order Proof Rules for Branching Quantifiers Branching Quantifiers as Second Order Formulae In this part, we focus on the expression of branching quantifiers as second-order constructions. Such quantifiers can be quite complex, so we limit ourselves to studying the simplest branching quantifier. Our main object of study is the typical branching constructions found in natural language in the so-called Hintikka sentences, such as : (H) A member of each team and a member of each board of directors know each other
The branching-quantifier reading of the above English sentence can be formulated within second-order logic:5 ∀∃ ′
As mentioned earlier, this formula can be expressed as a second order formula with existential quantification over functions:
(Hfun) ∶ ∃ ∃∀∀ [ () ∧ ( )] → ( (), ( )) Natural Deduction Rules With Binary Predicates This formulation of the Henkin quantiifer as a second-order formula with quantification over functions is however not fully satisfactory, for it actually provides a stronger efect than needed: defining and as functions implies the unicity of () and ( ) for any given and , while the original formula with a branching quantifier only requires that there exists one (possibly more) ′ for each and ′ for each . Thus and need not be functions, but only need be non-empty binary predicates — as always with Skolem functions, the choice of () for each is part of the interpretation of the function symbol.
Therefore, we propose another second-order representation of this reading of the sentence using quantification over predicates instead of quantification over functions: (Hpred) ∶∃ ∃[∀∃
′ () → (, ∧ [∀∀ ′∀ ∀ ′[ () ∧ ( ) ∧ (, ′)] ∧ [∀ ∃ ′( ) → ( , ′) ∧ ( ,
′)] ′)] → ( ′, ′)]
This formula simply replaces each of the two functions and of ( ) above with the binary predicates and . These two predicates act intuitively as relations that select suitable ′ and ′, since all we need to ensure is that whenever ′ is a valid representative for (and ′ for ), then ′ and ′ know each other. The binary predicates and are required to relate each possible value of their first argument which ought to be in the proper set/predicate ( for , for 5wThheicreh icsaanlsboeaefirxspt-roersdseedr rweaitdhiinngfirosft-tohridsesrenlotgenicc:e, w[∀h∃ich′∀th∃e ’e′ac h()o∧th(e)r’→(p(e,rhaps) ma′k)e∧s l(e, ss pe′r)ce∧p(tible′,, a′n)]d∧ [∀∃ ′∀∃ ′ () ∧ () → (, ′) ∧ (, ′) ∧ ( ′, ′)]. According to Szymanik [25], in two-thirds of cases, the first-order reading is preferred to the branching quantifier reading. (resp. ′) such that (,
′) (resp. ( , where one is explicitly chosen. ) to at least one value of their second argument.6 There is nevertheless a diference between using function as in (Hfun) and (Hpred): in (Hpred) there may well exist several values of ′ ′)), there is no need to chose one as opposed to (Hfun),
The natural deduction rules for second-order logic from section 2.2 give us the introduction and elimination rules for the branching Henkin quantifier. For the sake of readability, let us write from here on: and Φ( , , , ′, , ′) = [ () ∧ ( ) ∧ (, ′) ∧ ( , ′)] → ( ′, ′) Ψ( , ) = [∀∃ ′ () → (, ′)] ∧ [∀ ∃ ′ ( ) → ( ,
′)] ∧ [∀, ∀ ′∀ ∀ ′Φ( , , , ′, , ′)]
The introduction rule is quite straightforward: , ′, and , are terms. eliminations of ∃2: where is a formula with free variables exactly , ′, a formula with free variables exactly The elimination rule, however, is more complicated due to the use of two second-order (, ) ( , )
Φ(, , , ′)] ∧ [∀ ∃ ′ ( ) → ( , ′, , ′
) ′)] ∧ [∀, ∀ ′ ∀ ∀ ′Φ( , , , ′, , ′)] ∃ ∃Ψ( , )
′) the branching quantifier that binds the two universally and the two existentially quantified variables , ′ ′ e.g. the example in which and must not appear free in .
Let us write as above (, quantified variables , above may be written (, ifrst order quantifiers
∃ and ∀ .
Let ℋ be the set of closed formulae that can be written with this quantifier and the two usual In the near future, we intend to determine whether our direct rules can be used to derive all the formulae in ℋ that can be derived with the usual rules for second and first quantifiers. It seems plausible to us, because cut-elimination holds for second order logic. [26] However, we are not yet fully certain, and this is one aspect that we intend to clarify in the near future. 6Similarly, we could ask that ′ and ′ are in the proper set/predicate ( for ′, for ′) but it is less important. Thus we do not add this precision, which is not needed — unlike the restriction to and — and makes the formulae, (, ′) ∧ ( ′ )] ∧ [∀∀ ′ ∀∀ ′ () ∧ (
′) ∧ () ∧ ( which are already long enough, considerably longer: Hpred ∶ ∃ ∃[∀∃ ′ ′) ∧ (, ′ ) ∧ (, ′ ) → ( ′, ′)] ′ () → (, ′) ∧ ( ′ )] ∧ [∀∃ ′ () →
This ongoing work deals with the proof rules of extensions of first order quantification viewed as second order logic constructions which do not need the full expressive power (and complexity) of second order logic.
We first described usual first order quantifiers within the second order logic as quantification over individual concepts and obtained that this description works provided individual concepts are asked to be non empty — unsurprisingly it does not work without this restriction.
Thereafter we focused on the non first order reading of the simplest branching quantifier that one finds in sentences like: “A member of each team and a member of each board of directors know each other”. Regarding this (reading of this) quantifier, we proposed a definition of it within second order logic and provided direct introduction and elimination rules for this complex quantifier which is often only described in model-theoretic terms. Later on we shall prove that the complete set of second order rules does not derive more sentences with those connectives than our direct rules.
While we were working on the final version of this article, we realised that Matthias Baaz and Anela Lolic [27] proposed an analytic calculus for Henkin quantifiers. In their paper, Henkin quantifiers are viewed as the existence of functions (i.e. as a particular form of second order quantification), and they proved cut-elimination for this calculus. It is too late for this paper of ours to examine how their account of Henkin quantifiers difers from ours, but this will be be our first aim in continuing our work. A first remark is that (1) ∶ ∃ ∀ ∃ (, ) seems slightly weaker than (2) ∶ ∃ (, ()) : in order to derive (2)from 1, it is necessary to utilise some form of the axiom of choice. Another diference, a very small one actually, is that our rules are natural deduction rules (introduction/elimination rules) and not sequent calculus: sequent-calculus right-rules correspond to natural-deduction introduction-rules but sequent-calculus left-rules do not correspond to natural-deduction elimination-rules.
By way of conclusion, let us mention a prospect that has opened up to us recently. The epsilon calculus [28, 29] may express readings that are close to branching quantifier readings, with epsilon formulas that have no equivalent in first or higher order logic 7. Indeed, the subnectors epsilon and tau express quantification with some scope ambiguities (under-specification) 8. However, it is presently too early to say anything definite about this question.
We would like to express our gratitude to the anonymous reviewers and to the chairs of ARQNL2024 for their valuable feedback, which has been instrumental in helping us to enhance this article. Furthermore, we would like to extend our gratitude to the programme chairs who accepted some late modifications. 7The formula ( ()) is not equivalent to any first order formula — although it is equivalent to ∃ () ∧ () when additionally ∃ () ≡ ( ()) holds. 8As an example of under-specification or scope ambiguity in the -calculus, a formula like ( (), ()) which has no equivalent in first order logic, has some logical relation, depending on whether and are ∅ or , with the two first-order formulas ∀∃ () ⟹ (() ∧ (, )) and ∃∀ () ∧ (() ⟹ (, )) .