arXiv subjects

Rodrigo Nicolau Almeida

Publications and source records attributed to Rodrigo Nicolau Almeida.

14 recordsLinked to original sources

arXiv2026

Medvedev logic is undecidable

We show that Medvedev's logic of finite problems, a well-known superintuitionistic logic, is undecidable. The key method is a reduction from the periodic tiling problem to non-theoremhood in Medvedev's logic. This settles a longstanding open problem. Using similar techniques, but reducing instead to the ordinary tiling problem, we likewise obtain undecidability of Skvortsov's logic of infinite problems, and the fact that the two logics are distinct -- in fact, they are separated by any aperiodic tiling of the plane. Due to the fact that Medvedev's logic figures in so many different areas, these results have implications for several fields -- for example, the study of schematic fragments of logics such as propositional dependence logic, or the study of internal logics of toposes. The core idea and technical work of the undecidability proof were obtained using ChatGPT Sol 5.6, and formally verified in Lean by Claude Opus 5. A detailed methodology section outlines how such results were obtained.

math.LO↗

arXiv2026

Uniform Local Tabularity in Intuitionistic Logic

By contrast with S4, the analysis of local tabularity above IPC has provided a difficult challenge. This paper studies a strengthening of local tabularity - uniform local tabularity - where one demands that all formulas be equivalent to formulas of a given implication depth. Algebraically, this amounts to considering Heyting algebras generated by finitely many iterations of the implication operation. It is shown that in contrast with locally finite Heyting algebras, n-uniformly locally finite Heyting algebras always form a variety, and an explicit axiomatization of the variety of n-uniform locally finite Heyting algebras for n below 3 is given. In connection with this analysis, it is shown that there exist locally tabular logics which are not uniformly locally tabular, answering a question of Shehtman - an example of a pre-uniformly locally tabular logic is presented, which is shown to be the unique pre-uniformly locally tabular extension of the system KG.

math.LO↗

arXiv2026

Coequivalence Relations and Descent in Modal Logic

A coequivalence relation over a modal logic L is a formula in two tuples of propositional variables of the same length such that the logic L proves it to be an equivalence relation. They were introduced by Ghilardi and Zawadowski in the context of the categorical study of non-classical logics. A coequivalence relation is said to separate variables or to be separating if it corresponds to a collection of formulas, which serve as explicit definitions of quotients. A logic L where all coequivalence relations are separating is said to have the coequivalence separation property (CoSP). Ghilardi and Zawadowski showed that CoSP fails for IPC. In previous work, the second author showed that such a phenomenon happens already in presumably simpler systems like S5. Ghilardi and Zawadowski therefore raised the question whether a weaker property, formulated in categorical terms related to descent theory, was still true. In this paper, we identify the logical meaning of such a property in relation to CoSP. We introduce the notion of local coequivalence relations, which have the additional structure of a local transition term, intuitively capturing the structure of elements lying in the same fiber. We introduce the local coequivalence separation property (LCoSP), and prove it to be equivalent, in good cases, to the almost Barr-exactness of the category dual to finitely presented algebras. We conclude by showing that S5 has the LCoSP.

math.LO↗

arXiv2026

A topos for étale-finite Heyting algebras

A longstanding open problem is whether every Heyting algebra is the lattice of truth values (i.e., of subterminal objects) of some elementary topos. A positive answer is known for complete Heyting algebras (i.e., locales) via sheaves, and for Boolean algebras via a construction due to Peter Freyd. We extend Freyd's construction to all étale-finite Heyting algebras, in the sense of Evgeny Kuznetsov. These are the Heyting algebras satisfying a generalisation of the law of excluded middle relative to some finite Heyting subalgebra. For every étale-finite Heyting algebra $H$, we use Esakia duality to construct an elementary topos whose lattice of truth values is isomorphic to $H$, thereby extending the class of Heyting algebras for which a positive answer to the Heyting-to-topos problem is known. The toposes we construct are categories of certain compact étale spaces. As a consequence, they are finitely propositional: every object has a finite cover by subterminal objects. We show that a Heyting algebra occurs as the lattice of truth values of some finitely propositional topos if and only if it is étale-finite. This exhibits an obstruction to extending the use of compact étale spaces beyond the étale-finite case.

math.LO↗

arXiv2026

Fischer-Servi logic does not have interpolation

We prove that the Fischer-Servi logic $\mathsf{IK}$ does not have the (Craig) interpolation property. This is obtained by showing that the corresponding class of modal Heyting algebras lacks the amalgamation property. We also generalize this result to some extensions of the Fischer-Servi logic such as $\mathsf{IT}$, $\mathsf{IK4}$, $\mathsf{IS4}$, and $\mathsf{IGL}$.

math.LO↗

arXiv2026

Colimits of Heyting Algebras through Esakia Duality

In this note we generalize the construction, due to Ghilardi, of the free Heyting algebra generated by a finite distributive lattice, to the case of arbitrary distributive lattices. Categorically, this provides an explicit construction of a left adjoint to the inclusion of Heyting algebras in the category of distributive lattices This is shown to have several applications, both old and new, in the study of Heyting algebras: (1) it allows a more concrete description of colimits of Heyting algebras, as well as, via duality theory, limits of Esakia spaces, by knowing their description over distributive lattices and Priestley spaces; (2) It allows a direct proof of the amalgamation property for Heyting algebras, and of related facts; (3) it allows a proof of the fact that the category of Heyting algebras is co-distributive. We also study some generalizations and variations of this construction to different settings. First, we analyse some subvarieties of Heyting algebras -- such as Boolean algebras, $\mathsf{KC}$ and $\mathsf{LC}$ algebras, and show how the construction can be adapted to this setting. Second, we study the relationship between the category of image-finite posets with p-morphisms and the category of posets with monotone maps, showing that a variation of the above ideas provides us with an appropriate general idea.

