[FOM] Regarding strictness

[Anthony Coulter]

In this post I use the notation "Is[t]" to assert that "t exists". I
use the notation "s ~ t" for what in TeX would be $s\simeq t$---the
fancy tilde-equality that everyone defines as (Is[s] & Is[t]) -> s = t.
I use the word "strict" as follows:

If a strict relation R is true, then its arguments must all exist:
    R[x,y,z] -> Is[x] & Is[y] & Is[z]
If a strict function f exists, then its arguments must all exist:
    Is[f(x,y)] -> Is[x] & Is[y] & Is[z]

Equality is "substitutive" if these schemas hold for all s, t, f, and P
regardless of any existence considerations:
    t = t
    s = t -> f(s) = f(t)
    s = t -> P[s] -> P[t]

It is a simple fact that equality cannot be both strict and
substitutive. Proof:
  - For strict equality, 1+1=2 -> (1+1)/0 = 2/0.
  - For substitutive equality, (1+1)/0 = 2/0 -> Is[2/0].
  - Then 1+1=2 -> Is[2/0], which is clearly false.

Dr's Farmer and Friedman (and probably many others) handle this by
choosing the "real, fundamental" equality to be strict, and by
creating a second equality, defined by
    s ~ t <-> ((Is[s] or Is[t]) -> s = t)
which is substitutive. I don't like this solution for two reasons:

1. When I took calculus in school we had only one equal sign to worry
    about. I'm looking through my 3rd edition Spivak and I don't see
    any discussion about there being a second equality relation. So I'm
    skeptical that "the traditional approach to undefinedness" really
    involves two distinct notions of equality.
2. Tilde-equality doesn't even solve all of your problems. To evaluate
    a limit you might derive
      (x^2 - 4)/(x-2) = (x+2)*(x-2)/(x-2) = x+2
    under the explicit assumption that x != 2. Replacing regular
    equality with tilde-equality will *not* let you drop the explicit
    "x != 2" assumption because "(x+2)*(x-2)/(x-2) ~ x+2" is false.

A logic with two equalities is (to me, at least) almost as bad as a
logic with three truth values. Why have two? Clearly substitutivity is
important to all of us; that's why you created tilde-equality. But
then, why not take tilde-equality as primitive and define plain
equality as "a = b <-> a~b & Is[a] & Is[b]" ? From this perspective,
plain equality looks kind of silly (it's just a way to combine
existence and equivalence statements into a single symbol) and can be
dropped; now you're left with a tilde-equality which we can write with
regular "=" notation since it's the only equality left. But now your
equality is equivalent to mine (which I took from Lambert) except that
you have the extra rule that all nonexistent terms equal each other.

A single substitutive, non-strict equality is plenty.

For what it's worth, I do see one advantage to strict functions: you
can define the domain of "f(x) = 2 + 1/x" as the set {x: Is[2+1/x]}
like you would expect and then prove that 0 is not in the domain.
If functions were not strict, then the fact that ~Is[1/0] would be
insufficient to prove that ~Is[2+1/0]. (You would still be able to
prove that all nonzero numbers are in the domain, but you would not
be able to prove either "0\in dom(f)" or its negation.) I can agree
that this could be a problem. But on the other hand, Donald Knuth is
fond of using what he calls "multiplication by a strong zero" whereby
0*x = 0 even when x is undefined (usually because x is an expression
that diverges to infinity). I also believe that sometimes it's
convenient to extend the number systems. Maybe you want to define 1/0
as a projective point at infinity. If your axioms have already proven
that ~Is[1/0] then you have to create a new number system from scratch.
But if the existence of 1/0 is undecidable in your base theory, you can
add "1/0 = projectiveinfinity" and "Is[projectiveinfinity]" as axioms
without any trouble at all.

Regards,
Anthony