FOM: FOM based on functions
Henk Barendregt
henk at uow.edu.au
Tue Jan 13 16:45:41 EST 1998
Steve Simpson wrote:
> There is room for more discussion about which mathematical concepts
> are the most basic. I would think that the most controversial item on
> my list would be "function". Has there ever been a decent
> foundational scheme based on functions rather than sets? I know that
> some category theorists want to claim that topos theory does this, but
> that seems pretty indefensible. For one thing, there doesn't seem to
> be any way to do real analysis in a topos.
I think one can defend that a system like lambda-PRED-omega is a
good candidate for a FOM based on functions.
See my paper in vol. II Handbook of Logic in Computer Science, OUP for a
definition of that system. (Paper also available from
http://www.cs.kun.nl/~henk/papers.html)
What is your argument, Steve, that one cannot do analysis in a topos?
Technical question. In order to show that this type-theory is well behaved
one usually shows that the more simple system lambda-C (Calculus of
Constructions) is strongly normalising. This is done in ZF. Is the statement
lambda-C is SN
provable in Z, i.e. ZF without the scheme of replacement?
I guess not.
Henk
-----------------------------------------------------
Name: Henk Barendregt
Position: professor of fo(m&cs)
Place: Nijmegen University, The Netherlands
More information about the FOM
mailing list