Does specifying which variables depend on which other variables strengthen arithmetic?

Question

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$.

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.