Sequent Combinators: A Hilbert System for the Lambda Calculus

Healfdene Goguen


This paper introduces a Hilbert system for lambda calculus called sequent combinators. Sequent combinators address many of the problems of Hilbert systems, which have led to the more widespread adoption of natural deduction systems in computer science. This suggests that Hilbert systems, with their more uniform approach to meta-variables and substitution, may be a more suitable framework than lambda calculus for type theories and programming languages.


This report is available in the following formats:

Previous | Index | Next