# Semantics and expressive power of generic element quantifiers

In real analysis (and other applications like the graph-theoretic structural approach to sparse matrices), it would sometimes be convenient to quantify over all generic elements. A generic element $\xi$ would basically satisfy $(\exists xf(x)\neq g(x))\to f(\xi)\neq g(\xi)$ for all functions $f$, $g$ relevant to the current context. So a generic element quantifier would be a kind of "last word" quantifier, i.e. it has to wait until all other context is laid down, before it can fix its meaning. But even as a "last word" quantifier, it seems to be more ambiguous and brittle then other "overly expressive" quantifiers like second order quantifiers or Henkin quantifiers.

Let's assume that the first order language (with equality) contains only function symbols, but no predicate symbols. Is it possible to give a semantics for generic element quantifiers in this case? If this shouldn't be possible in general, even in the weak sense of full semantics for second order quantifiers, then maybe it helps if we restrict the allowed models to $\mathbb R^n$?

If it is possible to give a semantics for generic element quantifiers, do they extend the expressive power of the corresponding logic significantly?

• At least for $\mathbb R^n$, an idea for a possible semantics just occurred to me. The interior of the set of all $\xi$ for which the proposition is true should be dense in $\mathbb R^n$. So this type of semantics might work as soon as the model is required to have a topology. Doesn't look too bad for the moment. Apr 27 '14 at 11:18

By Ηerbrand theorems all one can expect for an universal theory Γ:

     Γ |- ∃xP(x)


That we can find terms t1,..,tn such that:

     Γ |- P(t1) & ... & P(tn)


Herbrands theorem is for when predicate symbols exist. But I guess a function symbol can also act as a predicate symbol, if it is the characteristic function of a relation, and we would use f(x1,..,xn)=1 to express the predicate. So I guess banning predicates doesn't help.

On the other hand if you do something with the connectives and quantifiers in your theory Γ, you might get a so called existence property. For example intuitionistic logic has the existence property, but also Horn clauses classically.