FOM: New quantifiers
Joe Shipman
shipman at savera.com
Fri Mar 16 12:43:52 EST 2001
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
More information about the FOM
mailing list