[FOM] free logic

[Mitchell Spector]

Harvey Friedman wrote:
> There has been discussion of how to handle undefined terms in the
> formalization of mathematics.
> ...
>
> 16. Examples. 1/0 - 1/0 <= 1/0 - 1/0 is false.
 > ...



I'm trying to see how you're handling atomic formulas with relation symbols here.

It appears that you are taking <= to be a relation symbol of your language, and then applying the 
following principle:
if R is an n-place relation symbol, if t1, ..., tn are terms, and if at least one of t1, ..., tn is 
undefined, then R(t1, ...., tn) is false.

But if this is what you're doing, it has an unfortunate consequence.  Specifically, consider the 
formula 1/0 - 1/0 > 1/0 - 1/0.

If > is taken to be a relation symbol of the language also, then 1/0 - 1/0 > 1/0 - 1/0 is false.

But if x > y is taken to be an abbreviation for NOT(x <= y), then 1/0 - 1/0 > 1/0 - 1/0 is true.


This seems like an undesirable state of affairs.


The issue may be related to the fact the equality relation has been accorded the two varieties = and 
~, but other relation symbols haven't been accommodated with similar variants.


Mitchell Spector
E-mail: spector at alum.mit.edu




>
> Harvey Friedman
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>