Lambda Logic

Abstract

The main aim of this paper is to formulate "natural" logical foundations for type-free lambda-calculus. The importance of such foundations for analyzing arbitrary order computational properties of programs is emphasized. Lamda logic is a deductive system based on combinatory lambda-terms. Its language is conceived by extending the set of lambda-terms through the addition of new terms which are logical connectives. The model for lamda-logic is Dana Scott's D infinity, which can be represented as a pseudo-Boolean algebra. We present detailed proof that D infinity can be constructed as a Heyting algebra, thus being a model for some Heyting intuitionistic logical system. Our result, briefly described above, poses new problems. In particular, the relation between algebraic models of computer languages and the algebraic model theory is of great interest if one wants to establish a logical framework for the verification of programs written in these languages.