math.LO↗

arXiv2026

Superamalgamation for modal lattices via non-distributive dualities

We show that the variety of modal lattices has the superamalgamation property. As a consequence, we obtain that the weak positive modal logic has the Craig interpolation property. Our proof employs the recent duality for modal lattices based on modal L-spaces. Moreover, we extend this result to a number of other weak positive modal logics axiomatized by modal axioms corresponding to universal Horn sentences.

math.LO↗

arXiv2025

Esakia order-compactifications and locally Esakia spaces

We introduce Esakia order-compactifications and study how they fit in the general theory of Priestley order-compactifications. We provide an analog of Dwinger's theorem by characterizing Esakia order-compactifications by means of special rings of upsets. These considerations naturally lead to the notion of a locally Esakia space, for which we prove that taking the largest Esakia order-compacification is functorial, thus obtaining an analog of Banaschewski's theorem.

math.LO↗

arXiv2025

Structural Completeness in bi-IPC

In this note we show that no extension of bi-intuitionistic logic, except for classical logic, is structurally complete; indeed, none of them are passively structurally complete. A direct proof of active structural completeness is given for some simple systems.

math.LO↗

arXiv2024

Maximality Principles in Modal Logic and the Axiom of Choice

We investigate the set-theoretic strength of several maximality principles that play an important role in the study of modal and intuitionistic logics. We focus on the well-known Fine and Esakia maximality principles, present two formulations of each, and show that the stronger formulations are equivalent to the Axiom of Choice (AC), while the weaker ones to the Boolean Prime Ideal Theorem (BPI).

math.LO↗

arXiv2024

$Π_{2}$-Rule Systems and Inductive Classes of Gödel Algebras

In this paper we present a general theory of $Π_{2}$-rules for systems of intuitionistic and modal logic. We introduce the notions of $Π_{2}$-rule system and of an Inductive Class, and provide model-theoretic and algebraic completeness theorems, which serve as our basic tools. As an illustration of the general theory, we analyse the structure of inductive classes of Gödel algebras, from a structure theoretic and logical point of view. We show that unlike other well-studied settings (such as logics, or single-conclusion rule systems), there are continuum many $Π_{2}$-rule systems extending $\mathsf{LC}=\mathsf{IPC}+(p\rightarrow q)\vee (q\rightarrow p)$, and show how our methods allow easy proofs of the admissibility of the well-known Takeuti-Titani rule. Our final results concern general questions admissibility in $\mathsf{LC}$: (1) we present a full classification of those inductive classes which are inductively complete, i.e., where all $Π_{2}$-rules which are admissible are derivable, and (2) show that the problem of admissibility of $Π_{2}$-rules over $\mathsf{LC}$ is decidable.

math.LO↗

arXiv2024

A Coalgebraic Semantics for Intuitionistic Modal Logic

We give a new coalgebraic semantics for intuitionistic modal logic with $\Box$. In particular, we provide a colagebraic representation of intuitionistic descriptive modal frames and of intuitonistic modal Kripke frames based on image-finite posets. This gives a solution to a problem in the area of coalgebaic logic for these classes of frames, raised explicitly by Litak (2014) and de Groot and Pattinson (2020). Our key technical tool is a recent generalization of a construction by Ghilardi, in the form of a right adjoint to the inclusion of the category of Esakia spaces in the category of Priestley spaces. As an application of these results, we study bisimulations of intuitionistic modal frames, describe dual spaces of free modal Heyting algebras, and provide a path towards a theory of coalgebraic intuitionistic logics.

math.LO↗

arXiv2024

Unification with Simple Variable Restrictions and Admissibility of $Π_{2}$-rules

We develop a method to recognize admissibility of $Π_{2}$-rules, relating this problem to a specific instance of the unification problem with linear constants restriction, called here "unification with simple variable restriction". It is shown that for logical systems enjoying an appropriate algebraic semantics and a finite approximation of left uniform interpolation, this unification with simple variable restriction can be reduced to standard unification. As a corollary, we obtain the decidability of admissibility of $Π_{2}$-rules for many logical systems.

math.LO↗

arXiv2023

Polyatomic Logics and Generalised Blok-Esakia Theory

This paper presents a novel concept of a Polyatomic Logic and initiates its systematic study. This approach, inspired by Inquisitive semantics, is obtained by taking a variant of a given logic, obtained by looking at the fragment covered by a selector term. We introduce an algebraic semantics for these logics and prove algebraic completeness. These logics are then related to translations, through the introduction of a number of classes of translations involving selector terms, which are noted to be ubiquitous in algebraic logic. In this setting, we also introduce a generalised Blok-Esakia theory which can be developed for special classes of translations. We conclude by showing some systematic connections between the theory of Polyatomic Logics and the general Blok-Esakia theory for a wide class of interesting translations.

math.LO↗