[FOM] Additional expressiveness of free logic

[Mario Carneiro]

On Wed, Oct 28, 2015 at 5:40 PM, Anthony Coulter <fom at anthonycoulter.name>
wrote:

> 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.
>

Indeed you are absolutely correct, and this even extends to the untyped
quantifiers, which are analogously governed by
  (all x: P[x]) -> (t in V) -> P[t]
  (t in V) -> P[t] -> (exists x: P[x])
where "t in V" is shorthand for "t exists" or "exists x: x = t" or "t is a
set". Since t is a class here this is not necessarily a trivial assertion.
I have spent much of my time reading the free logic debate trying to figure
out how this "Is[t]" differs from "t in V" as it is defined in this system.

Of course unconditional existence of iota is apparently considered a bad
thing by free logic advocates, whereas the my definition gave naturally
existence in V. Perhaps these folks will prefer the definition of
restricted iota:

  iota x in A: P[x] = if Exu x in A: P[x] then iota x: (x in A /\ P[x])
else Undef(A)

where Undef(A) is an "anti-choice operator" satisfying Undef(A) not in A.
With this definition, (iota x in A: P[x]) in A iff Exu x in A: P[x], which
makes it even more like Lambert's iota. (Unfortunately the forward
implication is not intuitionistically valid - in needs a NOT NOT in the
consequent.)

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.
>

You have correctly predicted my counterargument here. In my case we do
indeed have inter(A) = {x| all y: x in y -> y in A}, but the unrestricted
quantifier only ranges over sets (this is ZF+classes, not NBG). Thus we do
have
  all A: ~empty[A] -> all x: x\in inter(A) <-> all y: x\in y -> y\in A
but not
  all A: exists I: ~Empty[A] -> all x: x\in I <-> all y: y\in A -> y\in I
because, following the rule I mentioned above, this would require proving
inter(A) in V, which is not possible unconditionally (even in classical
ZF). (In fact, I don't even think it is intuitionistically provable under
~empty[A] but only under inhabited[A] since we need an explicit upper bound
to apply separation.)

So by comparison to the terminology of the free-logic advocates, proper
classes are not "non-denoting" - they are quite meaningful, and in
particular A = B and A in B make sense even when A and B are not sets; and
the only one of these which is forced false is A in B when A is a proper
class. Neither is A = B always true when both A and B are proper classes,
for example, On =/= V (where On is the class of ordinals). On the other
hand, all quantifiers ignore proper classes - all x: P[x] ranges over only
sets and all x in A: P[x] is just shorthand for all x: (x in A -> P[x]) -
which looks similar to the free logic approach.


> 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.
>

This is true - it should be emphasized that this is only for first-order
logics where there is at least some approximation of set theory to make
sense of the union operation. Most type theories or higher order logics
have their own approach to iota, where it is usually taken as axiomatic or
derived from epsilon (the indefinite choice operator, i.e. global choice).

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20151029/c0394175/attachment.html>