Next: Axiom of integers Up: Recursive structures for Previous: A recursive functional

# Functional hierarchy axioms

We will give the axioms defining the objects that exist in our system. We will follow each axiom with the C ++ code to implement the axiom or construct the objects that it defines from other objects. These axioms will use recursive definitions that are not in general valid in ZF. At each stage at which we can, we will give a definition in ZF of the objects intended at that stage. The ZF definition will exhaustively define the objects that meet a given recursive definition. In particular the ZF definition will disallow any infinite descending functional evaluations. In the recursive definitions these are not explicitly prohibited (to do requires quantification over the reals) but only objects that satisfy this can be built up form the definitions. This is similar to ZF where well founded sets are not explicitly excluded (the axiom of regularity is generally not considered a part of ZF) but only well founded sets can be constructed.

In this formulation objects from C ++ class Functional take the place of sets in ZF. Everything, well almost everything, is an instance of this class. Of course we have the structure of C ++ as a preexisting framework for the structures we define. It is also convenient to treat integers as a special case. A Functional that represents an integer has a member function that returns the C ++ notion of an integer as a very_long  object. This can be defined as a standard C ++ integer object or as a class object that implements arbitrarily long integers.

The axioms loosely follow the axioms for ZF defined in Appendix on page . The power set axiom is replaced by the well foundedness axiom. The replacement axiom is replaced by the combination of the well foundedness axiom and the induction axiom.

Next: Axiom of integers Up: Recursive structures for Previous: A recursive functional
Mountain Math Software
Email comments to: webmaster@mtnmath.com