Nested proof search as reduction in the Lambda-calculus
Nicolas Guenot · 2011
We present a system for propositional implicative intuitionistic logic in the calculus of structures, which is a generalisation of the sequent calculus to the deep inference methodology. We show that it is sound and complete with respect to the usual sequent calculus, and consider a restricted system for a smaller class of formulas. Then, we encode lambda-terms with explicit substitutions in these formulas and exhibit a correspondence between proof search in this system and reduction in a lambda-calculus with explicit substitutions. Finally, we present a further restriction to allow a correspondence with the standard lambda-calculus, and show that we can prove results on lambda-calculi by proving results on derivations in the proof systems.