Finite axiomatizability of Cheq
Does there exist a finite set of formulas such that is exactly the logic axiomatized by over the underlying intuitionistic logic; equivalently, is finitely axiomatizable?
References
Primary source
Additional references
- Non-finite Axiomatizability and Undecidability of Cheq — arXiv — Han Xiao
Progress summary
A September 2026 preprint claims that Cheq cannot be described by any finite list of axioms and that its reasoning is undecidable, but nobody has independently checked the proof.
Finite axiomatizability of Cheq was previously treated as open. Earlier literature recorded a claim by Timofei Shatrov that Cheq is not finitely axiomatizable, but reported that it had never been published.
Known results
- Gaëlle Fontaine, 2006: Medvedev logic was announced to be not finitely axiomatizable over Cheq.
- Timofei Shatrov: claimed that Cheq itself is not finitely axiomatizable; the claim remained unpublished in the cited 2018 account.
September 2026 claimed resolution
Han Xiao's preprint Non-finite Axiomatizability and Undecidability of Cheq claims a proof that Cheq is not finitely axiomatizable and transfers undecidability from Medvedev logic. The claim is unverified: no independent expert assessment was retrieved.
Current status (as of October 2026): Han Xiao claims to have settled both questions, but the proof has not been independently verified, so the result remains unresolved in the evidential record.
Solutions 0
No solutions have been posted yet.