First-Order Logic Without Bound Variables: Compositional Semantics

Abstract

A strict version of compositional semantics would have all composite meaningful expressions be of the form XY, where X and Y are meaningful and the concatenation expresses application of a function (X ) to an argument (Y ). In proof theory, compositionality is violated because of bound variables both in formulas (quantification) and in deductions (introduction rules). Two applications of typed combinator theory are used to introduce a proof theory for first-order predicate logic without identity in which there are no bound variables.