arXiv subjects

Raheleh Jalali

Publications and source records attributed to Raheleh Jalali.

14 recordsLinked to original sources

arXiv2026

Proof Complexity of Linear Logics

Proving proof-size lower bounds for $\mathbf{LK}$, the sequent calculus for classical propositional logic, remains one of the major open problems in proof complexity. We shed new light on this challenge by isolating the power of structural rules and showing that their combination is dramatically stronger than any individual structural rule alone, even in the presence of the controlled structural rules provided by linear exponentials. It is easy to see that $\mathbf{LK}$ without the weakening rule is significantly weaker than $\mathbf{LK}$ with respect to proof complexity. It therefore remains to study the impact of eliminating contraction and cut. Working over the Full Lambek calculus with exchange, $\mathbf{FL_e}$, as a base system, we begin with the role of contraction. We construct families of $\mathbf{FL_e}$-provable formulas that require exponential-size proofs in affine linear logic $\mathbf{LLW}$, yet admit polynomial-size proofs once contraction is restored. This yields exponential proof-size lower bounds for $\mathbf{FL_e}$-provable formulas in $\mathbf{LLW}$, and consequently in $\mathbf{MALL}$, $\mathbf{MALL_w}$, and full classical linear logic $\mathbf{LL}$. We then investigate the role of cut. We exhibit sequents with polynomial-size $\mathbf{FL_e}$-proofs that nevertheless require exponential-size proofs in cut-free $\mathbf{LK}$. This shows that the cut rule alone provides an exponential speed-up over the combination of weakening and contraction. As a consequence, we obtain exponential separations between several linear calculi and their cut-free counterparts.

cs.LO↗

arXiv2026

Interpolation in Proof Theory

This chapter provides a comprehensive overview of proof-theoretic methods for establishing interpolation properties across a range of logics, including classical, intuitionistic, modal, and substructural logics. Central to the discussion are two foundational techniques: Maehara's method for Craig interpolation and Pitts' method for uniform interpolation. The chapter demonstrates how these methods lead to results on the existence of well-behaved proof systems in the contemporary framework of universal proof theory and how they provide a road map for constructing interpolation proofs using modern proof formalisms. The emphasis of the chapter is on constructive, modular, and syntax-driven techniques that illuminate deeper connections between interpolation properties and proof systems.

cs.LO↗

arXiv2026

Feasibility of Primality in Bounded Arithmetic

We prove the correctness of the AKS algorithm \cite{AKS} within the bounded arithmetic theory $T^{count}_2$ or, equivalently, the first-order consequences of the theory $VTC^0$ expanded by the smash function, which we denote by $VTC^0_2$. Our approach initially demonstrates the correctness within the theory $S^1_2 + iWPHP$ augmented by two algebraic axioms and then show that they are provable in $VTC^0_2$. The two axioms are: a generalized version of Fermat's Little Theorem and an axiom adding a new function symbol which injectively maps roots of polynomials over a definable finite field to numbers bounded by the degree of the given polynomial. To obtain our main result, we also give new formalizations of parts of number theory and algebra: $\bullet$ In $PV_1$: We formalize Legendre's Formula on the prime factorization of $n!$, key properties of the Combinatorial Number System and the existence of cyclotomic polynomials over the finite fields $\mathbb{Z}/p$. $\bullet$ In $S^1_2$: We prove the inequality $lcm(1,\dots, 2n) \geq 2^n$. $\bullet$ In $VTC^0$: We verify the correctness of the Kung--Sieveking algorithm for polynomial division.

math.LO↗

arXiv2025

Universal Proof Theory, TACL 2022 Lecture Notes

These lecture notes survey the emerging area of Universal Proof Theory, which investigates general questions about the existence, equivalence, and characterization of good proof systems for broad classes of logics. In particular, the notes concentrate on the existence problem: for which logics do there exist proof systems satisfying desirable meta-properties (e.g. cut elimination, analyticity, termination)? After a brief historical and conceptual introduction, we survey different flavours of proof theory (Hilbert systems, natural deduction, sequent calculi) in the context of classical, intuitionistic, modal, and substructural logics. We then develop a general method for obtaining positive and negative existence results, based on interpolation and uniform interpolation techniques, and apply it to a range of logics (intermediate, modal, non-normal, conditional, and substructural). We also discuss variations of the method. As these are lecture notes, proofs are often sketched or omitted, with pointers to papers containing the full proofs. The survey thus aims to chart the scope and challenges of Universal Proof Theory for future work.

math.LO↗

arXiv2025

Universal Proof Theory: Semi-analytic Rules and Uniform Interpolation

