A Simple Class of Kripke-Style Models in Which Logic and Computation Have Equal Standing

We present a sound and complete model of lambda-calculus reductions based on structures inspired by modal logic (closely related to Kripke structures). Accordingly we can construct a logic which is sound and complete for the same models, and we identify lambda-terms with certain simple sentences (predicates) in this logic, by direct compositional translation. Reduction then becomes identified with logical entailment. Thus, the models suggest a new way to identify logic and computation. Both have elementary and concrete representations in our models; where these representations overlap, they coincide. In a concluding speculation, we note a certain subclass of the models which seems to play a role analogous to that played by the cumulative hierarchy models in axiomatic set theory and the natural numbers in formal arithmetic -- there are many models of the respective theories, but only some, characterised by a fully second order interpretation, are the `intended' ones.

• Type: Journal
• Year: 2010
• Where: LPAR
• Authors: Michael Gabbay, Murdoch James Gabbay
• Keywords: Automated Reasoning, Certain Simple Sentences, Cumulative Hierarchy Models, Logic, LPAR 2010