=Paper=
{{Paper
|id=Vol-3875/ARQNL2024_paper8
|storemode=property
|title=A Proof-Theoretical Approach to Some Extensions of First Order Quantification
|pdfUrl=https://ceur-ws.org/Vol-3875/ARQNL2024_paper8.pdf
|volume=Vol-3875
|authors=Loïc Allègre,Ophélie Lacroix,Christian Retoré
|dblpUrl=https://dblp.org/rec/conf/arqnl/AllegreLR24
}}
==A Proof-Theoretical Approach to Some Extensions of First Order Quantification==
https://ceur-ws.org/Vol-3875/ARQNL2024_paper8.pdf
A Proof-Theoretical Approach to Some Extensions of
First Order Quantification
Loïc Allègre1 , Ophélie Lacroix2 and Christian Retoré1
1
LIRMM (Univ Montpellier & CNRS), Montpellier, France
2
Resolve, Copenhagen, Danemark
Abstract
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.
Keywords
proof theory, second order logic, generalised quantifiers, branching quantifiers, individual concepts,
1. Generalisation of Usual First Order Quantification
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 in-
terpretations 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
ARQNL 2024: Automated Reasoning in Quantified Non-Classical Logics, 1 July 2024, Nancy, France
Envelope-Open loic.allegre@lirmm.fr (L. Allègre); ophelie.lacroix@resolve.tech (O. Lacroix); christian.retore@lirmm.fr
(C. Retoré)
GLOBE https://sites.google.com/site/ophelielacroixnlp/ (O. Lacroix); http://www.lirmm.fr/~retore (C. Retoré)
Orcid 0000-0002-2401-9158 (C. Retoré)
© 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
ceur-ws.org
ISSN 1613-0073 ARQNL 2024 92 P ROCEEDINGS
Proceedings
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.
2. A Reminder on Second Order Logic
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].
2.1. Language
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 (𝐴 → 𝐵) ∧ (𝐵 → 𝐴).
1
The first order language may also include an enumerable set of first order functions, but an 𝑛-ary function 𝑔 in the
language can replaced with an 𝑛 + 1-ary predicate 𝐺 with an axiom that 𝐹 is a function, and at second order there is
a formula 𝐹 [𝑋 ] saying that the 𝑛 + 1-ary predicate 𝑋 corresponds to an 𝑛-ary function.
93
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.
2.2. Proof Rules in Natural Deduction
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 , … , 𝑡 𝑛 ) ∶= 𝜙 𝑛 (𝑡 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).
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
𝑘 𝑘 𝑘 𝑘
formula stands for the formula obtained by replacing
• 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 𝜙(𝑥, 𝑦) = 𝑃(𝑥, 𝑦) ∧ 𝑄(𝑦, 𝑎), let 𝑇 [𝑋12 ] = 𝑋1,1 2 (𝑧, 𝑎) ∧ 𝑋 2 (𝑎, 𝑏) –
1,2
mind the second subscript of 𝑋1,• which indicates the occurrence number (there are
2
two occurrences of the predicate variable 𝑋12 in 𝑇 [𝑋12 ]. Then 𝑇 [𝑋1,𝑘 2 ∶= 𝜙(𝑡 1 , … , 𝑡 𝑛 )] is
𝑘 𝑘
2
This point is often under explained in the literature.
94
(𝑃(𝑥, 𝑦) ∧ 𝑄(𝑦, 𝑎))[𝑥 ∶= 𝑧; 𝑦 ∶= 𝑎] ∧ (𝑃(𝑥, 𝑦) ∧ 𝑄(𝑦, 𝑎))[𝑥 ∶= 𝑎; 𝑦 ∶= 𝑏] that is (𝑃(𝑧, 𝑎) ∧
𝑄(𝑎, 𝑎)) ∧ (𝑃(𝑎, 𝑏) ∧ 𝑄(𝑏, 𝑎)). From the definition and the example, it is unsurprising that
second order unification is undecidable [15].
𝑘
4. In the rule (∃𝑛 )𝐸 the expression [𝑇 [𝑋𝑖𝑛 ]] indicates that the hypothesis 𝑇 [𝑋𝑖𝑛 ] has been
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: 𝑥 = 𝑦 ∶ ∀1 𝑋 1 [𝑋 1 (𝑥) → 𝑋 1 (𝑦)] (because of negation
there is no need to use ⇔ in this definition)
3. being equal to 𝑥 is a property 𝐸𝑥 (𝑦) ∶ ∀1 𝑋 1 [𝑋 1 (𝑥) → 𝑋 1 (𝑦)].
4. the Dedekind finiteness, “any injective function is surjective” is definable:
∀2 𝑋 2 ((∀𝑥∀𝑦∀𝑧(𝑋 (𝑥, 𝑦) ∧ 𝑋 (𝑥, 𝑧) → 𝑦 = 𝑧)) ∧ (∀𝑥∀𝑦∀𝑧(𝑋 (𝑦, 𝑥) ∧ 𝑋 (𝑧, 𝑥) → 𝑦 = 𝑧)))
→(∀𝑤∃𝑢 𝑋 (𝑢, 𝑤))
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.
2.3. Standard and Non-standard Models, Completeness
We here follow [16, 13, 12].
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
∃𝑛 𝑋 𝑛 ∀𝑥1 ⋯ ∀𝑥𝑛 [𝜙(𝑥1 , … , 𝑥𝑛 ) ↔ 𝑋 𝑛 (𝑥1 , … , 𝑥𝑛 )] 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
95
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.
3. A Second Order View of First Order Quantification:
Quantifying Over Individual Concepts
3.1. 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 individ-
ual 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 𝐶(𝜙) ∶= 𝐶𝜖 (𝜙) ∧ ∃𝑧 𝜙(𝑧).
3.2. First Order Universal Quantification as Universal Quantification Over
Non-empty Individual Concepts
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.
3
This 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. [17].
4
The ”∶=” symbol denotes an abbreviation (or a definition) of a formula, and in proofs, the replacement of an
abbreviation by its expansion or vice-versa.
96
Proposition 1. First order universal quantification and second order quantification over individual
concepts are equivalent:
1. given a property 𝜑(𝑋 ) of individual concepts, the following equivalence holds: ∀𝑥 𝜑 ↓ (𝑥) ⇔
∀𝑋 (𝐶(𝑋 ) → 𝜑(𝑋 )) where 𝜑 ↓ (𝑥) ∶= ∃𝑋 (𝐶(𝑋 )∧ 𝑋 (𝑥) ∧ 𝜑(𝑋 )).
2. given a property 𝜓 (𝑥) of individuals, the following equivalence holds: ∀𝑥 𝜓 (𝑥) ⇔
∀𝑋 (𝐶(𝑋 ) → 𝜓 ↑ (𝑋 )) where 𝜓 ↑ (𝑋 ) ∶= ∃𝑥(𝑋 (𝑥) ∧ 𝜓 (𝑥)).
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 ∧ z = x] z=x ∧E
y=x ∧E symetrie
x = z mammSTESSF
eq
y=z
y = x∧z = x → y = z → I
∀1 I
∀z(y = x ∧ z = x → y = z)
∀1 I
∀y∀z(y = x ∧ z = x → y = z)
:=
C(Ex )
1. a) Assuming ∀𝑥 𝜑 ↓ (𝑥) one can prove ∀𝑋 (𝐶(𝑋 ) → 𝜑(𝑋 ))
Preuve.
[C(X)]
∀x∀y(X(x) ∧ X(y) → x = y) ∧ ∃xX(x)
∧E
∃xX(x) [X(x)]
∃1 E
[∀xϕ ↓ (x)] X(x)
↓
∧I
∀xϕ (x) ∧ X(x)
ϕ ↓ (x)
:=
∃YC(Y ) ∧Y (x) ∧ ϕ (Y ) [C(Y ) ∧Y (x) ∧ ϕ (Y )]
∃2 E
C(Y ) ∧Y (x) ∧ ϕ (Y )
∧E
Y (x) ∧ ϕ (Y )
∧E
ϕ (Y )
:=
ϕ (X)
→I
C(X) → ϕ (X)
∀2 E
∀X(C(X) → ϕ (X)
b) Assuming ∀𝑋 (𝐶(𝑋
Dans cette preuve)→on𝜑(𝑋 )) one cande
déduit prove ∀𝑥car
𝜑 ↓ (𝑥).et In the
sontproof
des concepts use 𝛿
individuels
below, we :
the proof that 𝐸𝑥 (_) = "_ = 𝑥" (that is, “being equal to 𝑥”) is an individual concept.
97
δ.
.. [∀X(C(X) → ϕ (X))]
. ∀E
δ. x=x C(Ex ) C(Ex ) → ϕ (Ex )
.. →E
. Ex (x) ϕ (Ex )
∧I
C(Ex ) Ex (x) ∧ ϕ (Ex )
∧I
C(Ex ) ∧ Ex (x) ∧ ϕ (Ex )
∃2 I
∃X(C(X) ∧ X(x) ∧ ϕ (X))
:=
ϕ ↓ (x)
∀1 E
∀xϕ ↓ (x)
2. ∀𝑥 𝜓 (𝑥)qui
ne fonction
a) Assuming one signifie ∀𝑋 (𝐶(𝑋
can prove“est égal) →
à 𝜓x”.
↑ (𝑋Ici
)) on obtient E x
[C(X)]
:=
∀x∀y(X(x) ∧ X(y) → x = y) ∧ ∃x X(x)
∧E
∃xX (x) [X(x)] [∀xψ (x)]
∃1 E ∀1 E
X(x) ψ (x)
∧I
X(x) ∧ ψ (x)
1
∃ I
∃x(X(x) ∧ ψ (x))
:=
ψ ↑ (X)
→I
C(X) → ψ ↑ (X)
∀2 I
∀X(C(X) → ψ ↑ (X)
b) Finally assuming ∀𝑋 (𝐶(𝑋 ) → 𝜓 ↑ (𝑋 )) one can prove: ∀𝑥 𝜓 (𝑥)
δ.
.. [∀X(C(X) → ψ ↑ (X)]
. ∀2 E
C(Ex ) C(Ex ) → ψ ↑ (Ex )
→E
ψ ↑ (Ex )
:=
∃yEx (y) ∧ ψ (y)
∃1 E
Ex (y) ∧ ψ (y)
:=
y = x ∧ ψ (y)
∧E
ψ (x)
∀1 I
∀xψ (x)
98
3.3. First Order Existential Quantification as Existential Quantification Over
Non-empty Individual Concepts
As for the universal quantification, we have:
Proposition 2. First order existential quantification and second order quantification over individ-
ual concepts are equivalent:
1. when 𝜙 is a property of individual concepts, one has ∃𝑥 𝜑 ↓ (𝑥) ⇔ ∃𝑋 (𝐶(𝑋 ) ∧ 𝜑(𝑋 )) where
𝜑 ↓ (𝑥) ∶= ∃𝑋 (𝐶(𝑋 )∧ 𝑋 (𝑥) ∧ 𝜑(𝑋 )).
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. ∃𝑥 𝜑 ↓ (𝑥) ⇔ ∃𝑋 (𝐶(𝑋 ) ∧ 𝜑(𝑋 )) where 𝜑 ↓ (𝑥) ∶= ∃𝑋 (𝐶(𝑋 )∧ 𝑋 (𝑥) ∧ 𝜑(𝑋 )
a) Let us prove ∃𝑋 (𝐶(𝑋 ) ∧ 𝜑(𝑋 )) under the assumption ∃𝑥 𝜑 ↓ (𝑥).
Preuve.
[C(X) ∧ X(x) ∧ ϕ (X)] [C(X) ∧ X(x) ∧ ϕ (X)]
∧E ∧E
[ϕ ↓ (x)] C(X) ϕ (X)
:= ∃2 I
∃X(C(X) ∧ X(x) ∧ ϕ (X)) C(X) ∧ ϕ (X)
∃2 E
[∃xϕ ↓ (x)] ∃X(C(X) ∧ ϕ (X))
∃1 E
∃X(C(X) ∧ ϕ (X))
Ensuite
b) Now let usonprove ∃𝑥 prouver
souhaite 𝜑 ↓ (𝑥) under
l’implication ∃𝑋y(𝐶(𝑋
inverse : s’il
the assumption a un )concept
∧ 𝜑(𝑋 )).
individuel
We firstqui
need
𝛼, 𝛽, 𝛾 i.e. the three following proofs :
𝛼∶
[C(X) ∧ ϕ (X)]
∧E
[∃X(C(X) ∧ X(x) ∧ ϕ (X))] C(X)
∃2 E
: C(X)
𝛽∶
[C(X) ∧ ϕ (X)]
∧E
[∃X(C(X) ∧ X(x) ∧ ϕ (X))] ϕ (X)
2
∃ E
: ϕ (X)
99
𝛾∶
α.
..
.
C(X)
:=
∀x∀y(X(x) ∧Y (x) → x = y) ∧ ∃xX(x)
∧E
∃xX(x) [X(x)]
: X(x)
and the proof we are looking for is:
α. γ
.. ..
. .. β
..
C(X) X(x) ..
∧I
C(X) ∧ X(x) ϕ (X)
∧I
C(X) ∧ X(x) ∧ ϕ (X)
∃2 I
∃X(C(X) ∧ X(x) ∧ ϕ (X))
:=
ϕ ↓ (x)
↓ ∃1 I
∃xϕ (x)
2. ∃𝑥 𝜓 (𝑥) ⇔ ∃𝑋 (𝐶(𝑋 ) ∧ 𝜓 ↑ (𝑋 )) where 𝜓 ↑ (𝑋 ) ∶= ∃𝑥(𝑋 (𝑥) ∧ 𝜓 (𝑥))
a) Let us prove ∃𝑋 (𝐶(𝑋 ) ∧ 𝜓 ↑ (𝑋 )) under the assumption ∃𝑥 𝜓 (𝑥) – 𝛿 is the proof of
𝐶(𝐸𝑥tilise
) defined
ici inlathe
preuve vu pour le1. lemme 2 pour déduire C
proof of proposition
x = x [∃xψ (x)] [ψ (x)] 1
∃ E
δ. Ex (x) ψ (x)
.. ∧I
. Ex (x) ∧ ψ (x)
∃1 I
C(Ex ) ∃y(Ex (y) ∧ ψ (y))
δ. ∧I
.. C(Ex ) ∧ ∃y(Ex (y) ∧ ψ (y))
. :=
C(Ex ) ψ ↑ (Ex )
∧I
C(Ex ) ∧ ψ ↑ (Ex )
∃2 I
∃X(C(X) ∧ ψ ↑ (X)
100
e. us prove ∃𝑥 𝜓 (𝑥) under the assumption ∃𝑋 (𝐶(𝑋 ) ∧ 𝜓 ↑ (𝑋 ))
b) Let
[∃X(C(X) ∧ ψ ↑ (X))] [C(X) ∧ ψ ↑ (x)]
∃2 E
C(X) ∧ ψ ↑ (X)
∧E
ψ ↑ (X) [X(x) ∧ ψ (x)]
:= ∧E
∃x(X(x) ∧ ψ (x)) ψ (x)
1
∃ E
ψ (x)
∃1 I
∃xψ (x)
3.4. Dealing With Possibly Empty Individual Concepts
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 [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.
4.1. Generalised Quantifiers
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.
101
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⟩:
∀𝐶 (𝐶, 𝜑) ⟺ 𝐶 ⊂ 𝜑 ∃𝐶 (𝐶, 𝜑) ⟺ 𝐶 ∩ 𝜑 ≠ ∅
4.2. Branching Quantifiers
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 ex-
pressed 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 | ∃𝑓 ∃𝑔∀𝑥∀𝑦 (𝑥, 𝑓 (𝑥), 𝑦, 𝑔(𝑦)) ∈ 𝑅}
102
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 quanti-
fier 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:
(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
5
There is also a first-order reading of this sentence, which the ’each other’ (perhaps) makes less perceptible, and
which can be expressed within first-order logic: [∀𝑥∃𝑥 ′ ∀𝑦∃𝑦 ′ 𝑇 (𝑥) ∧ 𝐵(𝑦) → 𝑀(𝑥, 𝑥 ′ ) ∧ 𝑀(𝑦, 𝑦 ′ ) ∧ 𝐾 (𝑥 ′ , 𝑦 ′ )] ∧
[∀𝑦∃𝑦 ′ ∀𝑥∃𝑥 ′ 𝑇 (𝑥) ∧ 𝐵(𝑦) → 𝑀(𝑥, 𝑥 ′ ) ∧ 𝑀(𝑦, 𝑦 ′ ) ∧ 𝐾 (𝑥 ′ , 𝑦 ′ )]. According to Szymanik [25], in two-thirds of cases,
the first-order reading is preferred to the branching quantifier reading.
103
𝑦) 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:
Φ(𝐹 , 𝐺, 𝑥, 𝑥 ′ , 𝑦, 𝑦 ′ ) = [𝑇 (𝑥) ∧ 𝐵(𝑦) ∧ 𝐹 (𝑥, 𝑥 ′ ) ∧ 𝐺(𝑦, 𝑦 ′ )] → 𝐾 (𝑥 ′ , 𝑦 ′ )
and
Ψ(𝐹 , 𝐺) = [∀𝑥∃𝑥 ′ 𝑇 (𝑥) → 𝐹 (𝑥, 𝑥 ′ )] ∧ [∀𝑦∃𝑦 ′ 𝐵(𝑦) → 𝐺(𝑦, 𝑦 ′ )]
∧ [∀𝑥, ∀𝑥 ′ ∀𝑦∀𝑦 ′ Φ(𝐹 , 𝐺, 𝑥, 𝑥 ′ , 𝑦, 𝑦 ′ )]
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 :
[Ψ(𝐴, 𝐵)](1)
⋅
⋅
⋅
[∃𝐺Ψ(𝐴, 𝐺)](2) 𝜑
∃2 𝐸 (1)
∃𝐹 ∃𝐺Ψ(𝐹 , 𝐺) 𝜑
∃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.
6
Similarly, 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′ ∶ ∃𝐹 ∃𝐺[∀𝑥∃𝑥 ′ 𝑇 (𝑥) → 𝐹 (𝑥, 𝑥 ′ ) ∧ 𝑇 (𝑥 ′ )] ∧ [∀𝑦∃𝑦 ′ 𝐵(𝑦) →
𝐺(𝑦, 𝑦 ′ ) ∧ 𝐵(𝑦 ′ )] ∧ [∀𝑥∀𝑥 ′ ∀𝑦∀𝑦 ′ 𝑇 (𝑥) ∧ 𝑇 (𝑥 ′ ) ∧ 𝐵(𝑦) ∧ 𝐵(𝑦 ′ ) ∧ 𝐹 (𝑥, 𝑥 ′ ) ∧ 𝐺(𝑦, 𝑦 ′ ) → 𝐾 (𝑥 ′ , 𝑦 ′ )]
104
6. Conclusion
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 logic7 . 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.
Acknowledgments
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.
7
The formula 𝐴(𝜀𝑣 𝐵(𝑣)) is not equivalent to any first order formula — although it is equivalent to ∃𝑣 𝐴(𝑣) ∧ 𝐵(𝑣)
when additionally ∃𝑣 𝐵(𝑣) ≡ 𝐵(𝜀𝑣 𝐵(𝑣)) holds.
8
As 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 ∃𝑤∀𝑢 𝐵(𝑤) ∧ (𝐴(𝑢) ⟹ 𝐺(𝑢, 𝑤)).
105
References
[1] G. Frege, Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen
Denkens, Verlag von Louis Nebert, Halle, 1879.
[2] W. Kneale, M. Kneale, The development of logic, 3rd ed., Oxford University Press, 1986.
[3] W. D. Goldfarb, Logic in the twenties: The nature of the quantifier, J. Symb. Log. 44 (1979)
351–368. URL: https://doi.org/10.2307/2273128. doi:10.2307/2273128.
[4] D. Hilbert, P. Bernays, Grundlagen der Mathematik. Bd. 1., Berlin: Julius Springer. XII, 471
S., 1934. Traduction française de F. Gaillard et M. Guillaume, L’Harmattan, 2001.
[5] D. Hilbert, P. Bernays, Grundlagen der Mathematik. Bd. 2., Springer, 1939. Traduction
française de F. Gaillard, E. Guillaume et M. Guillaume, L’Harmattan, 2001.
[6] A. Mostowski, On a generalization of quantifiers, Fundamenta Mathematicae 44 (1957)
12–36.
[7] P. Lindström, First order predicate logic with generalized quantifiers, Theoria 32 (1966)
186–195.
[8] J. Barwise, R. Cooper, Generalized quantifiers and natural language, Linguistics and
Philosophy 4 (1981) 159–219. doi:10.1007/BF00350139.
[9] E. Keenan, J. Stavi, A semantic characterization of natural language determiners, Linguistic
and Philosophy 9 (1986) 253–326.
[10] D. Westerståhl, Generalized Quantifiers, in: E. N. Zalta (Ed.), The Stanford Encyclopedia
of Philosophy, Winter 2019 ed., Metaphysics Research Lab, Stanford University, 2019.
[11] R. Montague, The proper treatment of quantification in ordinary english, in: J. Hintikka,
J. Moravcsik, P. Suppes (Eds.), Approaches to natural language: proceedings of the 1970
Stanford workshop on Grammar and Semantics, Reidel, Dordrecht, 1973.
[12] D. van Dalen, Logic and Structure, Universitext, fifth ed., Springer-Verlag, 2013.
[13] J. Väänänen, Second-order and Higher-order Logic, in: E. N. Zalta (Ed.), The Stanford
Encyclopedia of Philosophy, Fall 2021 ed., Metaphysics Research Lab, Stanford University,
2021.
[14] R. Moot, C. Retoré, Classical logic and intuitionistic logic: equivalent formulations in
natural deduction, Gödel-Kolmogorov-Glivenko translation, 2016. arXiv:1602.07608.
[15] W. D. Goldfarb, The undecidability of the second-order unification problem, Theor.
Comput. Sci. 13 (1981) 225–230. URL: https://doi.org/10.1016/0304-3975(81)90040-2. doi:10.
1016/0304-3975(81)90040-2.
[16] L. Henkin, Completeness in the theory of types, J. Symb. Log. 15 (1950) 81–91. URL:
https://doi.org/10.2307/2266967.
[17] S. Rudolph, Foundations of description logics, in: A. Polleres, C. d’Amato, M. Arenas,
S. Handschuh, P. Kroner, S. Ossowski, P. F. Patel-Schneider (Eds.), Reasoning Web. Semantic
Technologies for the Web of Data - 7th International Summer School 2011, Tutorial Lectures,
volume 6848 of LNCS, Springer, 2011, pp. 76–136. doi:10.1007/978-3-642-23032-5\_2.
[18] S. Kripke, Identity and necessity, in: M. Munitz (Ed.), Indentity and Individuation, New-
York University Press, 1971, pp. 135–164.
[19] S. Kripke, Naming and necessity, in: D. Davidson, G. Harman (Eds.), Semantics of Natural
Language, Reidel, 1972, pp. 253–355.
[20] M. Fitting, R. Mendelsohn, First-Order Modal Logic, Springer Netherlands, 1998.
106
[21] R. Muskens, A theory of names and true intensionality, in: M. Aloni, V. Kimmelman,
F. Roelofsen, G. W. Sassoon, K. Schulz, M. Westera (Eds.), Amsterdam Colloquium 2011,
volume 7218 of LNCS/FoLLI, Springer-Verlag, 2012, pp. 441–449.
[22] S. Peters, D. Westerståhl, Quantifiers in Language and Logic, Clarendon Press, 2006.
[23] L. Henkin, Some remarks on infinitely long formulas, in: Infinitistic Methods: Pro-
ceedings of the Symposium on Foundations of Mathematics, Warsaw, 1959, Panstwowe
Wydawnictwo Naukowe / Pergamon Press, Warsaw, 1961, pp. 167–183.
[24] J. Hintikka, G. Sandu, Game-theoretical semantics, in: J. van Benthem, A. ter Meulen
(Eds.), Handbook of Logic and Language, North-Holland Elsevier, Amsterdam, 1996, pp.
361–410.
[25] J. Szymanik, Branching Quantifiers, Springer International Publishing, Cham, 2016, pp.
143–162. doi:10.1007/978-3-319-28749-2_9.
[26] S. Hetzl, A. Leitsch, D. Weller, CERES in higher-order logic, Ann. Pure Appl. Log. 162
(2011) 1001–1034. doi:10.1016/J.APAL.2011.06.005.
[27] M. Baaz, A. Lolic, Towards a proof theory for Henkin quantifiers, J. Log. Comput. 31 (2021)
40–66. URL: https://doi.org/10.1093/logcom/exaa071.
[28] J. Avigad, R. Zach, The epsilon calculus, in: E. N. Zalta (Ed.), The Stanford Encyclopedia
of Philosophy, Center for the Study of Language and Information, 2008. URL: http://plato.
stanford.edu/.
[29] S. Chatzikyriakidis, F. Pasquali, C. Retoré, From logical and linguistic generics to Hilbert’s
tau and epsilon quantifiers, IfCoLog Journal of Logics and their Applications 4 (2017)
231–255.
107