ABSTRACT. In this talk I will discuss higher-order (“nested”) Kripke models [1], a generalization of traditional Kripke models that is remarkably close to Kripke’s original idea – both mathematically and conceptually. Standard models are now 0-ary models, whereas n-ary models for n > 0 are models whose set of objects (“possible worlds”) contain only (n − 1)-ary models. The models for non-classical logics are introduced after the paradigmatic cases of intuitionistic modal logics IK and M K (a logic stronger than IK) are considered. The n-ary models (for n > 0) define a concept of “alternative” for any substantial interpretation of the (n − 1)-ary models. The key ideas behind the new semantics are the nesting of models, the use of particular worlds w as “designated points” for their own modal definitions, and the use of relations between models at each level n. We start by defining higher-order models as follows: Definition 1 Any Kripke model is a 0-ary model ⟨M, ≻, v⟩, where W is a set of objects, R a binary relation over W , and v a function assigning sets of atoms to elements of W. Definition 2 A n-ary model is a Kripke model ⟨M, ≻, v⟩, where W is a set of (n − 1)-ary models. In the case of IK and M K, 0-ary models are defined as the traditional intuitionistic propositional Kripke models [2, pg. 21], and modal models are defined using only 1-ary models. In order to notationally distinguish between 1-ary and 0-ary models in this abstract, we denote 1-ary models by ⟨M, ≻, f⟩ and 0-ary models K by ⟨W_K, ≤K , vK ⟩. We then move from the abstract definition of model to a concrete intuitionistic one as follows: Definition 3 A set of 0-ary models is homogeneous if its models are de- fined over the same frame (e.g same sets W and relation ≤), and partially homogeneous if it contains a model M such that every other model is de- fined over a generated subframe [3, pg. 28] of the frame of M . Definition 4 An 1-ary model is a model for IK if its set M is partially homogeneous, and a model for MK if it is homogeneous. When we consider n-ary models in general, in any model ⟨M, ≻, v⟩ of level n > 0, validity of □A or ♢A in a world w ∈ M (which is a (n − 1)-ary model) depends only on which formulas are valid in other models w′ of M such that w ≻ w′ whose frames coincide at least in part with that of w. In the case of 1-ary models for IK, this is achieved through the following clauses, where 1 is a 1-ary model, K one of its 0-ary models, and w ∈ WK : ⊨1,Kw □A ⇐⇒ for all w′ with w ≤K w′, if K ≻ K′ and w′ ∈ W_K′ then ⊨1,K′w′ A; ⊨1,Kw ♢A ⇐⇒ there is a K′ with K ≻ K′ such that w ∈ K′ and ⊨1,K′w A; A modal accessibility K ≻ K′ is vacuous whenever the intersection of the objects in the frames of K and K′ is empty. If the intersection is non- empty, something is necessary in a world w iff it is true in all occurrences of the same w or in the w ≤ w′ in other accessible models, and it is possible if it is true in the w of at least one accessible model. Intuitively, given any substantial interpretation of w and M, the defi- nitions consider only alternative versions of the same entities; for instance, if w is interpreted as a particular moment in time and M as a timeline, modal validity in w is defined by considering only what is or is not true in the same moment w in time (or future moments) but in the accessi- ble “alternative timelines”. The traditional interpretation of accessibility relations in Kripke models as establishing different “possible worlds” is now lifted to a higher level and applied to Kripke models themselves by considering differences in the interpretation of their shared structure. This perspective becomes clearer when we consider clauses for MK, which is the strongest possible intuitionistic modal logic obtainable by requiring birelational models to satisfy frame conditions [2, pg. 46][4]. The clauses only considers alternative versions of the same world: ⊨1,Kw □A ⇐⇒ for all K′ such that K ≻ K′, we have ⊨1,K′w A; ⊨1,Kw ♢A ⇐⇒ there is a K′ with K ≻ K′ such that ⊨1,K′w A; The only intuitionistic thing about semantics for MK is the use of intuitionistic 0-ary models, so if we were to use 0-ary models for some other logic we would obtain a (very strong) modal logic for it. Weaker logics can also be obtained, although in some cases (such as that of IK) the semantic clauses might require reference to the specific non-modal relations defined for objects of the models. It is also the case that imposing conditions on n-ary relations for any modal logic yields the semantics traditionally obtained through the same conditions (e.g. by requiring the 1-ary relation to be reflexive and transitive the semantics for IK becomes one for IS4). We are currently working with collaborators to show that, if models are not required to share any structure, the framework provides a semantics for the intuitionistic modal logic WK [5], and a simple modification yields one for CK [4]. We are also investigating new sequent calculi obtainable by reflecting the semantic structures of the new models. The relationship between the semantics and first-order intuitionistic structures is yet to be investigated. Our results indirectly show that a mapping into first-order intuitionistic logic is available by mapping 1-ary models into birelational models, but it is unclear what a “direct mapping” would look like. Although 1-ary validity in models for IK and MK is fully determined by validity in 0-ary models (in the sense that something is valid in a 1-ary model iff it is valid in all its 0-ary models), this needs not always be the case. The framework may be capable of providing Kripke-like semantics to Kripke-incomplete logics if n-ary validity is defined in a way that makes it irreducible to (n − 1)-ary validity. This might open the door to simple but conceptually interesting characterisations of an ever broader class of intuitionistic modal logics, including non-normal ones. Keywords: Intuitionistic Logic, Intuitionistic Semantics, Modal Semantics, Relational Semantics, Higher-order Kripke models. References: [1] Barroso-Nascimento, Victor. “Higher-order Kripke models for intuitionis- tic and non-classical modal logics”. ArXiV Preprint, 2025. Available at: https://arxiv.org/abs/2507.18798 [2] Simpson, Alex “The Proof Theory and Semantics of Intuitionistic Modal Logic”. Ph.D. thesis, 1994. [3] Chagrov, Alexander and Zakharyaschev, Michael. “Modal logic”. Oxford University Press, New York, 1997. [4] Bozic, Milan and Dosen, Kosta. “Models for normal intuitionistic modal logics”. Studia Logica, pgs. 43:217-245, 1984. [5] Wijesekera, Duminda “Constructive modal logics I”. Annals of Pure and Applied Logic, 50:271-301, 1990.

