A synthetic axiomatization of Map Theory

TY - JOUR

T1 - A synthetic axiomatization of Map Theory

AU - Berline, Chantal

AU - Grue, Klaus Ebbe

PY - 2016

Y1 - 2016

N2 - This paper presents a substantially simplified axiomatization of Map Theory and proves the consistency of this axiomatization (called MT) in ZFC under the assumption that there exists an inaccessible ordinal. Map Theory axiomatizes lambda calculus plus Hilbert's epsilon operator. All theorems of ZFC set theory including the axiom of foundation are provable in Map Theory, and if one omits Hilbert's epsilon operator from Map Theory then one is left with a computer programming language. Map Theory fulfills Church's original aim of lambda calculus. Map Theory is suited for reasoning about classical mathematics as well as computer programs. Furthermore, Map Theory is suited for eliminating the barrier between classical mathematics and computer science rather than just supporting the two fields side by side. Map Theory axiomatizes a universe of “maps”, some of which are “wellfounded”. The class of wellfounded maps in Map Theory corresponds to the universe of sets in ZFC. The first axiomatization MT 0 of Map Theory had axioms which populated the class of wellfounded maps, much like the power set axiom along with others populate the universe of ZFC. The new axiomatization MT of Map Theory is “synthetic” in the sense that the class of wellfounded maps is defined inside Map Theory rather than being introduced through axioms. In the paper we define the notions of canonical and non-canonical κ- and κσ-expansions and prove that if σ is the smallest strongly inaccessible ordinal then canonical κσ-expansions are models of MT (which proves the consistency). Furthermore, in Appendix A, we prove that canonical ω-expansions are fully abstract models of the computational part of Map Theory.

AB - This paper presents a substantially simplified axiomatization of Map Theory and proves the consistency of this axiomatization (called MT) in ZFC under the assumption that there exists an inaccessible ordinal. Map Theory axiomatizes lambda calculus plus Hilbert's epsilon operator. All theorems of ZFC set theory including the axiom of foundation are provable in Map Theory, and if one omits Hilbert's epsilon operator from Map Theory then one is left with a computer programming language. Map Theory fulfills Church's original aim of lambda calculus. Map Theory is suited for reasoning about classical mathematics as well as computer programs. Furthermore, Map Theory is suited for eliminating the barrier between classical mathematics and computer science rather than just supporting the two fields side by side. Map Theory axiomatizes a universe of “maps”, some of which are “wellfounded”. The class of wellfounded maps in Map Theory corresponds to the universe of sets in ZFC. The first axiomatization MT 0 of Map Theory had axioms which populated the class of wellfounded maps, much like the power set axiom along with others populate the universe of ZFC. The new axiomatization MT of Map Theory is “synthetic” in the sense that the class of wellfounded maps is defined inside Map Theory rather than being introduced through axioms. In the paper we define the notions of canonical and non-canonical κ- and κσ-expansions and prove that if σ is the smallest strongly inaccessible ordinal then canonical κσ-expansions are models of MT (which proves the consistency). Furthermore, in Appendix A, we prove that canonical ω-expansions are fully abstract models of the computational part of Map Theory.

KW - Lambda calculus

KW - Foundation of mathematics

KW - Map theory

KW - Kappa-Scott semantics

KW - Hilbert's epsilon operator

U2 - 10.1016/j.tcs.2015.11.028

DO - 10.1016/j.tcs.2015.11.028

M3 - Journal article

SN - 0304-3975

VL - 614

SP - 1

EP - 62

JO - Theoretical Computer Science

JF - Theoretical Computer Science

ER -