[FOM] Additional expressiveness of free logic

[Anthony Coulter]

Mario derives:
 > ...so in particular we have
 >    all real a,b: b != 0 -> exists real c: a = b*c   -- provable
 >    all real a,b: exists real c: b != 0 -> a = b*c   -- unprovable

This is a valid claim but it involves some sleight of hand that is
mechanically equivalent to a free logic. Your typed quantifiers are
governed by the rules:
   (all real x: P[x]) -> (t is real) -> P[t]
   (t is real) -> P[t] -> (exists real x: P[x])
which is exactly the same as Lambert-style free logic without all of
the strictness rules you see in alternative free logics, except that
"t exists" is now called "t is real." But you're still dividing the
space of terms into "real terms" and "non-real terms" and restricting
quantification to the real ones.

Free logic is necessary to get this behavior for untyped quantifiers.
Consider intuitionistic ZF without classes. (We'll add classes in a
minute.) Start with the valid claim that every nonempty set has an
intersection:

all A: ~empty[A] -> exists I: all x: x\in I <-> all y: x\in y -> y\in A

Since I is provably unique, we can define an intersection operator. Use
whichever definition you consider to be more fundamental:

    inter(A) = iota I: all x: x\in I <-> all y: x\in y -> y\in A
             = {x| all y: x\in y -> y\in A}

We can then derive the intuitionistically valid sentence:

   all A: ~empty[A] -> all x: x\in inter(A) <-> all y: x\in y -> y\in A

 From which we derive the intuitionistically *invalid* sentence:

all A: exists I: ~Empty[A] -> all x: x\in I <-> all y: y\in A -> y\in I

Switching to a larger domain by adding proper classes doesn't solve the
problem---I can still insist on using untyped quantifiers, only this
time they range over class variables instead of set variables. If you
take iota as a primitive, the invalid derivation works without
modifications.

If you take class comprehension as a primitive, you might be able to
argue that quantifiers occurring in P[x] in {x|P[x]} must be restricted
to sets. So then you can just forbid my original definition, and
require instead the nonproblematic:
     inter(A) = {x| all set y: x\in y -> y\in A}
for which "inter(emptyset)" is the class of all sets. But this is not a
general solution; it works only in ZF-like axiomatic systems where
everything is a set. Your proposed iota definition
     (iota x: P[x]) = union {y| {x|P[x]} = {y}}
involves taking the union of arbitrary objects; it cannot be used in
constructive systems like Heyting arithmetic or Bishop-style analysis.

Anthony