[FOM] free logic

[Harvey Friedman]

An important component in this is the handling of atomic formulas. The
special atomic formulas use

=
~
uparrow
downarrow

This are right at the core of the free logic idea.

All of the other atomic formulas are treated as follows. they are
automatically false unless all of the component terms are defined.

This causes no difficulties as long as term substitution is done
properly. Term substitution requires the guard that the term used for
substitution is defined.

E.g., of course one has

(forall x,y)(x < y iff not (x >= y)).

We do have

1/0 - 1/0 < 1/0 - 1/0
1/0 - 1/0 >= 1/0 - 1/0

are both false. But that is not a problem since to create a problem,
we need to substitute for x,y, the term 1/0 - 1/0, and this term is
undefined.

Everything is very much under control with this semantically crustal
clear way of doing free logic.

Harvey Friedman

On Sun, Oct 25, 2015 at 9:24 PM, Mitchell Spector <spector at alum.mit.edu> wrote:
> 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
>>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom