FOM: Branching quantifiers

[Marcin Mostowski]

-Raatikainen Panu answer to Andrzej Trybulec

 As I understand the use of "z" instead of "y" or vice versa is just
misspelling. It seems to me that the formula (x) (z) S(x,F(x),z,G(z)) gives
the meaning to the simplest Henkin quantifier in proof-theoretical context
than in the standard semantical way. It can be made clear when you look at
natural deduction systems for Henkin quantifiers (my paper "Relational
semantics for branched quantifiers", in "Mathematical Logic and its
applications", ed. D. Skordev, Plenum Press 1987, or the paper by
Lopez-Escobar, Fundamenta Mathematicae 1990 or 1992, another approach G.
Takeuti "Proof Theory"). I have discussed the topic with Andrzej Trybulec
many, many years ago. As I remember many years ago he has tried to implement
Henkin quantifiers in his Mizar system (proof-verification system, actually
very rich database for mathematics). Anybody knows what is going on with
this or similar attempts?

-- Joe Shipman doubts.

1. Horizontal composition is just superposition of prefixes - which is
trivial and first order definable, similarly as duallisation, but not in a
context of combining these operations with vertical composition.

2. Such a game quantifier seems to be equivalent to (x)(Ey)R(x,y) if you do
not put any serious restrictions.

Marcin Mostowski