[FOM] FOM: Rigorous Formalization of Mathematics 3

[Dana Scott]

Harvey Friedman is suggesting:

> v. variables are always defined.
> vi. Constants always defined? I'm not sure, and see the merit in yes
> and no. Tentatively, constants always defined. Of course, this commits
> one to proving definedness when introducing new constants by
> definition.

I would rather suggest:

v. bound variables (in quantifiers and set abstraction)
are assumed to be always defined.

Therefore, "(some x) x ~ c" means that the constant 
is defined.

vi. Constants and free variables are not always defined.

Therefore substitution for free variables does not assume
definedness.  Also, in ZF the constant V for the universal
class is not defined (namely, "{x: x=x }").  And if you like, 
"c in V" also means that the constant is defined.

Another problem is descriptions.  How about "!{x: Phi(x)}"
as the notation for the unique element of the indicated class.
This, then, is a theorem:  "(all x) !{x} = x".

Just sayin'.