[FOM] free logic

[Anthony Coulter]

Harvey raises an excellent point about the necessity of choosing a free
logic that is systematic and internally consistent. He has provided his
system; for contrast, I provide my complete system, which I pretty much
lifted from Karel Lambert.

In addition to some obvious notations, I also use:
  Is[x]          x exists. (This is "s uparrow" in Harvey's notation.)
  Exi x: P[x]    There exists an x such that P[x]
  Exu x: P[x]    There exists a unique x such thatP P[x]
  Iota x: P[x]   The unique x for which P[x]; this is the definite
                 description operator.

I take the usual axioms of regular (nonfree) predicate logic, remove
the standard All-elimination and Exi-introduction (which I will replace
with new versions below), and add the axiom schemes:

1.  All x: Is[x]
2.  (All x: P[x]) -> Is[t] -> P[t]
3.  Is[t] -> P[t] -> Exi y: P[y]
4.  t = t
5.  s = t -> f(s) = f(t)
6.  s = t -> P[s] -> P[t]
7.  (Exu x: P[x]) -> P[Iota x: P[x]]
8.  (Exu x: P[x]) <-> Is[Iota x: P[x]]
9.  (All x: P[x] <-> Q[x]) -> (Iota x: P[x]) = (Iota x: Q[x])

If you remove axiom 9, this system is provably equivalent to Karel
Lambert's minimal free description theory. Of note:
   "Exi x: Is[x]" is NOT provable. (Nonempty domains are possible)
   "Is[t] <-> Exi y: t = y" is provable.
   "1/0 = 1/0" is an instance of axiom scheme (4)
   "1+1 = 2 -> (1+1)/0 = 2/0" is an instance of (5)
   Division is intended to be defined by "a/b = Iota c: a = b*c".
   "~Is[1/0] -> ~Is[f(1/0)]" is not provable. (If you want f(x) to exist
     only when f does, you have to postulate that fact separately.)

Lambert was unenthusiastic about my axiom 9 because it led to results
he considered absurd, e.g.
   (Iota x: x != x) = (Iota x: x != x & Is[x])
That is, "the unique object which doesn't equal itself is the same as
the unique object which doesn't equal itself *and also exists.*" There
is nothing paradoxical about this statement; neither object exists so
we don't get any contradictions. But as a philosopher, Lambert found
this line of reasoning unsatisfactory.

I added axiom 9 anyway because you need it to prove things like:
   (Iota x: 2 = 0*x) = (Iota x: 0*x = 2)
It would be very annoying (and unsystematic, as Harvey would note) if
the above formula were not provable when the below formula is:
   (Iota x: 1+1 = 0*x) = (Iota x: 2 = 0*x)

In early versions of my system I weakened axiom 8 to the one-way
8b. (Exu x: P[x]) -> Is[Iota x: P[x]]

until I realized that the strong form is needed to prove that
   Is[lim_{x->c} f(x)] -> (All epsilon > 0: Exi delta: ...)
after all the definitions are expanded out.

It looks like the differences between my system and Harvey's are:
A. I have a single equality relation; Harvey has two. (Note that axioms
    (4), (5), and (9) above make my equality ALWAYS support subformula
    substitution. Harvey's "=" does not have this property though, with
    all the rules taken together, it appears that "~" does. I informally
    believe that my/Lambert's rules are more systematic than Harvey's;
    this claim is open to debate.)
B. I do not follow the convention that Is[f(x)] -> Is[x] or that
    P[x] -> Is[x] for all atomic functions and relations f and P; I also
    allow people to define atomic constants which do not exist. But
    this isn't an incompatibility---my system is strictly weaker than
    his, so users can add these principles as non-logical axioms if they
    so desire.
C. I don't assume a nonempty domain. (But as with (B), people can still
    postulate the existence of various objects as proper axioms.)
D. My system also has a completeness theorem, but it is complete with
    respect to a different semantics. See B. C. van Fraassen's
     Zeitschrift fur mathematische Logik und Grundlagen der
       Mathematik 12 (1):219-234 (1966).

I would like also to mention that my system has some nice eliminability
properties; any Iota-terms which occur transiently in a proof but which
are not subterms of the assumptions or the conclusion can be
systematically removed from the proof. My addition of axiom 9 to
Lambert's system does not appear to compromise this result.

Anthony