[FOM] 642: Rigorous Formalization of Mathematics 3

[Arnon Avron]

On Sun, Nov 01, 2015 at 01:11:22AM -0500, Harvey Friedman wrote:
 
> 12. Function Abstraction. Here the situation is totally different. We
> do need special notation for function abstraction. This is something
> that mathematicians have been successfully resisting since at least
> the invention of the calculus, and Arnon has discussed on the FOM a
> number of times. If we are really going to support Fully Rigorous
> Formalization then we are going to have to confront this issue of
> Function Abstraction properly.

Actually, no further means are needed for that beyond the
possibility to use abbreviations. As is noted in my paper
"A Framework for Formalizing Set Theories Based on the
Use of Static Set Terms" (which I have mentioned already on FOM),
the use of { |  } suffices for everything. Thus 
$\lambda x\in A.t$ can be introduced as an abbreviation 
for {<x,t> | x\in A} (which itself is of course
an abbreviation of {y|\exists x. x\in A and y=t}, where
y is fresh). In turn, the application of a function to an argument
can be defined as f(t)= \iota y.<t,y>\in f, where \iota
is the operator for definite article, which Dana Scott 
suggested in a recent posting to introduce (in the form of
"!{x: Phi(x)}").  But \iota too is available here, and needs
no special introduction: since we assume that everything is
a set, \iota x.\Phi(x) can be taken as an abbreviation
for {y|\exists x.\Phi(x) and y\in x}, that is: the union
of {x: Phi(x)}. (Note that if
there exists a unique x such that \Phi(x) then this
expression denotes that single x. This is due to the fact
that the union of {x} is always x if we assume that every x is a set).

Arnon Avron