A Simple and Complete Model Theory for Intensional and Extensional Untyped Lambda-Equality

Abstract

We present a sound and complete model theory for theories of -reduction with or without -expansion. The models of this paper derive from structures of modal logic: we use ternary accessibility relations on ‘possible worlds’ to model the action of intensional and extensional lambda-abstraction in much the same way binary accessibility relations are used to model the box operators of a normal multi-modal logic.