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.
Common first order quantifiers ∃ and ∀ have been formalised the way they are in standard mathematics by Frege [1] whose logical and philosophical view matches Hilbert desiderata regarding logical foundations of mathematics. [2,3,4,5] By that time, mathematicians and logicians were making little difference between the interpretations of quantifiers in the standard model and their proof rules -before the work of Skolem or Gödel, mathematicians and logicians made little distinction between syntax and semantics, they worked with an interpreted language, see e.g. [2] --perhaps Hilbert was more demanding regarding quantifiers because he focused on foundations of mathematics [3].
Extensions of usual quantification have mainly been considered for faithfully modelling quantification modes that one finds in ordinary language, like numbers ("three students came to the party"), "most" ("most students came to the party"), percentages ("a third of the students came to the party"), vague quantifiers ("few students came to the party"), etc.
This gave rise to the theory of generalised quantifiers, initially intended for model theory [6,7], that was intensively developed in connection with linguistics. [8,9,10]. In such a setting, the lexical item expressing a quantifier (say "most A are B") is viewed as a function with two arguments that are predicates. This fits in well with the logico-functional view of quantification in Montague semantics [11]. Most (!) generalised quantifiers can be viewed as a second order construction. For instance the interpretation of a generalised quantifier depending on two unary predicates like "most" is interpreted as a second order construction, i.e. is true whenever the pairs of unary predicates it is applied to is a "legal" pair of subsets of the domain, namely a pair of sets (𝐴, 𝐵) such that |𝐴 ∩ 𝐵| > |𝐴 ∖ 𝐵|.
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 [13].
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 𝑥 𝑖 , with 𝑖 in ℕ • 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 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 first 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 (𝐴 → 𝐵) ∧ (𝐵 → 𝐴).
Although we shall not always write the 𝑛 superscript in ∀ 𝑛 and ∃ 𝑛 , beware that there are different pairs of second order quantifiers (∃ 𝑛 /∀ 𝑛 ), one pair for each arity. The occurrences of the variable 𝑥 𝑖 or 𝑋 𝑛 𝑖 are bound by the closest ∀𝑥, ∃𝑥, ∀ 𝑛 𝑋 𝑛 𝑖 , ∃ 𝑛 𝑋 𝑛 𝑖 -if any -above them in the formula tree.
We use natural deduction with standard rules as can be found in [12]. As we limit ourselves to classical logic, an extra principle is needed: tertium non datur (𝐴 ∨ ¬𝐴 for all 𝐴) or reductio ad absurdum (from a deduction with conclusion ⊥ under hypothesis ¬𝐴, conclude 𝐴), see e.g. [14] 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. this proof system can derive the comprehension axiom:
2. equality can be defined à la Leibnitz:
4. the Dedekind finiteness, "any injective function is surjective" is definable:
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 propositional quantifier ∀ 0 is impressive.
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 𝐴 𝑛 of 𝒫 (𝐷 𝑛 ) which is not necessarily the full powerset 𝒫 (𝐷 𝑛 ); for this structure to define a model, it must enjoy the comprehension axiom scheme
where the 𝑛-ary predicate variable 𝑋 𝑛 does not 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.
By definition, a second-order model is said to be standard (or full) whenever the subset 𝐴 𝑛 is 𝒫 (𝐷 𝑛 ) 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. [12].
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.
Quantifying Over Individual Concepts
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) [18,19,11]. For reasons like possible worlds semantics, see e.g. the discussion in [20, chapter 4], some logicians consider a variant of individual concepts that are possibly empty. This may look strange but if you think individual concepts are some kind of proper name that are part of the logical language, it is hard to tell what a proper name refers to before the reference actually exists. For instance, the individual concept Gödel(𝑥) has no reference in Egyptian times. Hence Kripke in the 70s dropped the existence condition from individual concepts (see [21] for a recent account of those ideas), thus obtaining a formula with a lower logical complexity profile:
So 𝐶(𝜙) can be defined as 𝐶(𝜙) ∶= 𝐶 𝜖 (𝜙) ∧ ∃𝑧 𝜙(𝑧).
The simplest quantifiers one can try to view as a second order construction are clearly the usual first order quantifiers ∀, ∃. So let us compare the second order quantification over individual concepts to usual quantification. 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:
Preuve.
[∀xϕ
Dans cette preuve on déduit de car et sont des concepts individuels : b) Assuming ∀𝑋 (𝐶(𝑋 ) → 𝜑(𝑋 )) one can prove ∀𝑥 𝜑 ↓ (𝑥). In the proof below, we use 𝛿 the proof that 𝐸 𝑥 (_) = "_ = 𝑥" (that is, "being equal to 𝑥") is an individual concept.
δ . . . . δ . . . .
As for the universal quantification, we have: Preuve.
Ensuite on souhaite prouver l'implication inverse : s'il y a un concept individuel qui b) Now let us prove ∃𝑥 𝜑 ↓ (𝑥) under the assumption ∃𝑋 (𝐶(𝑋 ) ∧ 𝜑(𝑋 )). We first need 𝛼, 𝛽, 𝛾 i.e. the three following proofs :
and the proof we are looking for is: tilise ici la preuve vu pour le lemme 2 pour déduire C δ . . . .
Let us prove ∃𝑥 𝜓 (𝑥) under the assumption ∃𝑋 (𝐶(𝑋 ) ∧ 𝜓 ↑ (𝑋 ))
e.
[∃X(C(X)
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.
This reminder mainly relies on the presentation given by Peters and Westerståhl [22], one may also consult the survey [10]. Generalised quantifiers, initially introduced by Mostowski [6] and further developed by Lindström [7] are a generalisation of standard universal and existential quantification. Roughly speaking, generalised quantifiers view quantifiers as relations over relations (or tuples of relations) -those relations are relations on the domain (a.k.a universe, model) of an interpretation: thus, quantifiers are viewed as second-order concepts.
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:
This in turn allows us to translate it as a generalised quantifier, for example here as the type ⟨4⟩ quantifier:
𝐻 𝑀 = {𝑅 ⊆ 𝑀 4 | ∃𝑓 ∃𝑔∀𝑥∀𝑦 (𝑥, 𝑓 (𝑥), 𝑦, 𝑔(𝑦)) ∈ 𝑅}
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 quantifier as a second-order formula with quantification over functions is however not fully satisfactory, for it actually provides a stronger effect 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:
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 𝑦) to at least one value of their second argument. 6 There is nevertheless a difference between using function as in (Hfun) and (Hpred): in (Hpred) there may well exist several values of 𝑥 ′ (resp. 𝑦 ′ ) such that 𝐹 (𝑥, 𝑥 ′ ) (resp. 𝐺(𝑦, 𝑦 ′ )), there is no need to chose one as opposed to (Hfun), where one is explicitly chosen.
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:
The introduction rule is quite straightforward:
where 𝜑 is a formula with free variables exactly 𝑥, 𝑥 ′ , 𝜓 a formula with free variables exactly 𝑦, 𝑦 ′ , and 𝑡, 𝑢 are terms.
The elimination rule, however, is more complicated due to the use of two second-order eliminations of ∃ 2 : ∃𝐹 ∃𝐺Ψ(𝐹 , 𝐺)
[∃𝐺Ψ(𝐴, 𝐺)] (2) [Ψ(𝐴, 𝐵)]
in which 𝐴 and 𝐵 must not appear free in 𝜑.
Let us write as above 𝐻 (𝑥, 𝑥 ′ , 𝑦, 𝑦 ′ ) the branching quantifier that binds the two universally quantified variables 𝑥, 𝑦 and the two existentially quantified variables 𝑥 ′ , 𝑦 ′ e.g. the example above may be written 𝐻 (𝑥, 𝑥 ′ , 𝑦, 𝑦 ′ ) Φ(𝐹 , 𝐺, 𝑥, 𝑥 ′ , 𝑦, 𝑦 ′ ).
Let ℋ be the set of closed formulae that can be written with this quantifier and the two usual first order quantifiers ∃𝑥 and ∀𝑦.
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.
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 differs 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 difference, 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.