[Prev][Next][Index][Thread]

BAD MSG: somewhere between ZFC and ZFC+SI. The lower bound is proved in cite{grue92} by means of a syntactical translation of ZFC (including classical propositional and predicate calculus) into map theory, and the upper bound by building an (exceedingly complex) model of map theory within ZFC+SI. The present paper confirms the upper bound by providing much simpler models, the ``canonical models'' of the paper, which are in fact the paradigm of a large class of quite natural models of MT. That all these models interpret a model of ZFC is a consequence of the syntactic translation, which is a difficult theorem of \cite{grue92}. We can however give here a direct proof of a stronger result, namely that they interpret some $(V_{\sigma},{\in})$, where $\sigma$ is an inaccessible cardinal. Finally we return to the ``canonical'' models and show that they are adequate for the notion of computation which underlies MT.

- Prev:
**No Subject** - Next:
**Workshop on Types for Program Analysis** - Index(es):