ABSTRACT. In a recent paper, de Groot and Shillito proved that iS4 is sound and complete with respect to all models ⟨W, ⪯, τ, V ⟩, where: ⟨W, ⪯, V ⟩ is a model for IPC, ⟨W, τ ⟩ is a topology, and all open sets of τ are upwards closed with respect to ⪯. Furthermore, they showed that completeness still holds even if we require ⪯ to be the specialisation order of τ . In this sense, iS4 is complete with respect to all topological models. We extend their result in two directions. First, we prove analogous topological completeness results for various logics related to iwK4, an intuitionistic version of the logic wK4 of weak transitive frames. In our setting, we interpret the □ modality via the coderivative operator—the dual of the Cantor derivative—instead of the interior operator. We can also omit the intuitionistic relation ⪯—as long as we interpret it as a coderivative specialisation order. Second, we prove completeness with respect to various classes of bimetric spaces. We do not have completeness if we restrict ourselves to models consisting of an intuitionistic relation and a metrizable topological space: in this setting the ordering ⪯ needs to be the equality relation and so the logic becomes classical.

ABSTRACT. We develop polytopological semantics for various constructive, intuitionistic, and Gödel-Dummett variations of K4 and S4. In our models, intuitionistic and modal operators are interpreted via various topologies over a single set, equipped with either the closure or derivative operators. We identify regularity conditions to ensure that spaces validate each of our target logics and prove that all the logics considered are sound and strongly complete with respect to their respective semantics.

ABSTRACT. Recently, Ramesh has introduced new categorical concepts, introspective theories and geminal categories, which formalize "self-internalizing" structures sharing the form of Löb's theorem ($\square A \vdash A$ implies $\vdash A$). We reorganize the theory of geminal categories in a self-contained manner by introducing "code structures on fibrations," which serve as a categorical abstraction of Gödel coding. This approach leads to a generalization and a significant simplification of the proof of Löb's theorem for geminal categories, yielding a categorical counterpart of the Gödel–Löb axiom ($\square (\square A \to A) \to \square A$). This formulation offers an accessible framework for Ramesh's ideas. Moreover, we analyze the relationships between geminal categories and existing modal calculi such as Kavvos' DGL. While establishing the formal relationship requires further investigation, the strong resemblance between them suggests that there might be common categorical structures underlying metamathematics (the second incompleteness theorem) and metaprogramming (intensional recursion), unifying meta- and object-level interactions in logic and computer science.

ABSTRACT. Decidability of intuitionistic S4 has been an open question since the problem was formulated by Simpson (1994). We thought to have settled the issue: our LICS'23 claimed that IS4 was decidable, and provided a proof-theoretic algorithm to calculate the truth value of formulas. However, some six months after publication, Agi Kurucz designed a clever yet simple IS4 formula which could not be decided by our algorithm. In this talk, we set the record straight by discussing the main ideas behind our LICS '23 paper, explore Kurucz's counterexample, and discuss ongoing work on solutions to the problem of showing decidability of IS4.

ABSTRACT. We develop a second-order extension of intuitionistic modal logic, allowing quantification over propositions, both syntactically and semantically. A key feature of second-order logic is its capacity to define positive connectives from the negative fragment. Duly we are able to recover the diamond (and its associated theory) using only boxes, as long as we include both forward and backward modalities (‘tense’ modalities). We propose axiomatic, proof theoretic and model theoretic definitions of ‘second-order intuitionistic tense logic’, and ultimately prove that they all coincide. In particular we establish completeness of a labelled sequent calculus via a proof search argument, yielding at the same time a cut-admissibility result. Our methodology also applies to the classical version of second-order tense logic, which we develop in tandem with the intuitionistic case.

