A synthetic axiomatization of Map Theory
| Autor: | Klaus Grue, Chantal Berline |
|---|---|
| Přispěvatelé: | PPS, Preuves, Programmes et Systèmes (PPS), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Department of Computer Science [Copenhagen] (DIKU), Faculty of Science [Copenhagen], University of Copenhagen = Københavns Universitet (KU)-University of Copenhagen = Københavns Universitet (KU), For Chantal Berline: CNRS, PPS, UMR 7126, Univ Paris Diderot, Sorbonne Paris Cité, F-75205 Paris, FranceFor Klaus Grue: DIKU, Universitetsparken 1, DK-2100 Copenhagen East, Denmark |
| Rok vydání: | 2016 |
| Předmět: |
Pure mathematics
Class (set theory) General Computer Science 03B40 03B70 03E99 68N18 0102 computer and information sciences 01 natural sciences ACM: G.: Mathematics of Computing Theoretical Computer Science symbols.namesake Kappa-Scott semantics Computer Science::Logic in Computer Science Inaccessible cardinal Lambda-calculus Set theory Foundations of mathematics Axiom Mathematics Classical mathematics [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Prewellordering ACM: F.: Theory of Computation Algebra [MATH.MATH-LO]Mathematics [math]/Logic [math.LO] Mathematics::Logic Von Neumann–Bernays–Gödel set theory 010201 computation theory & mathematics Hilbert's epsilon operator symbols Map Theory |
| Zdroj: | Theoretical Computer Science Theoretical Computer Science, Elsevier, 2016, 614, pp.1-62. ⟨10.1016/j.tcs.2015.11.028⟩ |
| ISSN: | 0304-3975 1879-2294 |
| DOI: | 10.1016/j.tcs.2015.11.028 |
| Popis: | Includes TOC détaillée, index et appendices; International audience; This paper presents a subtantially simplified axiomatization of Map Theory and proves the consistency of this axiomatization 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 introducing lambda calculus. Map Theory is suited for reasoning about classical mathematics as well ascomputer programs. Furthermore, Map Theory is suited for eliminating thebarrier 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 version MT0 of Map Theory had axioms which populated the class of wellfounded maps, much like the power set axiom et.al. populates 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 MapTheory rather than being introduced through axioms. In the paper we define the notion of kappa- and kappasigma-expansions and prove that if sigma is the smallest strongly inaccessible cardinal then canonical kappasigma expansions are models of MT (which proves the consistency). Furthermore, in the appendix, we prove that canonical omega-expansions are fully abstract models of the computational part of Map Theory. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect