Map theory
type: Item
instance of: scholarly article
title: Map theory
zbMATH Open document ID: 0805.03044
DOI: 10.1016/0304-3975(92)90296-R
author: Klaus Grue
published in: Theoretical Computer Science
publication date: 1992-09-27T00:00:00Z
review text: The language of Map is that of \(\lambda\)-calculus augmented with five individual constants: \(\top\), \(\bot\), if, \(\phi\), \(\epsilon\) . The first two represent truth and undefinedness and the third is MacCarthy's conditional, but the strength of the theory relies on the last two: \(\phi\) is a map which codes a well-foundedness predicate \(\Phi\) and \(\epsilon\) is a choice function ``à la Hilbert'' which is linked to well-foundedness. The ideas behind \(\phi\) and \(\epsilon\) are very elegant, but the axioms are only able to express consequences of them. Formulas of ZFC are coded by terms of Map and theorems of ZFC by equations of the form \(A=\top\) which are provable in Map, so consistency of Map implies consistency of ZFC. Conversely in every model \(U\) of ZFC + SI , where SI asserts the existence of a strongly inaccessible cardinal, a model of Map theory will be definable. The paper is divided into three parts. The first one is a clear exposition of the ideas and intuitions behind Map theory, of its expressive power, and it contains a survey of the other two parts. The second part deals with the precise axiomatisation of Map and develops ZFC and its logical environment within Map theory. The third one deals with the construction of a model of Map inside a model of ZFC+SI. This construction is highly technical and uses relativisation, Gödel numberings, fixed point theorems for natural but rather complicated functionals, intricate definitions, and finally a quotient construction. New consistency proofs have been recently given by the author and the reviewer, in the spirit of denotational semantics (paper in preparation). They rely on expansions of ``\(\xi\)-denotational semantics'', where \(\xi\) is a regular cardinal (the usual Scott semantics corresponds to \(\xi = \omega\)). The models which are given satisfy all the intuitive properties of \(\Phi\) and \(\epsilon\) which have guided the author and should lead to more attractive versions of Map Theor…
Mathematics Subject Classification ID: 03E70
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03E35
Mathematics Subject Classification ID: 03E30
Mathematics Subject Classification ID: 68Q55
zbMATH DE Number: 64938
zbMATH Keywords: lambda calculus
zbMATH Keywords: MacCarthy's conditional
zbMATH Keywords: well-foundedness predicate
zbMATH Keywords: consistency
zbMATH Keywords: strongly inaccessible cardinal
zbMATH Keywords: model of Map theory
zbMATH Keywords: axiomatisation
zbMATH Keywords: ZFC
zbMATH Keywords: semantics
zbMATH Keywords: choice function
reviewed by: Chantal Berline
MaRDI profile type: Publication
cites work: Q3992552
cites work: The lambda calculus, its syntax and semantics
cites work: Q3997112
cites work: Towards a computation system based on set theory
cites work: The Vienna development method: The meta-language
cites work: Q5573370
cites work: Q4108328
cites work: Q5585364
cites work: Q3862437
cites work: Q5812175
cites work: Set theory. An introduction to independence proofs
cites work: Q5586435
cites work: Q5553251
cites work: Q4099613
cites work: Q5601829
cites work: Q5586197
cites work: Q4109652
cites work: A new implementation technique for applicative languages
full work available at URL: 0304-3975(92)90296-r
OpenAlex ID: W2912844405
description: scientific article; zbMATH DE number 64938