An axiomatic theory for partial functions (Q1317437)

The author develops an axiomatic theory of one-place, unary functions. The theory has one basic ternary relation \({\mathbf A}\), called the relation of application, where \({\mathbf A} (x,y,z)\) has the meaning ``the function \(x\) applied to the argument \(y\) yields the result \(z\)''. To make formulas more readable the author introduces pseudoterms. He discusses the Russell Paradox and shows how it can be solved. In the main chapter, he introduces and describes the eight axioms of the theory. He gives some consequences of them. So, natural numbers are defined as specific one- place functions. He proves that functions may be defined inductively and that the operation of currying on \(n\)-ary functions is well-defined. The theory contains a model of (extensional) lambda calculus. The author shows relative consistency of the theory by interpreting it in ZF set theory without the axiom of foundation but including Boffa's axiom of universality. He also shows that this variant of set theory can be interpreted within the theory of functions thus showing that ZF set theory and the theory presented here are equi-consistent and equally powerful.