MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics

DOI10.4230/LIPIcs.CSL.2018.37OpenAlexW2963572521MaRDI QIDQ5079762

Kazushige Terui

Publication date: 28 May 2022

Full work available at URL: https://arxiv.org/abs/1804.11066

zbMATH Keywords

\(\Omega\)-rulemacneille completionalgebraic cut eliminationparameter-free second-order logic

Mathematics Subject Classification ID

Logic in computer science (03B70)

Related Items

Hyper-MacNeille completions of Heyting algebras

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An extension of the omega-rule
• Algebraic proof theory for substructural logics: cut-elimination and completions
• Algebraic proof theory: hypersequents and hypercompletions
• Zur Kennzeichnung der Dedekind-MacNeilleschen Hülle einer geordneten Menge
• On the fundamental conjecture of \(GLC\). V
• Parameter-free polymorphic types
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Lattice-valued representation of the cut-elimination theorem
• Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic
• A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
• A Buchholz rule for modal fixed point logics
• MacNeille completions of lattice expansions
• Bounded distributive lattice expansions
• Residuated frames with applications to decidability
• Induction and inductive definitions in fragments of second order arithmetic
• A nonconstructive proof of Gentzen’s Hauptsatz for second order predicate logic
• Boolean Algebras with Operators. Part I
• On the completion by cuts of distributive lattices
• Bounded lattice expansions
• Explaining the Gentzen-Takeuti reduction steps: A second-order system