In \cite{Craig}, we introduced a syntactically defined and highly general class of calculi known as \emph{semi-analytic}. We then demonstrated that any sufficiently strong (modal) substructural logic with a semi-analytic calculus must satisfy the Craig interpolation property. In this paper, we show that if the calculus is also terminating in a certain formal sense, then its logic has the Uniform Interpolation Property (UIP). This result has significant applications. On the positive side, it provides a uniform and modular method for proving UIP for various logics, including $\mathsf{FL_e}$, $\mathsf{FL_{ew}}$, $\mathsf{CFL_e}$, $\mathsf{CFL_{ew}}$, and their $K$, $D$, and $T$-type modal extensions, as well as $\mathsf{CPC}$, $\mathsf{K}$, and $\mathsf{KD}$. However, its more striking consequence lies in the negative direction. It extends the negative results of \cite{Craig} to logics with CIP but without UIP. In particular, it shows that the modal logics $\mathsf{K4}$ and $\mathsf{S4}$ do not have a terminating semi-analytic calculus. \textbf{keywords:} Uniform interpolation, Sequent calculi, Substructural logics, Modal logics, Subexponential modalities

cs.LO↗

arXiv2025

Skolemization In Intermediate Logics

Skolemization, with Herbrand's theorem, underpins automated theorem proving and various transformations in computer science and mathematics. Skolemization removes strong quantifiers by introducing new function symbols, enabling efficient proof search algorithms. We characterize intermediate first-order logics that admit standard (and Andrews) Skolemization. These are the logics that allow classical quantifier shift principles. For some logics not in this category, innovative forms of Skolem functions are developed that allow Skolemization. Moreover, we analyze predicate intuitionistic logic with quantifier shift axioms and demonstrate its Kripke frame-incompleteness. These findings may foster resolution-based theorem provers for non-classical logics. This article is part of a larger project investigating Skolemization in non-classical logics.

cs.LO↗

arXiv2025

On the Completeness of Interpolation Algorithms

Craig interpolation is a fundamental property of classical and non-classic logics with a plethora of applications from philosophical logic to computer-aided verification. The question of which interpolants can be obtained from an interpolation algorithm is of profound importance. Motivated by this question, we initiate the study of completeness properties of interpolation algorithms. An interpolation algorithm $\mathcal{I}$ is \emph{complete} if, for every semantically possible interpolant $C$ of an implication $A \to B$, there is a proof $P$ of $A \to B$ such that $C$ is logically equivalent to $\mathcal{I}(P)$. We establish incompleteness and different kinds of completeness results for several standard algorithms for resolution and the sequent calculus for propositional, modal, and first-order logic.

cs.LO↗

arXiv2024

Universal Proof Theory: Semi-analytic Rules and Craig Interpolation

We provide a general and syntactically-defined family of sequent calculi, called \emph{semi-analytic}, to formalize the informal notion of a "nice" sequent calculus. We show that any sufficiently strong (multimodal) substructural logic with a semi-analytic sequent calculus enjoys the Craig Interpolation Property, CIP. As a positive application, our theorem provides a uniform and modular method to prove the CIP for several multimodal substructural logics, including many fragments and variants of linear logic. More interestingly, on the negative side, it employs the lack of the CIP in almost all substructural, superintuitionistic and modal logics to provide a formal proof for the well-known intuition that almost all logics do not have a "nice" sequent calculus. More precisely, we show that many substructural logics including $\mathsf{UL^-}$, $\mathsf{MTL}$, $\mathsf{R}$, $\mathsf{L}_n$ (for $n \geq 3$), $\mathsf{G}_n$ (for $n \geq 4$), and almost all extensions of $\mathsf{IMTL}$, $\mathsf{L}$, $\mathsf{BL}$, $\mathsf{RM^e}$, $\mathsf{IPC}$, $\mathsf{S4}$, and $\mathsf{Grz}$, (except for at most 1, 1, 3, 8, 7, 37, and 6 of them, respectively) do not have a semi-analytic calculus. Keywords. Craig interpolation, sequent calculi, substructural logics, linear logics, subexponential modalities

cs.LO↗

arXiv2023

Extensions of K5: Proof Theory and Uniform Lyndon Interpolation

We introduce a Gentzen-style framework, called layered sequent calculi, for modal logic K5 and its extensions KD5, K45, KD45, KB5, and S5 with the goal to investigate the uniform Lyndon interpolation property (ULIP), which implies both the uniform interpolation property and the Lyndon interpolation property. We obtain complexity-optimal decision procedures for all logics and present a constructive proof of the ULIP for K5, which to the best of our knowledge, is the first such syntactic proof. To prove that the interpolant is correct, we use model-theoretic methods, especially bisimulation modulo literals.

cs.LO↗

arXiv2022

Universal Proof Theory: Feasible Admissibility in Intuitionistic Modal Logics

In this paper, we introduce a general family of sequent-style calculi over the modal language and its fragments to capture the essence of all constructively acceptable systems. Calling these calculi \emph{constructive}, we show that any strong enough constructive sequent calculus, satisfying a mild technical condition, feasibly admits all Visser's rules, i.e., there is a polynomial time algorithm that reads a proof of the premise of a Visser's rule and provides a proof for its conclusion. As a positive application, we show the feasible admissibility of Visser's rules in several sequent calculi for intuitionistic modal logics, including $\mathsf{CK}$, $\mathsf{IK}$ and their extensions by the modal axioms $T$, $B$, $4$, $5$, the modal axioms of bounded width and depth and the propositional lax logic. On the negative side, we show that if a strong enough intuitionistic modal logic (satisfying a mild technical condition) does not admit at least one of Visser's rules, then it cannot have a constructive sequent calculus. Consequently, no intermediate logic other than $\mathsf{IPC}$ has a constructive sequent calculus.

