5

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

Christopher King
  • 10,365

1 Answers1

6

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.

Noah Schweber
  • 245,398
  • Interesting. Do all the usual theorems of FOL apply (computability, completeness, incompleteness, etc...)? – Christopher King Mar 08 '18 at 22:37
  • Also, I'm guessing it strengthens set theory as well, right? – Christopher King Mar 08 '18 at 22:40
  • @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. – Noah Schweber Mar 08 '18 at 22:44
  • oh, it strengthens any theory then, right? – Christopher King Mar 08 '18 at 22:48
  • @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. – Noah Schweber Mar 08 '18 at 22:50