A note on the proof theory of the \(\lambda \Pi\)-calculus (Q1891931)

The \(\lambda \Pi\)-calculus is a theory of first-order dependent function types, and so is a member of and/or related to the Edinburgh Logical Framework. Logics for computer science have been developed with an eye to checking formal proofs, etc. In this paper, the author turns the table around and proves the cut-elimination theorem (which was formulated and proved for a formal calculus by Gentzen six decades ago) in this \(\lambda \Pi\)-calculus. He formulates \(\lambda \Pi\) in two formats; one as natural deduction, N, and the other as the sequent calculus, \(G\). Then he shows the equivalence of G, N, and G-cut, establishing the eliminability of the rule, cut. Here, this rule is formulated as: from \(\Gamma \vdash_\Sigma M\):\(A\) and \(\Gamma, x\):\(A, \Delta \vdash_\Sigma X\), \(\text{infer} \Gamma, \Delta [M/x] \vdash_\Sigma X[M/x]\). In the second half of the paper, the author formulates and mentions a number of meta-calculi for proof search in \(\lambda \Pi\), utilizing ideas of unification and of resolution. Here is an example: first, he presents the calculus, NR, with a resolution rule, and shows its equivalence with N. Then he formulates a meta-calculus LNR, and shows: \(\Phi\) is an LNR proof of \(\Gamma \Rightarrow_\Sigma A\) if and only if NR proves \(\Gamma \vdash_\Sigma M\):\(A\) where \(M\) is the extract-object of \(\Phi\).