[FOM] free logic

[Harvey Friedman]

There has been discussion of how to handle undefined terms in the
formalization of mathematics.

I have stated my views in one form or another perhaps half a dozen
times on the FOM and a few times recently.

Now that there is a focus on this, let me elaborate a bit on it again.

1. Mathematicians have good instincts about this, but are not normally
interested in being systematic and entirely consistent. They just want
to make sure that there is no practical ambiguity in what they write.

2. I have practiced a particular way of dealing with undefined terms
for many decades and am totally convinced that from the formalization
of mathematics point of view, which does not include any
considerations about Provers, that there is an optimally simple
systematic way of handling this. Furthermore, that this would also be
the easiest and most friendly *systematic* solution for the general
mathematical community, and that they would easily accept it as the
Gold Standard if they were compelled to endorse a Gold Standard.

3. This way of handling undefined terms is not due to me. I don't know
what credit should be assigned to it. It comes also with the entirely
appropriate and obvious Completeness Theorem. It can be done first in
one sorted predicate calculus with equality, and then extended to many
sorted predicate calculus with or without equality in obvious ways.

4. So I will only talk about one sorted predicate calculus with
equality. I will proceed semiformally. There is no problem being fully
formal.

5. In addition to =, there is ~ and uparrow and downarrow. There is no
such thing as "the undefined element".

6. We have constants, relation symbols, function symbols.

7. s = t means that the terms s,t are defined and have the same value.

8. s ~ t means that the terms s,t are either both undefined or both
defined with the same value.

9. s uparrow means s is undefined. s downarrow means s is defined.

10. Variables are always defined. I.e., we have x downarrows.
Constants are always defined. I.e., we have c downarrows.

11. All atomic formulas are true or false. There is no such thing as
an undefined atomic formula, or an undefined truth value. In fact,
there is no explicit notion of truth value other than what is
represented if we are using the absurdity symbol. (absurdity indicates
false, and absurdity --> indicates true). However, that is a
propositional calculus matter, and is optional.

12. A term other than a variable or a constant, is defined if and only
if all of its subterms are defined. E.g., 1/0 - 1/0 is not defined for
x = 0.

13. There is the usual implicit assumption that there is at least one
thing in the domain.

14. forall x  blah blah blah, means, of course, that for all actual
existing elements of the domain, x, such that blah blah blah.

15. therexists x blah blah blah, means, of course, that there is an
actual existing element of the domain, x, such that blah blah blah.

16. Examples. 1/0 - 1/0 <= 1/0 - 1/0 is false. 1/0 - 1/0 = 1/0 - 1/0 is false.

Harvey Friedman