A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.

DOI10.1016/S0304-3975(02)00024-5zbMath1048.03042MaRDI QIDQ1603701

Mitsuhiro Okada

Publication date: 15 July 2002

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

linear logicsubstructural logicintuitionistic logiccut-eliminationgeneralization of phase semantics of linear logichigher-order phase semantics

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Related Items (23)

Logic and majority voting ⋮ Syntactic Completeness of Proper Display Calculi ⋮ Phase semantics and decidability of elementary affine logic ⋮ Phase semantics for light linear logic ⋮ Algebraic proof theory for substructural logics: cut-elimination and completions ⋮ Cut elimination and strong separation for substructural logics: an algebraic approach ⋮ Kripke models for classical logic ⋮ A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms ⋮ Orthogonality and Boolean Algebras for Deduction Modulo ⋮ A simple proof that super-consistency implies cut elimination ⋮ Completeness of second-order intuitionistic propositional logic with respect to phase semantics for proof-terms ⋮ Dynamic non-commutative logic ⋮ Forcing in Proof Theory ⋮ Constructive decision via redundancy-free proof-search ⋮ Phase semantics and Petri net interpretation for resource-sensitive strong negation ⋮ The bounded proof property via step algebras and step frames ⋮ MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics ⋮ Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus ⋮ Hyper-MacNeille completions of Heyting algebras ⋮ On the unification of classical, intuitionistic and affine logics ⋮ Gentzen-type calculi for involutive quantales ⋮ On the Convergence of Reduction-based and Model-based Methods in Proof Theory ⋮ Towards a semantic characterization of cut-elimination

Cites Work

• The structure of multiplicatives
• Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic
• The undecidability of second order multiplicative linear logic
• Logics without the contraction rule
• Non‐commutative intuitionistic linear logic
• Ein Ausgezeichnetes Modell Für Die Intuitionistische Typenlogik
• The finite model property for various fragments of intuitionistic linear logic
• The finite model property for various fragments of linear logic
• Pretopologies and completeness proofs
• Categorical reconstruction of a reduction free normalization proof
• Hauptsatz for higher order logic
• Intensional interpretations of functionals of finite type I
• A nonconstructive proof of Gentzen’s Hauptsatz for second order predicate logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.