Model-theoretic characterization of intuitionistic predicate formulas

DOI10.1093/LOGCOM/EXT014MaRDI QIDQ2937693zbMATH OpenOpenAlexFDO

Authors Grigory Olkhovikov

Publication date 12 January 2015

Published in Journal Of Logic And Computation (Search for Journal in Brave)

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

zbMATH Keywords

first-order logicintuitionistic logicmodel theoryconstant domainsmodal characterization theorem

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20)

Abstract: Notions of asimulation and k-asimulation introduced in [Olkhovikov, 2011] are extended onto the level of predicate logic. We then prove that a first-order formula is equivalent to a standard translation of an intuitionistic predicate formula iff it is invariant with respect to k-asimulations for some k, and then that a first-order formula is equivalent to a standard translation of an intuitionistic predicate formula iff it is invariant with respect to asimulations. Finally, it is proved that a first-order formula is equivalent to a standard translation of an intuitionistic predicate formula over a class of intuitionistic models (intuitionistic models with constant domain) iff it is invariant with respect to asimulations between intuitionistic models (intuitionistic models with constant domain).

Recommendations

• Model-theoretic characterization of intuitionistic propositional formulas
• A bisimulation characterization for interpretability logic
• On expressive power of basic modal intuitionistic logic as a fragment of classical FOL
• Syntactic preservation theorems for intuitionistic predicate logic
• A note on bisimulations of finite Kripke models

Cited in

(10)

• Models of intuitionistic TT and NF
• Proof-irrelevant model of CC with predicative induction and judgmental equality
• A model of intuitionistic affine logic from stable domain theory
• A Lindström theorem for intuitionistic first-order logic
• A Lindström theorem for intuitionistic propositional logic
• Model-theoretic characterization of intuitionistic propositional formulas
• On expressive power of basic modal intuitionistic logic as a fragment of classical FOL
• On generalized van Benthem-type characterizations
• A van Benthem theorem for atomic and molecular logics
• scientific article; zbMATH DE number 176198 (Why is no real title available?)

This page was built for publication: Model-theoretic characterization of intuitionistic predicate formulas

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