Map theory (Q1193653)

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 Theory.