Algebraic proof theory: Hypersequents and hypercompletions

详细信息    查看全文

• 作者：Agata Ciabattoni^a ; ^{agata@logic.at} ; Nikolaos Galatos^b ; ^{ngalatos@du.edu} ; Kazushige Terui^c ; ^{terui@kurims.kyoto-u.ac.jp}
• 关键词：03B47 ; 03G10 ; 03F05 ; 03F03
• 刊名：Annals of Pure and Applied Logic
• 出版年：2017
• 出版时间：March 2017
• 年：2017
• 卷：168
• 期：3
• 页码：693-737
• 全文大小：827 K
• 卷排序：168

文摘

We continue our program of establishing connections between proof-theoretic and order-algebraic properties in the setting of substructural logics and residuated lattices. Extending our previous work that connects a strong form of cut-admissibility in sequent calculi with closure under MacNeille completions of corresponding varieties, we now consider hypersequent calculi and more general completions; these capture logics/varieties that were not covered by the previous approach and that are characterized by Hilbert axioms (algebraic equations) residing in the level P3P3 of the substructural hierarchy. We provide algebraic foundations for substructural hypersequent calculi and an algorithm to transform P3P3 axioms/equations into equivalent structural hypersequent rules. Using residuated hyperframes we link strong analyticity in the resulting calculi with a new algebraic completion, which we call hyper-MacNeille.