[FOM] free logic

[Mitchell Spector]

I think you're right, Mario.  Instead of taking "x > y" to abbreviate "NOT(x <= y)", we should take 
it to abbreviate "(x is defined) & (y is defined) & NOT(x <= y)".  If we do that, everything works 
nicely.

Note, incidentally, that there's no problem with expressing "x is defined" here; we can regard "x is 
defined" as an abbreviation for "x = x".

Mitchell Spector




Mario Carneiro wrote:
>
>
> On Sun, Oct 25, 2015 at 9:24 PM, Mitchell Spector <spector at alum.mit.edu
> <mailto:spector at alum.mit.edu>> wrote:
>
>     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.
>
>
>
> I would put forward that this state of affairs is not as undesirable as you suggest. This issue also
> comes up in the plain ZFC approach to relations: Suppose that < is defined as a relation on R, that
> is, a subset of R x R. and similarly for <=. Then x > y <-> NOT(x <= y) is true when x and y are in
> R, but not generally. Is i < i (where i is the imaginary unit)? I would suggest that i < i be false,
> not undefined, and similarly for i <= i.
>
> With this interpretation of relations in untyped set theory, the Harvey's suggestion seems to fit
> naturally. (Consider also the possibility of what I call "reverse closure": If x R y for some
> relational predicate R, we can deduce that x and y are defined and in the domain of the relation,
> which simplifies the antecedents to theorems of the form x R y => A.)
>
> Mario