math.LO↗

arXiv2022

Uniform Lyndon Interpolation for Basic Non-normal Modal and Conditional Logics

In this paper, a proof-theoretic method to prove uniform Lyndon interpolation for non-normal modal and conditional logics is introduced and applied to show that the logics $\mathsf{E}$, $\mathsf{M}$, $\mathsf{EN}$, $\mathsf{MN}$, $\mathsf{MC}$, $\mathsf{K}$, and their conditional versions, $\mathsf{CE}$, $\mathsf{CM}$, $\mathsf{CEN}$, $\mathsf{CMN}$, $\mathsf{CMC}$, $\mathsf{CK}$, in addition to $\mathsf{CKID}$ have that property. In particular, it implies that these logics have uniform interpolation. Although for some of them the latter is known, the fact that they have uniform Lyndon interpolation is new. Also, the proof-theoretic proofs of these facts are new, as well as the constructive way to explicitly compute the interpolants that they provide. On the negative side, it is shown that the logics $\mathsf{CKCEM}$ and $\mathsf{CKCEMID}$ enjoy uniform interpolation but not uniform Lyndon interpolation. Moreover, it is proved that the non-normal modal logics $\mathsf{EC}$ and $\mathsf{ECN}$ and their conditional versions, $\mathsf{CEC}$ and $\mathsf{CECN}$, do not have Craig interpolation, and whence no uniform (Lyndon) interpolation.

math.LO↗

arXiv2022

Uniform Lyndon interpolation for intuitionistic monotone modal logic

In this paper we show that the intuitionistic monotone modal logic $\mathsf{iM}$ has the uniform Lyndon interpolation property (ULIP). The logic $\mathsf{iM}$ is a non-normal modal logic on an intuitionistic basis, and the property ULIP is a strengthening of interpolation in which the interpolant depends only on the premise or the conclusion of an implication, respecting the polarities of the propositional variables. Our method to prove ULIP yields explicit uniform interpolants and makes use of a terminating sequent calculus for $\mathsf{iM}$ that we have developed for this purpose. As far as we know, the results that $\mathsf{iM}$ has ULIP and a terminating sequent calculus are the first of their kind for an intuitionistic non-normal modal logic. However, rather than proving these particular results, our aim is to show the flexibility of the constructive proof-theoretic method that we use for proving ULIP. It has been developed over the last few years and has been applied to substructural, intermediate, classical (non-)normal modal and intuitionistic normal modal logics. In light of these results, intuitionistic non-normal modal logics seem a natural next class to try to apply the method to, and we take the first step in that direction in this paper.

math.LO↗

arXiv2021

Uniform interpolation via nested sequents and hypersequents

A modular proof-theoretic framework was recently developed to prove Craig interpolation for normal modal logics based on generalizations of sequent calculi (e.g., nested sequents, hypersequents, and labelled sequents). In this paper, we turn to uniform interpolation, which is stronger than Craig interpolation. We develop a constructive method for proving uniform interpolation via nested sequents and apply it to reprove the uniform interpolation property for normal modal logics $\mathsf{K}$, $\mathsf{D}$, and $\mathsf{T}$. We then use the know-how developed for nested sequents to apply the same method to hypersequents and obtain the first direct proof of uniform interpolation for $\mathsf{S5}$ via a cut-free sequent-like calculus. While our method is proof-theoretic, the definition of uniform interpolation for nested sequents and hypersequents also uses semantic notions, including bisimulation modulo an atomic proposition.

cs.LO↗

arXiv2020

Proof Complexity of Substructural Logics

In this paper, we investigate the proof complexity of a wide range of substructural systems. For any proof system $\mathbf{P}$ at least as strong as Full Lambek calculus, $\mathbf{FL}$, and polynomially simulated by the extended Frege system for some infinite branching super-intuitionistic logic, we present an exponential lower bound on the proof lengths. More precisely, we will provide a sequence of $\mathbf{P}$-provable formulas $\{A_n\}_{n=1}^{\infty}$ such that the length of the shortest $\mathbf{P}$-proof for $A_n$ is exponential in the length of $A_n$. The lower bound also extends to the number of proof-lines (proof-lengths) in any Frege system (extended Frege system) for a logic between $\mathsf{FL}$ and any infinite branching super-intuitionistic logic. We will also prove a similar result for the proof systems and logics extending Visser's basic propositional calculus $\mathbf{BPC}$ and its logic $\mathsf{BPC}$, respectively. Finally, in the classical substructural setting, we will establish an exponential lower bound on the number of proof-lines in any proof system polynomially simulated by the cut-free version of $\mathbf{CFL_{ew}}$.

math.LO↗