[FOM] Additional expressiveness of free logic

[Anthony Coulter]

 > Advocates of free logics really have to prove that they can deliver
 > useful additional expressiveness without imposing unreasonable costs.

Free logic is required if you want to support partial functions on
undecideable domains in intuitionistic logic. See:
   http://cs.nyu.edu/pipermail/fom/2015-September/019169.html

The gist of the problem is that if you wanted to formalize Errett
Bishop's book "Constructive Analysis," you would run into a problem
because these two sentences are NOT intuitionistically equivalent:

    all real a,b: b != 0 -> exists c: a = b*c   -- Weaker (and true)
    all real a,b: exists c: b != 0 -> a = b*c   -- Stronger (and false)

The trouble is that if (a/b) always exists (even in places where it is
undefined), then the stronger sentence is an immediate consequence of:

    all real a,b: b != 0 -> a = b*(a/b)

This is the reason I was finally won over by free logic. While I'm not
a diehard intuitionist, I do see value in being able to distinguish
constructive proofs from nonconstructive ones. Usually in mathematics
it is fairly easy to tell when a nonconstructive step is taken: modern
etiquette is to shout loudly whenever you invoke the axiom of choice,
and proofs by contradiction are easy to spot. But this existential
leakage problem is insidious---the only way to be sure it hasn't
infected your proof is to go back and re-check your quantifier rules
to make sure that you didn't assume something existed when it didn't.
Free logic just forces you to do this checking from the beginning.

So that's the additional expressiveness free logic buys you:
compatibility with intuitionism. What's the cost? That depends on your
choice of free logic. I've seen some very complicated systems in this
discussion, but the standard free logic developed by Lambert isn't
so bad. It's axiomatized here:
   http://cs.nyu.edu/pipermail/fom/2015-October/019270.html

I don't consider the cost here to be very high:
1. Conceptually, you can rationalize existence as "just another type";
    you can pretend that the quantifier "All real x:" really means
    "All existing real x:"). Then the only differences between existence
    and any other type are that (1a) existence is mandatory; you are not
    allowed to quantify over nonexistent objects and (1b) because it is
    mandatory you never have to explicitly write it.
2. Mechanically, you can implement existence as just another type, too.
    Suppose that you are working in a system where the underlying sort
    for your variables is a strict superset of the reals (so that the
    bare expression "All z: P[z]" involves more than just reals---e.g.
    complex numbers, and so inferring P[t] from "All real x: P[x]"
    requires a bit of work to prove that t is real). Then proving that
    a complex expression like (a+b*sin(x))/(a+c) exists is exactly as
    difficult as proving that it is real; you can use the same automation
    to check both of these claims.
3. Metalogically, free logic is *almost* a strict subset of regular
    logic. That is, if you set things up carefully, you will *almost*
    never be able to prove ~Is[t] for any term t. (So you can prove
    neither "Is[1/0]" nor its negation.) So you are free to imagine that
    existence is really just a constructive concept---that in "classical"
    logic there is an axiom scheme which asserts that everything exists
    (even 1/0, though it is still *undefined*) but that in your proof
    checker you only have the ability to prove that some things exist.

I say "almost" for point (3) because one of the axioms in the referenced
post breaks this property for the whole system. Axiom (8) [in the linked
post] follows Lambert in requiring that Is[Iota x: P[x]] (which says
that the unique object with property P exists) imply "Exu x: P[x]"
(which says that there is a unique object with property P). This axiom,
unfortunately, makes it possible to prove that some terms do not exist.
But this axiom can be weakened to (8b) [also in the linked post, but
further down], and point (3) [from this post] holds in the weakened
logic.

How would you feel about that? Any formula which is provable in
intuitionistic/free logic would also be provable in classical/nonfree
logic, and the only two differences between the two are that in
classical/nonfree logic, the law of the excluded middle holds and
everything is assumed to exist. Now the costs would be paid only by
people who want to pay them, because they want to track their use of
nonconstructive reasoning.

Anthony