[FOM] On definitions of terms, and free logic---a quick follow-up

[Harvey Friedman]

I will be spelling out a lot of details in how I recommend the
formalization of mathematics proceed beyond what I have written in

http://www.cs.nyu.edu/pipermail/fom/2015-October/019240.html
http://www.cs.nyu.edu/pipermail/fom/2015-October/019281.html

in a lot more detail, and one of the main issues is the handling of
the many faces of {blah blah blah} - i.e., the braces.

One of the multiple faces of the braces is its use as an
indefinite-ary function symbol. (Another separate role is its use as
an abstraction operator).

The use of indefinite-ray function symbols is of essential importance
in mathematics. The most famous example of an indefinite-ary function
symbol is +. (Another issue that must be addressed, is + on what? How
do we indicate what the what is?)

As an indefinite-ary function symbol,braces behaves for each n, like
any other function symbol in free logic - e.g., +. Of course, this
particular one, in set theory, has the property that for all
arguments, it is defined. But at any undefined argument(s) it is
undefined, just like +. (Of course, + does differ from braces in the
sense that + is an indefinite-ray infix function symbol, whereas
braces surround. I have forgotten the name for surrounding function
symbols.)

To see the big advantages of this for the formalization of
mathematics, consider ordered pairing. We certainly want <x,1/0> to be
undefined for all x. We also want (or want some variant of)

<x,1/0> ~ {{x},{x,1/0}}.

And since the left side is undefined, we definitely need to have
{x,1/0} undefined (for any x).

Harvey Friedman

On Tue, Oct 27, 2015 at 8:22 AM, Tennant, Neil <tennant.9 at osu.edu> wrote:
> The definitional abbreviationist treats {t1,...,tn} as a mere abbreviation
> for the set-abstraction term {x|x=t1v...vx=tn}. The curly-parentheses
> operationalist thinks that, for each value of n, there is a distinct n-ary
> operation sign { ,..., } that, when supplied with the n argument terms
> t1,...,tn, forms the functional term {t1,...,tn}.
>
> In my last post I pointed out that the definitional abbreviationst can say
>
> {1/0,2} = {x|x=1/0 v x=2} = {2}
>
> whereas the curly-parentheses operationalist says any identity statement
> involving {0/1,2} is false, while the identity statement {x|x=1/0 v x=2} =
> {2} is true.
>
> The follow-up point of this post is to observe that the definitional
> abbreviationist can also assert the identity claim
>
> {1/0} is the empty set, i.e. {1/0} = {x|~x=x}.
>
> Another nice thing is that this last identity is a theorem of core set
> theory in free logic.
>
> By way of corollary, there is an embarrassment for the reductive
> set-theorist who wishes to identify 0 as the empty set, and identity 1 as
> the singleton of the empty set. S/he would get
>
>      {{emptyset}/emptyset} = emptyset
>
> and would then have some explaining to do.
>
> There is also an embarrassment for the Fregean who tries to handle
> non-denoting (i.e., undefined) singular terms by making them (arbitrarily)
> denote the empty set. For then the empty set would be its own singleton (if
> s/he is also a definitional abbreviationist). Also, talking of the world
> more widely, s/he would assert that Santa Claus is 1/0.
>
> Neil Tennant