[FOM] Standardization of sets, sorts, and free logic

[Anthony Coulter]

Dear Freek,

 > > But the Standard Library needs a Standard
 > > Logic, so "(1+1)/0 = 2/0" and "1/0 + 2 = 2 + 1/0" must
 > > each either be provable or not provable.

 > Isn't there a third possibility: both these statements
 > are ill-formed?  Or does that fall in your "not provable"
 > category?  But in that case the negation is not provable
 > either.

Ah, yes, that is also a possibility. But I don't think it corresponds
to regular practice. That is, I don't believe that most mathematicians
would consider formulas involving division by zero to be ill-formed.
Consider the following three sentences:

1)  all real x: x != 0 -> x/x = 1
2)  0 is real
3)  0 != 0 -> 0/0 = 1

If "0/0" is not a well-formed term, then (3) is not a well-formed
sentence and so is formally meaningless. But I believe most
mathematicians would accept both the well-formedness *and* the
correctness of the deduction. If you show those three lines to a
mathematician down your hall and ask if line (3) is meaningless,
you'll probably be told that "No, line (3) is right. It doesn't
matter whether 0/0 = 1 because the antecedent is false."

4) all real x: 1/(sqrt 3 + sin x + cos x) = 1 / (cos x + sin x + sqrt 3)
5) all real x: 1/(sqrt 2 + sin x + cos x) = 1 / (cos x + sin x + sqrt 2)

Sentence (4) is true, but sentence (5) entails division by zero at pi/4.
Does that mean sentence (5) is not well-formed? I was brought up to
regard "well-formedness" as a syntactic property, and these two
sentences are syntactically almost identical!

Meanwhile, think of the sophistication required for a computer to figure
out that sin(x) + cos(x) > -sqrt(2) for all x; we need both this fact
and the fact that sqrt(3) > sqrt(2) to show that the denominator in
sentence (4) is always nonzero. Proving that (4) is well-formed will
take more effort and ingenuity than proving that (4) is true! That seems
quite backwards to me.

Regards,
Anthony