FOM: Branching quantifiers

[Marcin Mostowski]

A few comments about the discussion:

- Raatikainen Panu  claims that the equivalence of SOL (second order logic)
with LBD (Henkin quantifiers with duallization) requires AC. It is not true.
The proof was given by me without AC see the papers mentioned (survey MK&MM
"Henkin Quantifiers", and MM "Quantifiers definable by second order means",
both in "Quantifiers" Kluwer 1995).

- A. P. Hazen has listed a few nonelementary quantifiers. All of them are
essentially weaker than Henkin quantifiers. Then they cannot give the power
of second order logic, but only a little of it. There is a frequent habit of
calling some nonelementary logics by "sublogics of SOL". However frequently
they have their own - independent of SOL - intuitive meaning. I think this
is so with Henkin quantification. Why we do not treat first order logic in
this way?

- In general Henkin quantifiers also do not give the power of full SOL,
therefore you should add duallization operator to obtain the full power.

- Raatikainen Panu gave a good exlanation of semantics for Henkin
quantifiers. I can that if you use phrases like "there is ... dependent on
.." nad "there is ... independent of ...", and similar in your quantifier
prefixes then you use Henkin quantifiers. So they were not invented by
Henkin, but they were discovered by Henkin.

- I appreciate very much Quine, but his remark that "existence of a complete
proof procedure is a necessary condition of logicalness" cannot be treated
as an argument. It can be treated only as a terminological proposal for
which theories can be called logics. E.g. first order logic enriched by the
quantifier "there is uncountably many" is a logic because it has
quantification only for first order variables and a complete proof
procedure, but Henkin quantifiers go beyond logic because they have no
complete proof procedure. It seems to me quite arbitrary.
Cezary Cie{\'s}li{\'n}ski, a few years ago at my seminar, proposed an
interpretation of Quine's claim, but very far from the spirite of Quine. The
idea is that otherwise there were no psychological mechanisms potentially
recognizing validity of logical inferences. However we can still ask why
such a mechanism should work for ALL valid inferences? Why it should be
complete?
For instance I have defined the proof system for the logic with Henkin
quantifiers (for references see the papers mentioned). It is complete only
relatively to some weaker semantics. Again, why completeneness is useful we
know, but why it should be necessary for logics - I do not know.

Marcin Mostowski