[FOM] free logic

[Rob Arthan]

> On 26 Oct 2015, at 23:59, Harvey Friedman <hmflogic at gmail.com> wrote:
> 
> 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}
> 

And the fact that Neil Tennant quickly responded with he suggestion
that set displays should be defined as syntactic abbreviations for set
comprehensions so {1/0, 2} would be equal to {2} is a nice illustration
of the following point of mine:

>> [the free logic approach] requires what someone (Fred Brooks?) called the "language lawyers”
>> to be brought in to pontificate on arcana like “{x | x = 1/0 \lor x = 2} = {1/0, 2}”
>> which depend on the fine details of how the language designers have chosen to
>> define the set display construct.
> 


That said, I am much less averse to the free logic approach than i have
been in the past. I do think it’s important to be able to give a simple intuitive
account of how undefinedness propagates. The intuition should be
that any term involving an undefined term is undefined unless there is
some quantification around it that traps the undefined case. Syntactic
abbreviations that introduce hidden bound variables are then going to be
a source of considerable confusion and should be avoided. So I support
Harvey’s proposal that an n-element set display should be an application of
an n-ary function symbol.

>> 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”.

I was thinking of x and y as metavariables for possibly undefined terms.
Surely:

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

is not true in the free logic approach?

> …
> 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.

I agree. Presumably, you avoid the need for an undefined
element in the semantics for free logic by making the semantic
valuation function for terms a partial function?

Regards,

Rob.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20151028/c90d05ca/attachment-0001.html>