[FOM] free logic

[Harvey Friedman]

Rob's example

{x | x = 1/0 or x = 2} = {1/0, 2}

is a nice illustration of what I am talking about in free logic. The
above is false. The reason is that what is on the left side is
defined, but what is on the right side is undefined. This is because
1/0 is undefined, and for a term to be defined, all component terms
must be defined. That's true about any operation whatsoever. The
following is correct:

{x | x = 1/0 or x = 2} = {2}

On Mon, Oct 26, 2015 at 5:08 PM, Rob Arthan <rda at lemma-one.com> wrote:
>
>> On 26 Oct 2015, at 07:36, Mitchell Spector <spector at alum.mit.edu> wrote:
>>
>> 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.
>
> This also falls out in the wash if (working with set theory with \in as the only non-logical symbol)
> you take "x > y” to abbreviate "(x, y) \in (>)”.
>
> This free logic approach to undefined terms is not unknown in computer science:
...

> The most obvious place where it backfires is that "x > y” and “\lnot x \le y”
> don’t mean the same thing, which people find surprising.

x > y and not (x <= y) do mean the same thing.

(forall x in R)(x > y iff (not (x <= y)))

is certainly true. If by "mean" you mean something else, then of
course they don't "mean" the same thing. This is not any kind of
"backfiring".

Once again, I emphasize what best fits mathematical thinking and
mathematical practice, among mathematicians who want to engage in
absolute rigor. Computer Science and Provers may have some different
agendas.

I should mention that having an "undefined element" - which the
version of free logic I am advocating does not - might serve some CS
and Prover agendas, but is a non starter for mathematicians - at least
at the fundamental level. Mathematicians are obviously free to invent
some setup on top of free logic ZFC, with actual undefined elements as
they desire.

Harvey Friedman