arxiv: 2605.00523 · v1 · submitted 2026-05-01 · 🧮 math.LO · cs.LO

Recognition: unknown

Intuitionistic Common Knowledge

Lukas Zenger

Pith reviewed 2026-05-09 15:05 UTC · model grok-4.3

classification 🧮 math.LO cs.LO

keywords intuitionistic logiccommon knowledgeepistemic logicsequent calculusdecidabilityfinite model propertymodal logiccyclic proofs

0 comments

The pith

An intuitionistic common knowledge logic admits sound and complete axiomatizations plus analytic cyclic sequent calculi that decide validity in exponential time.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper introduces ICK, an extension of intuitionistic propositional logic that adds multiple agent knowledge operators and a common knowledge operator. It interprets the language over birelational Kripke models that obey a fixed interaction rule between the intuitionistic ordering and the accessibility relations, and it treats the reflexive, S4, and S5 restrictions of those models. Complete axiomatizations and analytic cyclic sequent calculi are supplied for every variant; each system is shown sound and complete, to enjoy the finite model property, and to support automated proof search. Validity and proof-search problems for all the logics are placed in exponential time, and a translation from classical common knowledge over S5 into the corresponding intuitionistic system is exhibited.

Core claim

ICK extends intuitionistic propositional logic by box modalities for individual agents and a common-knowledge operator, interpreted over birelational Kripke models obeying a simple interaction principle between the intuitionistic order and modal accessibility. Axiomatizations and analytic cyclic sequent calculi are given for ICK and its reflexive, S4, and S5 restrictions; each is proved sound and complete. The finite model property and decidability follow, proof search in the cyclic calculi can be automated, classical CK over S5 translates into ICK over S5, and all validity and proof-search problems lie in exponential time.

What carries the argument

Birelational Kripke models obeying an interaction principle between intuitionistic order and modal accessibility, equipped with analytic cyclic sequent calculi.

If this is right

Validity and satisfiability for each logic can be decided by an exponential-time procedure.
Proof search in the cyclic calculi is automatable and terminates.
Classical common knowledge over S5 embeds into the intuitionistic version over S5.
Each logic possesses the finite model property.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The exponential bound makes small multi-agent common-knowledge queries computationally feasible inside constructive settings.
The same cyclic-calculus technique may transfer to other intuitionistic modal operators beyond common knowledge.
The translation result suggests that classical epistemic conclusions can sometimes be recovered inside an intuitionistic framework without loss.

Load-bearing premise

The semantics are given by birelational Kripke models that satisfy a simple interaction principle between the intuitionistic order and the modal accessibility relations.

What would settle it

A concrete formula that is provable in one of the presented axiomatizations yet fails in some birelational model satisfying the interaction principle, or a formula valid in all such models yet unprovable in the corresponding cyclic calculus.

Figures

Figures reproduced from arXiv: 2605.00523 by Lukas Zenger.

**Figure 1.** Figure 1: The diagram above depicts the triangle confluence condition. The partial order view at source ↗

**Figure 2.** Figure 2: A cyclic proof for the induction axiom. Example 5.11. Recall that ¬φ is a shortcut for φ → ⊥. The sequent ⇒ Kap ∨ ¬Kap u has a proof in cICKS5, depicted below. id Kap u ⇒ Kap u , ⊥u ⇒ →Ka Kap u , Kap → ⊥u ∨R ⇒ Kap ∨ (Kap → ⊥) u Note that with the standard intuitionistic right implication rule, this proof is not possible: if →R is applied (bottom-up) to the sequent ⇒ Kap u , Kap → ⊥u , the premise is Kap u … view at source ↗

read the original abstract

We study an intuitionistic version of common knowledge logic (CK), called ICK, which was introduced by J\"ager and Marti. ICK extends intuitionistic propositional logic (IPL) by multiple box modalities interpreted as knowledge operators for various agents and a common knowledge operator. Formulae are interpreted over birelational Kripke models satisfying a simple interaction principle between the intuitionistic order and the modal accessibility relations. Furthermore, we consider the restriction to reflexive, S4 and S5 models. We present axiomatizations as well as analytic cyclic sequent calculi for all considered logics and prove them to be sound and complete. Furthermore, we establish the finite model property and decidability, show that proof-search in the cyclic calculi can be automated, provide a translation of CK over S5 into ICK over S5 and establish that the proof-search and validity problems of all considered logics can be solved in exponential time.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This paper supplies analytic cyclic sequent calculi, a useful S5 translation, and exponential-time bounds for intuitionistic common knowledge logics on top of the Jäger-Marti base.

read the letter

