Internalization: The case of hybrid logics

DOI10.1093/LOGCOM/11.5.671MaRDI QIDQ2772880zbMATH OpenOpenAlexFDO

Authors Jeremy Seligman

Publication date 29 August 2002

Published in Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL https://semanticscholar.org/paper/856c1727dc07be0c5c104c393759e3b24a4be03b

zbMATH Keywords

hybrid logicinternalizationsequent calculus

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05)

Review text

The author presents a method of internalization for hybrid logic. It works in three steps. First the semantic theory of hybrid logic is formalized in a sequent calculus of predicate logic with additional axioms. In a second step a refined calculus with the subformula property is introduced which, however, is not fully internalized. This is solved in a third step by another calculus which uses a hybrid operator. In the final paragraph the author claims that the given strategy can be applied to a wide range of logical operations but that the exact limits of the method are still open.

Recommendations

• Hybrid logic and its proof-theory
• Justification logics and hybrid logics
• Internalizing labelled deduction
• Termination for Hybrid Tableaus
• Modal Hybrid Logic

Cited in

(16)

• A proof-theoretic study of the correspondence of hybrid logic and classical logic
• Recapturing dynamic logic of relation changers via bounded morphisms
• Formalizing a Seligman-style tableau system for hybrid logic (short paper)
• ExpTime tableaux with global caching for hybrid PDL
• Simple cut elimination proof for hybrid logic
• An Analytic Logic of Aggregation
• A Two-Dimensional Hybrid Logic of Subset Spaces
• Coalgebraic Hybrid Logic
• Why does the proof-theory of hybrid logic work so well?
• Internalizing labelled deduction
• Analytic Non-Labelled Proof-Systems for Hybrid Logic: Overview and a couple of striking facts
• The logicality of equality
• On temporal references via definite descriptions in first-order monadic logic of order
• Synthetic completeness for a terminating Seligman-style tableau system
• Sequent calculi and decidability for intuitionistic hybrid logic
• Operators vs. arguments: The ins and outs of reification

This page was built for publication: Internalization: The case of hybrid logics

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