For a set of universally quantified variables $\{a_1,\dots,a_n\}$, let $\exists_{a_1,\dots,a_n} x. s$ mean that there exists $x$ depending on $a_1,\dots,a_n$ (and no other universally quantified variables) making $s$ true. That is, while evaluating a closed statement containing $\exists_{a_1,\dots,a_n} x. s$, we must find a closed predicate $p(x,a_1,\dots,a_n)$ such that we can replace $\exists_{a_1,\dots,a_n} x. s$ with $\exists!x.p(x,a_1,\dots,a_n) \land \exists x. (p(x,a_1,\dots,a_n) \land s)$ to make the statement true.

For example, $\forall x. \exists_x y. x < y$ is true (with the witness predicate $y=x+1$), but $\forall x. \exists_\emptyset y. x < y$ is false (since the witness predicate would need to fix $y$).

Using the language of arithmetic, does adding this quantifier make the language strictly more expressive, or can we express any statement with this quantifier without using this quantifier.

For example, given $\forall x. \forall y. \exists_x a. \exists_y b. p(x,y,a,b)$, it is not clear how we could express it in normal arithmetic, even if we are given a specific $p$.


1 Answer 1


Great question! This does indeed result in a strengthening of first-order logic.

Historically, the first example of this sort of thing was the notion of a Henkin (or branching) quantifier; it was further developed in Hintikka's independence-friendly logic and later, and I believe most generally, Vanaanen's dependence logic. Roughly speaking, dependence logic "is" the fragment of second-order logic consisting of formulas of the form $\exists F_1, ..., F_n\theta$ where $\theta$ is first-order: (in)dependence of first-order variables is captured by talking about the existence of appropriate Skolem functions. Interestingly, this is not closed under negation! Just because a sentence can be expressed using dependence logic does not mean that its negation is so expressible.

Vanaanen's book is I think the best source on this topic.

To see that branching quantifiers of this type do in fact yield a system which is strictly stronger than first-order logic, note that we can use them to write a sentence in the empty language which is true in exactly the infinite structures:

"There is a $z$ such that for every $x$ and every $y$, there are $u$ and $v$ depending only on $x$ and $y$ respectively such that $u=v\iff x=y$ and $z\not=u$."

This sentence describes an injection which is not a surjection, and is clearly not first-order expressible.

  • $\begingroup$ Interesting. Do all the usual theorems of FOL apply (computability, completeness, incompleteness, etc...)? $\endgroup$ Commented Mar 8, 2018 at 22:37
  • $\begingroup$ Also, I'm guessing it strengthens set theory as well, right? $\endgroup$ Commented Mar 8, 2018 at 22:40
  • $\begingroup$ @PyRulez Re: your first comment, compactness and Lowenheim-Skolem apply, but the former is weakened since dependence logic isn't closed under negation. Incompleteness holds a fortiori, and re: the others see here. I don't know what you mean by "strengthens set theory." The issue isn't about arithmetic, but the logical framework itself. $\endgroup$ Commented Mar 8, 2018 at 22:44
  • $\begingroup$ oh, it strengthens any theory then, right? $\endgroup$ Commented Mar 8, 2018 at 22:48
  • $\begingroup$ @PyRulez I'm not sure what you mean by "strengthens any theory." There are certainly sets of first-order sentences which remain complete even for dependence logic - e.g. the axioms for dense linear orders without endpoints. $\endgroup$ Commented Mar 8, 2018 at 22:50

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .