An axiomatic theory for partial functions

DOI10.1006/INCO.1993.1063MaRDI QIDQ1317437zbMATH OpenOpenAlexFDO

Authors Jan Kuper

Publication date 22 January 1995

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://research.utwente.nl/en/publications/an-axiomatic-theory-for-partial-functions(e9db9484-baf5-49b0-825d-608bf451344d).html

zbMATH Keywords

Boffa's axiom of universalitymodel of lambda calculusone- place functionsrelation of applicationrelative consistencyRussel paradoxtheory of functions

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Other classical set theory (including functions, relations, and set algebra) (03E20) Nonclassical and second-order set theories (03E70)

Review text

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.

Recommendations

• An axiomatization of partial n-place operations
• A partial functions version of Church's simple theory of types
• A set theory with support for partial functions
• Partial functions in type theory
• scientific article; zbMATH DE number 1341476

Cited in

(15)

• Map theory
• A set theory with support for partial functions
• Axiomatic theory of partial continuous functions and the Peano curve
• Difference-restriction algebras of partial functions: axiomatisations and representations
• Axiomatization and the antimean function on paths
• scientific article; zbMATH DE number 3873292 (Why is no real title available?)
• Towards a Theory of Extractable Functions
• Axiomatic recursion theory and the continuous functionals
• scientific article; zbMATH DE number 4037816 (Why is no real title available?)
• An axiomatization of partial n-place operations
• Lambda theory: introduction of a constant for ``nothing into set theory, a model of consistency and most noticeable conclusions
• Implicit dynamic function introduction and Ackermann-like function theory
• A partial functions version of Church's simple theory of types
• A first order theory of functional parthood
• The axiomatization of override and update

This page was built for publication: An axiomatic theory for partial functions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1317437)