Papers With

← All papers
First page of Very weak subintuitionistic logics

Very weak subintuitionistic logics

Taishi Kurahashi, Mashu Noguchi

math.LO May 20, 2026 · v2
formalization logic
Read PDF arXiv abstract Code
TL;DR
All results on the very weak subintuitionistic logic VF, its semantics and modal companions are stated to be formalized and verified in Lean 4.
Abstract
We introduce a new propositional logic, called very weak subintuitionistic logic $\mathbf{VF}$, by adapting the relational semantics of Fitting, Marek, and Truszczyński for the pure logic of necessitation $\mathbf{N}$ to the propositional setting. We prove that $\mathbf{VF}$ and its closed negative extensions are sound and complete with respect to this semantics, and that they have the disjunction property and the finite frame property. We also prove that $\mathbf{VF}$ is strictly weaker than the weak subintuitionistic logic $\mathbf{WF}$ of Maleki and de Jongh. Finally, we study modal companions of $\mathbf{VF}$ and its closed negative extensions via Corsi's modified Gödel translation.
Problem

Subintuitionistic logics drop the preorder and persistency conditions of intuitionistic Kripke semantics. The work seeks a propositional logic weaker than Maleki and de Jongh's WF, modeled on the Fitting–Marek–Truszczyński semantics for the pure logic of necessitation N.

Approach

The logic VF is defined by a Hilbert system, together with its closed negative extensions. A propositional FMT semantics is introduced in which accessibility relations are indexed by formulas. The disjunction property is proved via Aczel's slash, and completeness and the finite frame property via finite tableaux. Modal companions are obtained through Corsi's modified Gödel translation. All content is reported as formalized in Lean 4.

Results

VF and its closed negative extensions are sound and complete for FMT semantics and have the disjunction property and the finite frame property. VF is strictly weaker than WF, and N is a modal companion of VF, with closed negative extensions corresponding to closed modal extensions of N.