Rule extensions of the implication--negation fragment of intuitionistic logic

@misc{kowalski2026rule,
  title = {{Rule extensions of the implication--negation fragment of intuitionistic logic}},
  author = {Tomasz Kowalski and Katarzyna Słomczyńska},
  howpublished = {arXiv},
  year = {2026},
  month = nov,
  doi = {10.48550/arxiv.2611.05928},
  eprint = {2611.05928},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2611.05928},
  note = {CC BY 4.0},
}

TY  - UNPB
TI  - Rule extensions of the implication--negation fragment of intuitionistic logic
AU  - Tomasz Kowalski
AU  - Katarzyna Słomczyńska
PY  - 2026
DA  - 2026/11/04
PB  - arXiv
DO  - 10.48550/arxiv.2611.05928
UR  - https://arxiv.org/abs/2611.05928
AB  - We present an algebraic study of extensions of the implication--negation fragment IPC_→,¬ of intuitionistic propositional logic. Such extensions by inference rules correspond to subquasivarieties of the variety varHo of Hilbert algebras with zero. We describe the lattice of such extensions of IPC_→,¬ by means of its generators: it is isomorphic to the lattice of upsets of a countable poset, and in particular it is completely distributive. Consequently, varHo is not Q-universal, in contrast to several other varieties related to IPC. Nevertheless, this lattice is very complex: at each suitably defined height it has intervals containing continuum many quasivarieties which are not varieties. To the best of our knowledge IPC_→,¬ is the only natural fragment of intuitionistic logic known to combine a completely distributive lattice of extensions with continuum many non-axiomatic extensions.
ER  -