FOM: New quantifiers

[Joe Shipman]

Mostowski:

>You take the following composition rules
> 1. for each variable x, the following are prefixes: Ex, Ax;
> 2. if Q and Q' are prefixes then the following are prefixes: (QQ') -
>horizontal composition, (Q/Q') - vertical composition, and Q^d - the
>dualization of Q.

> The dualization means that Q^d is equivalent to ~Q~, which trivially
is
>first-order definable, but not in a context of vertical compositions.
> Without dualization you will get the logic with Henkin quantifiers,
but with
>dualization you will obtain just the logic equivalent to the second
order
>logic.

Shipman:

> Can someone please give an ordinary-language semantic
> interpretation of these quantifiers?  I don't understand  what
> they're supposed to mean.

Raatikainen:

>This can be easily done with Skolem functions. If you have an
>ordinary first order sentence
>(x)(Ey)(z)(Eu) S(x, y, z, u)
>the corresponding Skolem function form is
>(Ef)(Eg)(x)(z) S(x, f(x), z, g(x, z)),
>i.e. the last existential quantifier depends on the both earlier
>unversal quantifiers. What if one would like to have it depend only
>on the first. This cannot be expressed in the standard FO logic.
>But it can be expressed by Henkin (branching, or partially ordered)
>quantifier:
>
>(x)(Ey)
>              S(x, y, z, u)
>(z)(Eu)
>
>The Skolem function form of this is:
>
>(Ef)(Eg)(x)(z) S(x, f(x), z, g(z)).

This explains vertical composition but what about horizontal
composition?

Another question: What kind of expressive power do you get with a "game"
quantifier?  This would assert that the 2-player game played on a binary
formula where you have to pick X_n such that Phi(X_(n-1),X_n) holds, and
lose if you can't find one, is a win for the first player.  [This isn't
quite right, you need to initialize somehow so that the first move isn't
unrestricted].

-- Joe Shipman