An analytic representation of the semantics of first-order S5

DOI10.1007/978-3-032-04167-8_4MaRDI QIDQ6852322zbMATH OpenFDO

Authors Matthias Baaz, Mariami Gamsakhurdia, Anela Lolic

Publication date 26 February 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-032-04167-8_4

zbMATH Keywords

cut eliminationHerbrand's theoreminterpolationmodal S5prenex fragmenttwo-sorted logic

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Logic in artificial intelligence (68T27) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• Algebraic proof theory for substructural logics: cut-elimination and completions
• Craig's theorem in superintuitionistic logics and amalgamable varieties of pseudo-Boolean algebras
• Failures of the interpolation lemma in quantified modal logic
• First-order modal logic
• Grundlagen der Mathematik. I.
• Handbook of modal logic
• scientific article; zbMATH DE number 755666 (Why is no real title available?)
• Interpolation properties of superintuitionistic logics
• Intuitionistic logic and implicit definability
• Proof theory. 2nd ed
• Semantical investigations in Heyting's intuitionistic logic
• The complexity of explicit definitions
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory

This page was built for publication: An analytic representation of the semantics of first-order S5

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6852322)