Intuitionistic K is a Bisimulation-Invariant Fragment of Intuitionistic First-Order Logic

We define the notion of IK-bisimulation between the relational semantics for the intuitionistic modal logic IK, and prove that IK arises as the IK-bisimulation-invariant fragment of intuitionistic first-order logic.En route, we provide an intrinsic characterisation result of this logic by way of a Hennessy-Milner-style theorem and develop some intuitionistic first-order model theory, including intuitionistic analogues of Łoś's Theorem, elementary embeddings and countable saturation.

Authors

Publication Details

Journal
Electronic Proceedings in Theoretical Computer Science
Published
2026-06-28
DOI
https://doi.org/10.4204/eptcs.447.26
Primary Topic
Logic, Reasoning, and Knowledge
Type
article
Field-Weighted Citation Impact
0.00

Funders

Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
article

Intuitionistic K is a Bisimulation-Invariant Fragment of Intuitionistic First-Order Logic

João Marcos, Rodrigo Stefanes, Jim de Groot
Electronic Proceedings in Theoretical Computer Science
Logic, Reasoning, and Knowledge
article

Intuitionistic K is a Bisimulation-Invariant Fragment of Intuitionistic First-Order Logic

João Marcos, Rodrigo Stefanes, Jim de Groot
article en

Abstract

We define the notion of IK-bisimulation between the relational semantics for the intuitionistic modal logic IK, and prove that IK arises as the IK-bisimulation-invariant fragment of intuitionistic first-order logic.En route, we provide an intrinsic characterisation result of this logic by way of a Hennessy-Milner-style theorem and develop some intuitionistic first-order model theory, including intuitionistic analogues of Łoś's Theorem, elementary embeddings and countable saturation.

Electronic Proceedings in Theoretical Computer ScienceVol. 447
National Science Foundation, Schweizerischer Nationalfonds zur Förderung der Wissenschaftlichen Forschung, Conselho Nacional de Desenvolvimento Científico e Tecnológico, Universidade Federal de Santa Catarina, Dirección General de Asuntos del Personal Académico, Universidad Nacional Autónoma de México
Reduced inequalities
Openalex Percentile: Top 6%
Logic, Reasoning, and Knowledge
DOIOpen Access PDFOpenAlex
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.