[FOM] Harrison Advocates ZFC (tweaked)

[Patrik Eklund]

On 2018-05-31 23:04, Harvey Friedman wrote:
> ...
> 
> I need to wrap my head around the issues Larry is talking about
> concerning n*x. If * is real multiplication, then n*x is automatically
> covered if every integer is a real number. But maybe one is going to
> have integers never real numbers. Then there is the canonical
> embedding j:Z into R, and one instead will write j(n)*x. Perhaps Larry
> is trying to avoid getting into a situation where you write j(n)*x.
> However, I don't see why we can't thrive in a situation where we
> simply make a choice:
> 
> 1. Every integer is a real. Then n*x is not problematic.
> 2. Integers are not reals. Then we write j(n)*x. One does see working
> mathematicians do stuff like this when they want to be a bit careful
> and are not doing 1.
> 
> Of course, there are overloading problems galore. Are we going to
> reuse j problematically? Sure, this is a problem, because we would
> rather not clutter up stuff with putting modifiers on j. Things get
> ugly quickly.
> 
> ...

I've often remarked that set theory is untyped, and this is one example. 
That j essentially "shifts types" (from nat to real), but since types 
and type constructors are not part of set theory, things indeed "get 
ugly quickly". As most of us know, set theory is ugly as it is.

Type constructing that j is not key. Type construction for managing 
power sets is. "Before Russell", set theorists new that and found it 
dubious to use X U PX. It is dubious to use it, and things get ugly when 
we do. Kreisel's 'Two notes ...' and many others have pointed that out.

Natural numbers is not a set. It's potentially a complicated 
construction of constructed types. Developing such things would 
significantly lower the importance of Gödel, Kleene and Princeton, and 
very few are prepared to try anything out that potentially leads to that 
lowering.

Set theory is imprisoned by its own stupidity.

We don't have that type theory. Type theories around are inadequate e.g. 
because they don't handle the "power type", and some in early stages 
have been brave to use "the type of all types". Abandoning set theory 
and reinventing problems is not what we should do.

However, we must now, and we will know.

Best,

Patrik