FOM: FOM based on functions

[Henk Barendregt]

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