FOM: Simpson's question: addendum

[Henk Barendregt]

PS 

I forgot to react to Steve's question. Henk

----------------------------------------------------------------------

Steve Simpson asked:

> I would like to ask Henk, can this alleged defect of ZFC be overcome
> by adding machinery for extension by definitions and, say, primitive
> recursive functions on omega?  Such machinery is fairly standard, I
> think.

First of all it should be primitive recursion over more general data
types. If we do it only over omega, then computations over say lists
or trees are awkward. Such computations are essential.

But this is not enough. We should allow that the side conditions in
the derivation rules (like t is free for x in A) are more general; we
want arbitrary predicates computable in the programming language
accompanying the system. This is what I call "the Poincare' Principle",
available in type theories (conversion rule).

==========================================================================