This paper presents a proof of strong normalization of natural deduction for minimal propositional logic, inspired by the syntax-directed inductive techniques of [20] . While this avenue bypasses semantic models, like computability predicates, and provides a short proof by embedding the reduction relation into syntactic rules, it operates within the framework of the lambda calculus, with almost no reference to the methods of Structural Proof Theory. Instead, we conciliate both methodologies by reinterpreting their arguments to provide an explanatory and syntax-directed proof in the context of natural deduction, emphasizing the diagrammatic manipulation of derivations, the combinatorial behavior of proof-trees and the usefulness of an enhanced syntax of lambda calculus to codify diagrams, thus putting the Curry-Howard correspondence at work. Our approach not only bridges the gap between the algebraic reasoning of the lambda calculus and the diagrammatic intuition of natural deduction but also aligns with the increasingly tangible ideal of producing computer-assisted formalizations of non-trivial mathematical results.

Abstract The proof theory of the constructive modal logic S4 (hereafter $\mathsf{CS4}$ ) has been settled since the beginning of this century by means of either standard natural deduction and sequent calculi or by the reconstruction of modal logic through hypothetical and categorical judgments à la Martin-Löf, an approach carried out by using a special kind of sequents, which keeps two separated contexts representing ordinary and enhanced hypotheses, intuitively interpreted as true and valid assumptions. These so-called dual-context sequents, originated in linear logic, are used to define a natural deduction system handling judgments of validity, truth, and possibility, resulting in a formalism equivalent to an axiomatic system for $\mathsf{CS4}$ . However, this proof-theoretical study of $\mathsf{CS4}$ lacks, to the best of our knowledge, its third fundamental constituent, namely a sequent calculus. In this paper, we define such a dual-context formalism, called ${\bf DG_{CS4}}$ , and provide detailed proofs of the admissibility for the ordinary cut rule as well as the elimination of a second cut rule, which manipulates enhanced hypotheses. Furthermore, we make available a formal verification of the equivalence of this proposal with the previously defined axiomatic and dual-context natural deduction systems for $\mathsf{CS4}$ , using the Coq proof-assistant.