Model-theoretic characterization of intuitionistic predicate formulas

DOI10.1093/LOGCOM/EXT014zbMATH Open1338.03008arXiv1202.1195OpenAlexW1600736686MaRDI QIDQ2937693FDOQ2937693

Authors: Grigory Olkhovikov 

Publication date: 12 January 2015

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

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).

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

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

zbMATH Keywords

first-order logicintuitionistic logicmodel theoryconstant domainsmodal characterization theorem

Mathematics Subject Classification ID

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

Cited In (10)

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

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)