The main new pieces are the axiomatizations and analytic cyclic sequent calculi for ICK and its reflexive, S4, and S5 restrictions, together with the translation from classical CK over S5 into ICK over S5 and the exponential-time results for proof search and validity. These sit on top of the earlier ICK definition and give concrete proof systems plus decidability machinery that were not there before. The work also claims soundness, completeness, and the finite model property for all of them, which would be the expected package for this kind of extension. The birelational Kripke models with the stated interaction principle between the intuitionistic order and the modal relations are the standard minimal setup needed to interpret the modalities intuitionistically, so that part does not introduce extra assumptions. The cyclic rules for the common knowledge operator follow the usual fixed-point treatment and the paper presents them as working without special complications. No circular reasoning or parameter fitting appears in the setup. The soft spots are limited. Completeness for cyclic calculi can be delicate when common knowledge is involved, but the abstract and stress-test description give no sign of gaps, and the arguments are described as standard model-theoretic and proof-theoretic constructions. A referee would still want to inspect the details of the cyclic completeness proof to be sure the fixed-point handling carries over cleanly to the intuitionistic case. Overall the technical content is grounded and the claims are the sort that can be verified directly. This is for specialists in intuitionistic epistemic logic or cyclic proof systems who want decidability tools or automated-reasoning support. It has enough new formal results to justify sending it to peer review rather than a desk rejection.

Referee Report

0 major / 3 minor

Summary. The manuscript introduces intuitionistic common knowledge logic (ICK) as an extension of intuitionistic propositional logic with agent-specific knowledge modalities (box operators) and a common knowledge operator. Formulae are interpreted over birelational Kripke models equipped with an interaction principle between the intuitionistic preorder and the modal accessibility relations; variants are considered for reflexive, S4, and S5 frames. The paper supplies axiomatizations together with analytic cyclic sequent calculi for all variants, proves soundness and completeness, establishes the finite model property and decidability, shows that proof search in the cyclic calculi is automatable, gives a translation of classical CK over S5 into ICK over S5, and proves that validity and proof-search problems lie in EXPTIME.

Significance. If the central claims hold, the work supplies a technically complete treatment of common knowledge in an intuitionistic epistemic setting, including both Hilbert-style and cyclic sequent calculi. The analytic cyclic rules for the fixed-point operator, the finite-model property, and the explicit EXPTIME bound are substantive contributions that make the logics amenable to automated reasoning. The translation result further connects the intuitionistic and classical cases. These results are of clear interest to researchers working at the intersection of constructive logic and epistemic logic.

minor comments (3)

[Semantics section] The interaction principle between the intuitionistic order and the modal relations is stated as minimal yet load-bearing; a brief paragraph illustrating a model that violates it and showing the resulting failure of the knowledge axioms would clarify its necessity.
[Complexity results] The complexity argument for EXPTIME membership is stated for all considered logics; it would help to make explicit whether the number of agents is treated as a fixed parameter or part of the input size.
[Cyclic calculi] Notation for the common-knowledge operator and the cyclic rules is introduced without a small worked example of a cyclic derivation; adding one short derivation would aid readability for readers unfamiliar with cyclic calculi.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the manuscript and for recommending minor revision. The provided summary accurately captures the main results on axiomatizations, cyclic sequent calculi, finite model property, and EXPTIME decidability for ICK and its variants.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper defines ICK over birelational Kripke models with a stated interaction principle between the intuitionistic order and modal relations, then constructs axiomatizations and analytic cyclic sequent calculi whose soundness and completeness are proved directly from those semantics using standard model-theoretic and proof-theoretic techniques. The finite model property, decidability, and exponential-time bounds follow from the same constructions without any reduction to fitted parameters, self-definitional equations, or load-bearing self-citations. The translation from CK over S5 to ICK over S5 is a separate embedding result, not a renaming or ansatz smuggling. All steps are self-contained against external benchmarks such as classical modal logic completeness proofs and cyclic proof systems for fixed points.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper relies on standard intuitionistic propositional logic and modal logic background together with one new semantic assumption.

axioms (1)

domain assumption Birelational Kripke models satisfy a simple interaction principle between the intuitionistic order and the modal accessibility relations
This principle is invoked to define the semantics of the knowledge and common-knowledge operators.

pith-pipeline@v0.9.0 · 5442 in / 1309 out tokens · 40397 ms · 2026-05-09T15:05:41.859781+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

43 extracted references · 2 canonical work pages

[1]

Intuitionisticµ-calculus with the lewis arrow

Bahareh Afshari and Lide Grotenhuis. Intuitionisticµ-calculus with the lewis arrow. InIn- ternational Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pages 374–392. Springer, 2025

2025
[2]

Leigh, and Lukas Zenger

Bahareh Afshari, Lide Grotenhuis, Graham E. Leigh, and Lukas Zenger. Intuitionistic master modality. InAdvances in Modal Logic, volume 15, pages 19–40, 2024

2024
[3]

Leigh, and Lukas Zenger

