×

Constructing possible worlds. (English) Zbl 0838.03046

This paper provides an intuitionistic account of possible worlds. The four forms of judgement of Martin-Löf’s type theory \[ \begin{alignedat}{2} &A:\text{set } &&\text{ which means\quad \(A\) is a set}\\ &A=B:\text{set}\quad &&\text{ which means\quad \(A\) and \(B\) are equal sets}\\ &a:A &&\text{ which means\quad \(a\) is an element of the set \(A\)}\\ &a= b:A &&\text{ which means\quad \(a\) and \(b\) are equal elements of the set \(A\)} \end{alignedat} \] are relativized to worlds by adding “in \(W\)” to each of them. What is an object in a world \(W\), either “set in \(W\)” or “element of a set in \(W\)”, is explained correlatively. Worlds are built gradually from contexts, and the four forms of judgement will be first relativized to contexts. The construction of worlds as limits of sequences of contexts follows Martin-Löf’s nonstandard extension of type theory [P. Martin-Löf, Lect. Notes Comput. Sci. 417, 146-197 (1990; Zbl 0721.03043)].
Our approach will be related to both situation semantics and possible worlds semantics.

MSC:

03F50 Metamathematics of constructive systems

Citations:

Zbl 0721.03043
PDFBibTeX XMLCite
Full Text: DOI