ABSTRACT. We develop non-commutative linear intuitionistic versions SIK, SIT, SIK4, SIS4 of modal logics K, T, K4 and S4 with multiplicative truth, conjunction and box (and also implication) in terms of sequent calculi. Each of these sequent calculi has cut admissible and is sound and complete, in particular in regards to equality of proofs, wrt. the appropriate categorical semantics. The box modality is interpreted as a strong monoidal functor in the case of K and progressively strengthens to a strong monoidal comonad in the case of SIS4. We use a sequent format where antecedents are lists of formulae indexed by natural numbers for box-depths. For a variant SIS4* of SIS4 where box is an idempotent strong monoidal comonad (satisfying more equations than in the basic non-idempotent case), these indices can be restricted to 0, 1. This corresponds to unboxed and boxed compartments of antecedents in sequent calculi for logics with exchange.

ABSTRACT. We duscuss the results of the paper (Dalmonte, Rev. Symb. Log. 2025), that presents a systematisation of a family of constructive modal logics and their relations with modal logics with a minimal basis.

ABSTRACT. The proof system KE is a variant of analytic tableaux, but it is more efficient than these. Namely, KE polynomially simulates tableaux, while the reverse relation does not hold [2]. Indeed, there are exponentially shorter proofs in KE w.r.t. some classes of formulas. Its hallmark is reducing the amount of branching to a minimum by making all branches mutually exclusive. Specifically, KE has only one branching rule that corresponds to a non-eliminable analytic-cut rule. The rest of the rules all have a non-branching format and correspond to traditional reasoning patterns such as modus ponens, modus tollens, disjunctive syllogism and its dual, etc. Recently, Balbiani and Gencer [1] put forward a uniform framework for characterizing a robust family of intuitionistic modal logics that, in te spirit of Fischer-Servi’s IK, contains “the formulas whose standard translation in a first-order language are intuitionistically valid”. The authors provided both axiomatic and semantic characterizations of these logics. In particular, a bi-relational semantics is given, where the conditions for ♢ depart from the traditional ones. Namely, ♢A is forced at a state w in a model (W,≤,R, V ) if and only if there exists an state w′ such that w≥◦Rw′ and A is forced at w′, where ≥◦R denotes the composition of the intuitionistic preorder ≥ and the accesibility relation R. Under this framework, the axiomatization of validity in the class of all models constitutes a minimal logic, Lmin, which is in that sense analogous to its classical counterpart K. While incomparable with Wijesekera’s WK, the logic Lmin is strictly contained in IK that, in turn, corresponds to validity in the class of all forward and backward confluent models. Other classes of models associated with different confluence conditions between ≤ and R—the latter possibly under a further condition of reflexivity, symmetry and transitivity—induce other logics, some of which can be axiomatized and belong to the family whose basis is Lmin. Now, we [5] recently extended the tableau-like KE system to intuitionistic propositional logic by means of labeled signed formulas so as to mimic countermodel-search in the relational semantics. Besides inheriting KE’s hallmark of reducing branch to a minimum—and unlike the currently most efficient SAT-based methods [e.g. 3]—our intuitionistic KE enjoys native interpretability within its underlying semantics and is modular in that it can naturally implement the “axiom-to-rule” methodology. In the line of Marin et al. [4], in this work we apply that methodology to a familiy of intuitionistic modal logics as characterized by Balbiani and Gencer’s framework. Namely, we enrich our intuitionistic KE system (IKE) with rules for the modalities, following the characterization of [1], to obtain a KE system that corresponds to Lmin and then—by adding rules corresponding to further frame conditions or axioms—we obtain systems corresponding to a family of logics thereof. Soundness of the resulting systems is straightforward given that the labels mechanism basically mimics the underlying bi-relational semantics. As for completeness, for the time being, we have proven it by simulating the axiomatic characterizations of each of the logics. That is, we have shown that each rule of the corresponding axiomatic system can be simulated in the respective KE system, while each axiom can be derived as a theorem therein. However, we discuss how the arguments for termination via countermodel extraction, given in [5] for the plain intuitionistic case, can be extended so as to cover our intuitionistic modal KE-style systems. As a whole, we show how our intuitionistic proof system IKE can be modularly extended to include modalities in a very natural way. References [1] P. Balbiani and C¸ . Gencer. Intuitionistic modal logics: A minimal setting. Studia Logica, pages 1–68, 2026. [2] M. D’Agostino and M. Mondadori. The taming of the cut. Classical refutations with analytic cut. Journal of Logic and Computation, 4(3):285–319, 1994. [3] C. Fiorentini. Efficient SAT-based Proof Search in Intuitionistic Propositional Logic. In A. Platzer and G. Sutcliffe, editors, Automated Deduction– CADE 28, pages 217–233, Cham, 2021. Springer International Publishing. [4] S. Marin, M. Morales, and L. Straßburger. A fully labelled proof system for intuitionistic modal logics. Journal of Logic and Computation, 31(3):998–1022, 2021. [5] A. Solares-Rojas, P. Baldi, and R. O. Rodriguez. Labeled KE for intuitionistic propositional logic. Manuscript conditionally accepted in Journal of Logic and Computation, 2026.