In
logic a branching quantifier,
also called a Henkin quantifier, finite partially ordered quantifier or even nonlinear quantifier, is a partial ordering
:
of
quantifiers for ''Q'' ∈ . It is a special case of
generalized quantifier. In
classical logic
Classical logic (or standard logic or Frege-Russell logic) is the intensively studied and most widely used class of deductive logic. Classical logic has had much influence on analytic philosophy.
Characteristics
Each logical system in this class ...
, quantifier prefixes are linearly ordered such that the value of a variable ''y
m'' bound by a quantifier ''Q
m'' depends on the value of the variables
: ''y''
1, ..., ''y''
''m''−1
bound by quantifiers
: ''Qy''
1, ..., ''Qy''
''m''−1
preceding ''Q
m''. In a logic with (finite) partially ordered quantification this is not in general the case.
Branching quantification first appeared in a 1959 conference paper of
Leon Henkin. Systems of partially ordered quantification are intermediate in strength between
first-order logic and
second-order logic. They are being used as a basis for
Hintikka's and Gabriel Sandu's
independence-friendly logic.
Definition and properties
The simplest Henkin quantifier
is
:
It (in fact every formula with a Henkin prefix, not just the simplest one) is equivalent to its second-order
Skolemization, i.e.
:
It is also powerful enough to define the quantifier
(i.e. "there are infinitely many") defined as
:
Several things follow from this, including the nonaxiomatizability of first-order logic with
(first observed by
Ehrenfeucht
Andrzej Ehrenfeucht (, born 8 August 1932) is a Polish-American mathematician and computer scientist.
Life
Andrzej Ehrenfeucht formulated the Ehrenfeucht–Fraïssé game, using the back-and-forth method given in Roland Fraïssé's PhD thesis. ...
), and its equivalence to the
-fragment of
second-order logic (
existential second-order logic)—the latter result published independently in 1970 by
Herbert Enderton and W. Walkoe.
The following quantifiers are also definable by
.
[
* Rescher: "The number of ''φ''s is less than or equal to the number of ''ψ''s"
::]Lindström quantifier In mathematical logic, a Lindström quantifier is a generalized polyadic quantifier. Lindström quantifiers generalize first-order quantifiers, such as the existential quantifier, the universal quantifier, and the counting quantifiers. They were ...
.[
]
Relation to natural languages
Hintikka in a 1973 paper advanced the hypothesis that some sentences in natural languages are best understood in terms of branching quantifiers, for example: "some relative of each villager and some relative of each townsman hate each other" is supposed to be interpreted, according to Hintikka, as:
: \begin\forall x_1 \, \exists y_1\\ \forall x_2 \, \exists y_2\end V(x_1) \wedge T(x_2)) \rightarrow (R(x_1,y_1) \wedge R(x_2,y_2) \wedge H(y_1, y_2) \wedge H(y_2, y_1))
which is known to have no first-order logic equivalent.[
The idea of branching is not necessarily restricted to using the classical quantifiers as leaves. In a 1979 paper, Jon Barwise proposed variations of Hintikka sentences (as the above is sometimes called) in which the inner quantifiers are themselves generalized quantifiers, for example: "Most villagers and most townsmen hate each other."][ Observing that \Sigma_1^1 is not closed under negation, Barwise also proposed a practical test to determine whether natural language sentences really involve branching quantifiers, namely to test whether their natural-language negation involves universal quantification over a set variable (a \Pi_1^1 sentence).]
Hintikka's proposal was met with skepticism by a number of logicians because some first-order sentences like the one below appear to capture well enough the natural language Hintikka sentence.
: forall x_1 \, \exists y_1 \, \forall x_2 \, \exists y_2\, \varphi (x_1, x_2, y_1, y_2)\wedge forall x_2 \, \exists y_2 \, \forall x_1 \, \exists y_1\, \varphi (x_1, x_2, y_1, y_2)/math>
where
: \varphi (x_1, x_2, y_1, y_2)
denotes
: (V(x_1) \wedge T(x_2)) \rightarrow (R(x_1,y_1) \wedge R(x_2,y_2) \wedge H(y_1, y_2) \wedge H(y_2, y_1))
Although much purely theoretical debate followed, it wasn't until 2009 that some empirical tests with students trained in logic found that they are more likely to assign models matching the "bidirectional" first-order sentence rather than branching-quantifier sentence to several natural-language constructs derived from the Hintikka sentence. For instance students were shown undirected bipartite graph
In the mathematical field of graph theory, a bipartite graph (or bigraph) is a graph whose vertices can be divided into two disjoint and independent sets U and V, that is every edge connects a vertex in U to one in V. Vertex sets U and V are ...
s—with squares and circles as vertices—and asked to say whether sentences like "more than 3 circles and more than 3 squares are connected by lines" were correctly describing the diagrams.[
]
See also
* Game semantics
* Dependence logic
* Independence-friendly logic (IF logic)
* Mostowski quantifier
* Lindström quantifier In mathematical logic, a Lindström quantifier is a generalized polyadic quantifier. Lindström quantifiers generalize first-order quantifiers, such as the existential quantifier, the universal quantifier, and the counting quantifiers. They were ...
* Nonfirstorderizability
References
{{reflist
External links
Game-theoretical quantifier
at PlanetMath.
Quantifier (logic)