Bahareh Afshari, Grotenhuis, Lide, Graham E. Leigh, and Lukas Zenger. Ill-founded proof systems for intuitionistic linear-time temporal logic. InAutomated Reasoning with Analytic Tableaux and Related Methods, volume 14278, pages 223–241, 2023. 72 Intuitionistic Common Knowledge

2023
[4]

Bahareh Afshari and Graham E. Leigh. Lyndon interpolation for modalµ-calculus. In Aybüke Özgün and Yulia Zinova, editors,Language, Logic, and Computation, pages 197–213, Cham,
[5]

Springer International Publishing
[6]

About cut elimination for logics of common knowledge

Luca Alberucci and Gerhard Jäger. About cut elimination for logics of common knowledge. Annals of Pure and Applied Logic, 133(1-3):73–99, 2005

2005
[7]

Intuitionisticepistemiclogic.The Review of Symbolic Logic, 9(2):266–298, 2016

SergeiArtemovandTudorProtopopescu. Intuitionisticepistemiclogic.The Review of Symbolic Logic, 9(2):266–298, 2016

2016
[8]

Intuitionistic logic

Nick Bezhanishvili and Dick de Jongh. Intuitionistic logic. Technical report, University of Amsterdam, 2006

2006
[9]

Boudou, M

J. Boudou, M. Diéguez, and D. Fernández-Duque. A decidable intuitionistic temporal logic. In 26th EACSL Annual Conference on Computer Science Logic, CSL 2017, August 20-24, 2017, Stockholm, Sweden, pages 14:1–14:17, 2017

2017
[10]

Exploring the jungle of intuitionistic temporal logics.Theory Pract

Joseph Boudou, Martín Diéguez, David Fernández-Duque, and Philip Kremer. Exploring the jungle of intuitionistic temporal logics.Theory Pract. Log. Program., 21(4):459–492, 2021

2021
[11]

PhD thesis, University of Edinburgh, 2006

James Brotherston.Sequent calculus proof systems for inductive definitions. PhD thesis, University of Edinburgh, 2006

2006
[12]

C. S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasipolynomial time. InProceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2017, page 252–263, New York, NY, USA, 2017. Association for Computing Machinery

2017
[13]

Sofía Santiago-Fernández David Fernández-Duque, Jost J. Joosten. The complexity of the constructive master modality.ArXiv:2603.05131v1, 2025

work page arXiv 2025
[14]

The intuitionistic temporal logic of dynamical systems.Logical Methods in Computer Science, 14(3):1–35, 2018

David Fernández-Duque. The intuitionistic temporal logic of dynamical systems.Logical Methods in Computer Science, 14(3):1–35, 2018

2018
[15]

A family of decidable bi- intuitionistic modal logics

David Fernández-Duque, Brett McLean, and Lukas Zenger. A family of decidable bi- intuitionistic modal logics. InProceedings of the International Conference on Principles of Knowledge Representation and Reasoning, volume 20, pages 262–271, 2023

2023
[16]

A sound and complete axiomati- zation for intuitionistic linear temporal logic

David Fernández-Duque, Brett McLean, and Lukas Zenger. A sound and complete axiomati- zation for intuitionistic linear temporal logic. InProceedings of the International Conference on Principles of Knowledge Representation and Reasoning, volume 21, pages 350–360, 2024

2024
[17]

Sur quelques points de la logique de m

Valery Glivenko. Sur quelques points de la logique de m. brouwer.Bulletin de la Société Mathématique de Belgique, 15:183–188, 1929

1929
[18]

Springer, 2002

Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors.Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001], volume 2500 ofLecture Notes in Computer Science. Springer, 2002

2001
[19]

Halpern and Yoram Moses

Joseph Y. Halpern and Yoram Moses. Knowledge and common knowledge in a distributed environment.J. ACM, 37(3):549–587, 1990

1990
[20]

A guide to completeness and complexity for modal logics of knowledge and belief.Artificial intelligence, 54(3):319–379, 1992

Joseph Y Halpern and Yoram Moses. A guide to completeness and complexity for modal logics of knowledge and belief.Artificial intelligence, 54(3):319–379, 1992

1992
[21]

An intuitionistic epistemic logic for sequential consistency on shared memory

Yoichi Hirai. An intuitionistic epistemic logic for sequential consistency on shared memory. In Logic for Programming, Artificial Intelligence, and Reasoning, pages 272–289, 2010

2010
[22]

A canonical model construction for intuitionistic distributed knowledge

Gerhard Jäger and Michel Marti. A canonical model construction for intuitionistic distributed knowledge. InAdvances in Modal Logic, volume 11, pages 420–434, 2016

2016
[23]

Intuitionistic common knowledge or belief.Journal of applied 73 Zenger logic, 18:150–163, 2016

