On Proof Terms and Embeddings of Classical Substructural Logics

摘要: There is an intimate connection between proofs of the natural deduction systems and typed lambda calculus. It well-known that in simply calculus, notion formulae-as-types makes it possible to find fine structure implicational fragment intuitionistic logic, i.e., relevant BCK-logic linear logic. In this paper, we investigate three classical substructural logics (GL, GLc, GLw) Gentzen's sequent calculus consisting implication negation, which contain some right structural rules. terms Parigot's λμ-calculus with proper restrictions, introduce a proof term assignment these logics. According notions, can classify λμ-terms into four categories. proved well-typed GLx-λμ-terms correspond GLx proofs, GLx-λμ-term has principal type if stratified where x nil, c, w or cw. Moreover, embeddings corresponding Godel-style translations are preserving As by-products, obtained inhabitation problem decidable strongly normalizable.