This paper introduces Hilbert systems for λ-calculus, called sequent combinators, addressing
many of the problems of Hilbert systems that have led to the more widespread adoption of
natural deduction systems in computer science. This suggests that Hilbert systems, with their
uniform approach to meta-variables and substitution, may be a more suitable framework
than λ-calculus for type theories and programming languages. Two calculi are introduced
here. The calculus SKIn captures λ-calculus reduction faithfully, is confluent even in the
presence of meta-variables, is normalizing but not strongly normalizing in the typed case,
and standardizes. The sub-calculus SKInT captures λ-reduction in slightly less obvious ways,
and is a language of proof-terms not directly for intuitionistic logic, but for a fragment of S4
that we name near-intuitionistic logic. To our knowledge, SKInT is the first confluent,
first-order calculus to capture λ-calculus reduction fully and faithfully and be strongly
normalizing in the typed case. In particular, no calculus of explicit substitutions has yet
achieved this goal.
A Concrete Framework for Environment Machines