Gerhard Jäger and Michel Marti. Intuitionistic common knowledge or belief.Journal of applied 73 Zenger logic, 18:150–163, 2016

2016
[24]

Semantical analysis of intuitionistic logic i

Saul Kripke. Semantical analysis of intuitionistic logic i. InFormal Systems and Recursive Functions. North Holland, 1965

1965
[25]

Intuitionistische untersuchungen der formalistischen logik.Nagoya Mathe- matical Journal, 2:35–47, 1951

Sigekatu Kuroda. Intuitionistische untersuchungen der formalistischen logik.Nagoya Mathe- matical Journal, 2:35–47, 1951

1951
[26]

Lewis meets brouwer: constructive strict implication.Inda- gationes Mathematicae, 29(1):36–90, 2018

Tadeusz Litak and Albert Visser. Lewis meets brouwer: constructive strict implication.Inda- gationes Mathematicae, 29(1):36–90, 2018

2018
[27]

PhD thesis, Universität Bern, 2017

Michel Marti.Contributions to Intuitionistic Epistemic Logic. PhD thesis, Universität Bern, 2017

2017
[28]

The proof theory of common knowledge

Michel Marti and Thomas Studer. The proof theory of common knowledge. InJaakko Hintikka on Knowledge and Game-Theoretical Semantics, 2018

2018
[29]

Donald A. Martin. Borel determinacy.Annals of Mathematics, 102(2):363–371, 1975

1975
[30]

PhD thesis, Uni- versiteit van Amsterdam, 2024

Guillermo Menéndez Turata.Cyclic proof systems for modal fixpoint logics. PhD thesis, Uni- versiteit van Amsterdam, 2024

2024
[31]

Intuitionistic epistemic logic with distributed knowledge

Ryo Murai and Katsuhiko Sano. Intuitionistic epistemic logic with distributed knowledge. Computación y Sistemas, 26(2):823–834, 2022

2022
[32]

Intuitionistic public announcement logic with distributed knowledge.Studia Logica, 112(3):661–691, 2024

Ryo Murai and Katsuhiko Sano. Intuitionistic public announcement logic with distributed knowledge.Studia Logica, 112(3):661–691, 2024

2024
[33]

Cambridge University Press, 2001

Sara Negri, Jan von Plato, and Aarne Ranta.Structural Proof Theory. Cambridge University Press, 2001

2001
[34]

Game semantics for the constructiveµ-calculus.arXiv preprint arXiv:2308.16697, 2024

Leonardo Pacheco. Game semantics for the constructiveµ-calculus.arXiv preprint arXiv:2308.16697, 2024

work page arXiv 2024
[35]

Intuitionistic epistemic logic, kripke models and fitch’s paradox.Journal of philosophical logic, 41(5):877–900, 2012

Carlo Proietti. Intuitionistic epistemic logic, kripke models and fitch’s paradox.Journal of philosophical logic, 41(5):877–900, 2012

2012
[36]

A formalization of the propositional calculus of H-B logic.Studia Logica: An International Journal for Symbolic Logic, 33(1):23–34, 1974

Cecylia Rauszer. A formalization of the propositional calculus of H-B logic.Studia Logica: An International Journal for Symbolic Logic, 33(1):23–34, 1974

1974
[37]

Semi-boolean algebras and their applications to intuitionistic logic with dual operations.Fundamenta Mathematicae, 83:219–249, 1974

Cecylia Rauszer. Semi-boolean algebras and their applications to intuitionistic logic with dual operations.Fundamenta Mathematicae, 83:219–249, 1974

1974
[38]

An analytic proof system for common knowledge logic over S5

Jan M W Rooduijn and Lukas Zenger. An analytic proof system for common knowledge logic over S5. InAdvances in Modal Logic, volume 14, pages 659–679, 2022

2022
[39]

D. S. Shamkanov. Circular proofs for the Gödel-Löb provability logic.Mathematical Notes, 96(3):575–585, 2014

2014
[40]

Common knowledge does not have the beth property.Information processing letters, 109(12):611–614, 2009

Thomas Studer. Common knowledge does not have the beth property.Information processing letters, 109(12):611–614, 2009

2009
[41]

Springer Science & Business Media, 2007

Hans Van Ditmarsch, Wiebe van Der Hoek, and Barteld Kooi.Dynamic epistemic logic. Springer Science & Business Media, 2007

2007
[42]

On intuitionistic modal epistemic logic.Journal of Philosophical Logic, 21(1):63–89, 1992

Timothy Williamson. On intuitionistic modal epistemic logic.Journal of Philosophical Logic, 21(1):63–89, 1992

1992
[43]

PhD thesis, Universiteit Gent, 2025

Lukas Zenger.Intuitionistic Dynamic Logic. PhD thesis, Universiteit Gent, 2025. 74

2025