Inferentialist games, component modalities, and intuitionistic dynamics: four July logic works

Four works posted or revised between 12 and 16 July put the same pressure on different parts of non-classical logic: what must a semantics remember so that proof, validity, and consequence still line up? Waddington, Gheorghiu, and Pym make proof-search itself the object of a game; Zenger builds intuitionistic modal systems for change and information update; Tokuo makes modal accessibility constant within quantum-compatibility components; Kurahashi and Noguchi weaken intuitionistic semantics until formula-indexed relations carry the missing structure. The papers do not establish a field-wide turn, but together they give a precise local result: semantic adequacy is being obtained by exposing structural invariants instead of hiding them behind a generic notion of model.

The useful comparison is not that these works all study "intuitionistic logic" in the same way. They do not. It is that each one makes an otherwise easy-to-ignore piece of structure answer for a familiar metatheoretic demand. The first paper asks what a proof means as an interaction. The second asks how proof systems and models cope with change. The third asks which modal distinctions survive quantum compatibility. The fourth asks how little relational structure remains when ordinary intuitionistic assumptions are removed.

Waddington, Gheorghiu, and Pym start with a problem in proof-theoretic semantics. Base-extension semantics replaces a model-theoretic satisfaction relation with support relative to a base of atomic rules. Hyland-Ong games, by contrast, describe reasoning through moves between a Proponent and an Opponent. The authors' extended abstract asks whether the game can be reconstructed from the proof-theoretic primitives rather than imposed as an external model. 1

Their dictionary is concrete: a base becomes an arena, an argument from assumptions becomes a play, and a proof becomes a winning strategy. The result is a game-extension semantics for intuitionistic propositional logic. The paper states soundness and completeness for IPL, and uses a 4x4 Sudoku example to show how a domain that is not initially presented as logical consequence can still be organized as an arena of challenges and responses. 1

The important move is the direction of explanation. A winning strategy is not merely a model-theoretic witness that a formula is true. It records how a claim survives the sequence of challenges permitted by the arena. That gives inferentialism a dynamic object without abandoning proof-theoretic control. The paper is an extended abstract, so its scope is narrow: the central correspondence is established for IPL, not for every logic that admits a game presentation.

Zenger's Intuitionistic Dynamic Logic takes the neighboring problem of change directly. The thesis studies five systems: intuitionistic master modality, intuitionistic common knowledge logic, intuitionistic linear temporal logic, bi-intuitionistic modal logic, and bi-intuitionistic linear temporal logic. It combines Hilbert-style axiomatizations with non-wellfounded and cyclic sequent calculi, and studies birelational Kripke models satisfying confluence and other frame conditions. 2

The relation between the two works is methodological rather than bibliographic. Waddington and colleagues turn proof-search interaction into the semantic object. Zenger turns temporal, epistemic, and modal change into the relational object that proof systems must track. In both cases, a non-classical semantics earns its adequacy by retaining the structure that a proof actually uses. The first paper makes that structure sequential and dialogical; the thesis makes it persistent across dynamic transitions.

Kenji Tokuo's Component Modalities of Quantum Logic begins with a forcing condition connecting the compatibility relation of an orthoframe to modal accessibility. The paper proves that this condition makes modal successor sets constant on each compatibility component. In a connected frame, every allowed modal relation therefore has one common successor set. 3

That structural theorem has two consequences. First, boxed truth sets become unions of compatibility components, placing them in a canonical Boolean subalgebra of the stable-set ortholattice. In hard superselection models, the paper identifies the corresponding component algebra with the center of the product of sector lattices. Second, the paper argues that ordinary fixed-conclusion readings of multiple-conclusion sequents are too rigid for disconnected frames.

The replacement is local sequent validity: at each world, at least one conclusion must hold, but the selected conclusion may vary from world to world. This is what makes modal excluded middle valid when one component satisfies the boxed formula and another satisfies its quantum negation. Tokuo then proves soundness and completeness for the base calculus and for its T, 4, and B extensions, using maximal consistent pairs in a canonical model. 3

This is a sharper result than the generic claim that quantum logic is non-classical. The paper identifies the exact place where non-classical structure changes the consequence relation: disconnected compatibility components make a locally selected conclusion legitimate even when no single conclusion holds throughout the model. The semantic choice is doing proof-theoretic work.

That point connects Tokuo to Zenger, but the difference matters. Zenger's birelational models represent evolving information and temporal states. Tokuo's component decomposition controls which modal distinctions can vary across quantum-compatible regions. Both make relational structure visible, yet they preserve different kinds of variation: dynamic transition in one case, componentwise modal uniformity in the other.

Taishi Kurahashi and Mashu Noguchi's Very weak subintuitionistic logics moves in the opposite direction from a richer dynamic language. The authors introduce VF by adapting the relational semantics of Fitting, Marek, and Truszczyński's pure logic of necessitation to a propositional setting. Their propositional FMT semantics uses a family of relations indexed by formulas rather than one ordinary accessibility relation. 4

The paper proves soundness and completeness for VF and its closed negative extensions, along with the disjunction property and finite frame property. It also proves that VF is strictly weaker than Maleki and de Jongh's WF, and studies modal companions through Corsi's modified Gödel translation. The paper says that all of its results have been formalized and verified in Lean 4, with the formalization released through the Formalized Formal Logic project. 4

The July date needs care. The arXiv page identifies version 2 on 12 July 2026, while Semantic Scholar lists the paper's publication date as 20 May 2026. This is a revision signal, not a brand-new paper. Its result still belongs in the current comparison because the revision is the record available in the present window, but the citation clock should not be reset silently.

VF and Tokuo's component logic expose different forms of weakness. VF weakens the propositional base and compensates with formula-indexed relations. Tokuo constrains modal accessibility through compatibility components and then changes the validity clause for multiple conclusions. In both cases, the authors do not treat "weak" as equivalent to "underspecified." They specify the structure that remains and prove what that structure can still support.

Semantic Scholar's current records show no citations or influential citations for any of the four works. The reference counts are 45 for Waddington, Gheorghiu, and Pym; 12 for Tokuo; 0 for Zenger's thesis; and 24 for Kurahashi and Noguchi. 5 6 7 8

Google Scholar supplied no usable indexed records for these exact titles in the current check. That leaves no second-index movement to compare. The defensible reading is therefore publication clustering without measurable citation momentum. The numbers are too young, and in one case reflect a version history, to support a claim that one subfield is already gaining traction.

The more useful signal is structural. Each work names a constraint that a generic model description might leave implicit: a strategy's response policy, a dynamic frame's confluence conditions, a modal relation's component invariance, or an indexed relation's formula sensitivity. Citation data cannot yet rank these approaches. The papers themselves can show where their proofs require the structure to be made explicit.

These four works do not show that philosophical logic as a whole is moving toward one new paradigm. They do show a shared technical pressure across distinct problems. When classical uniformity is weakened, semantic adequacy depends on remembering the right distinctions: which challenge has been made, which transition is available, which compatibility component a world occupies, or which formula indexes the relation being used.

That is why the papers sit well together despite their different vocabularies. Their common contribution is not a new label for the field. It is a discipline of construction: expose the invariant, alter the consequence relation only where the invariant requires it, and then prove soundness or completeness against that choice. The July papers make that discipline visible in games, dynamic logics, quantum components, and very weak subintuitionistic frames.