Publications: abstracts


Provability logic of the Alternative Set Theory

Master’s thesis, Faculty of Philosophy and Arts, Charles University, Prague, 2001, 44 pp. [PDF, PS] [BIB]

(No abstract available; you can read the introductory chapter on a separate page instead.)


Reflexe v neregulárních univerzech

Master’s thesis, Faculty of Mathematics and Physics, Charles University, Prague, 2001, 41 pp., in Czech. [PDF, PS] [BIB]

Hlavním účelem této práce je studium elementárních vnoření univerzální třídy do tranzitivní třídy (stručně nazývaných reflexe) v jisté neregulární teorii množin, kterou budeme ve shodě s [1] označovat jako univerzální teorii (UT). Axiom regularity, který v klasické teorii množin značně omezuje (mimo jiné) možnost konstruovat elementární vnoření množinového univerza, je v UT nahrazen tzv. axiomem superuniverzality, jenž naopak dovoluje sestrojit množství reflexí s rozmanitými vlastnostmi. Reflexe lze s výhodou využít zejména pro modelování prostředků nestandardní analýzy a obecnějších nestandardních principů, my se však zaměříme na obecný popis reflexí a možností jejich konstrukce.

Ústředním pojmem kapitoly 2 jsou tzv. minimální reflexe. V celé kapitole budeme pracovat výhradně v UT. V sekci 2.1 nejprve ukážeme, že studium vlastností minimálních reflexí má mnoho důsledků i pro neminimální reflexe, neboť každá reflexe v jistém smyslu obsahuje určitou minimální reflexi, zde nazývanou jádro. Část tohoto tvrzení dále zobecníme na třídy, které jsou modelem tzv. axiomu kolekce, což nám zpětně umožní ukázat, že nekonečné schéma formulí v definici reflexe lze konečně axiomatizovat, tedy nahradit jedinou formulí.

Sekce 2.2 se krátce zabývá reflexemi vedoucími do kotranzitivních tříd (tedy např. do celé univerzální třídy) — ukážeme, že takové reflexe jsou triviální, tedy že se takřka neliší od identické reflexe.

V sekci 2.3 popíšeme obecnou konstrukci, kterou lze získat všechny minimální reflexe. Ukážeme, že každá minimální reflexe je direktní limitou vhodného usměrněného systému ultramocnin univerzální třídy, a na druhou stranu (téměř) každá taková direktní limita určuje minimální reflexi. Zjistíme také, že určité speciální typy minimálních reflexí (jednoduché reflexe, polojednoduché reflexe a PP-reflexe) lze charakterizovat podmínkami na tvar příslušné direktní limity. Navíc uvidíme, že tyto typy minimálních reflexí jsou uzavřené na některé způsoby konstrukce reflexí (ultraprodukty, skládání, podreflexe, direktní limity).

Sekce 2.4 obsahuje dva příklady minimálních reflexí se zajímavými vlastnostmi, pokusíme se ukázat, že přinejmenším některé z výše zmíněných tříd minimálních reflexí spolu nesplývají.

V kapitole 3 reflexe opustíme a budeme se věnovat axiomu silného výběru, který postuluje existenci vzájemně jednoznačného zobrazení univerzální třídy na třídu všech ordinálních čísel. Pro klasickou teorii množin s axiomem regularity je známo, že axiom silného výběru konzervativně rozšiřuje obyčejný axiom výběru, jeho použitím tedy není možné dokázat pouze o množinách nic nového. Pro neregulární teorii množin však zmíněná konzervativita neplatí. Přesto se nám podaří popsat množinové důsledky axiomu silného výběru pomocí jednoduchého schematu axiomů a dokážeme konzervativitu axiomu silného výběru nad takto modifikovanou teorií množin. Protože UT axiom silného výběru obsahuje, obdržíme jako důsledek také popis fragmentu UT v základním jazyce teorie množin.

  1. Petr Pajas, Endomorfismy, invariantní třídy a nestandardní principy v neregulárním universu množin, diplomová práce, MFF UK, Praha 1999.

A note on Grzegorczyk’s logic

Mathematical Logic Quarterly 50 (2004), no. 3, pp. 295–296. [DOI] [PDF, PS] [BIB]

Grzegorczyk’s modal logic (Grz) corresponds to the class of upwards well-founded partially ordered Kripke frames, however all known proofs of this fact utilize some form of the Axiom of Choice; G. Boolos asked in [1], whether it is provable in plain ZF. We answer his question negatively: Grz corresponds (in ZF) to a class of frames, which does not provably coincide with upwards well-founded posets in ZF alone.

  1. George Boolos, The Logic of Provability, Cambridge University Press, 1993, p. 163.

Dual weak pigeonhole principle, Boolean complexity, and derandomization

Annals of Pure and Applied Logic 129 (2004), pp. 1–37. [DOI] [PDF, PS] [BIB]

We study the extension (introduced as BT in [2]) of the theory S21 by instances of the dual (onto) weak pigeonhole principle for p-time functions, dWPHP(PV)xx². We propose a natural framework for formalization of randomized algorithms in bounded arithmetic, and use it to provide a strengthening of Wilkie’s witnessing theorem for S21 + dWPHP(PV). We construct a propositional proof system WF (based on a reformulation of Extended Frege in terms of Boolean circuits), which captures the ∀Πb1-consequences of S21 + dWPHP(PV). We also show that WF p-simulates the Unstructured Extended Nullstellensatz proof system of [1].

We prove that dWPHP(PV) is (over S21) equivalent to a statement asserting the existence of a family of Boolean functions with exponential circuit complexity. Building on this result, we formalize the Nisan–Wigderson construction (derandomization of probabilistic p-time algorithms) in a conservative extension of S21 + dWPHP(PV).

  1. Samuel R. Buss, Russell Impagliazzo, Jan Krajíček, Pavel Pudlák, Alexander A. Razborov, and Jiří Sgall, Proof complexity in algebraic systems and bounded depth Frege systems with modular counting, Computational Complexity 6 (1997), no. 3, pp. 256–298.
  2. Jan Krajíček, On the weak pigeonhole principle, Fundamenta Mathematicae 170 (2001), pp. 123–140.

Subdirectly irreducible non-idempotent left symmetric left distributive groupoids

Emil Jeřábek, Tomáš Kepka, and David Stanovský
Discussiones Mathematicae – General Algebra and Applications 25 (2005), no. 2, pp. 235–257. [DOI] [PDF] [BIB]

We study groupoids satisfying the identities x·xy = y and x·yz = xy·xz. Particularly, we focus our attention at subdirectly irreducible ones, find a description and characterize small ones.


Fragment of nonstandard analysis with a finitary consistency proof

Emil Jeřábek and Michal Rössler
Bulletin of Symbolic Logic 13 (2007), no. 1, pp. 54–70. [DOI] [PDF] [BIB]

We introduce a nonstandard arithmetic NQA based on the theory developed by R. Chuaqui and P. Suppes in [1] (we will denote it by NQA+), with a weakened external open minimization schema. A finitary consistency proof for NQA formalizable in PRA is presented. We also show interesting facts about the strength of the theories NQA and NQA+; NQA is mutually interpretable with IΔ0 + EXP, and on the other hand, NQA+ interprets the theories IΣ1 and WKL0.

  1. Rolando Chuaqui and Patrick Suppes, Free-variable axiomatic foundations of infinitesimal analysis: A fragment with finitary consistency proof, Journal of Symbolic Logic 60 (1995), no. 1, pp. 122–159.

Weak pigeonhole principle, and randomized computation

Ph.D. thesis, Faculty of Mathematics and Physics, Charles University, Prague, 2005, 116 pp. [browsable PDF with hyperlinks, printable PS] [BIB]

We study the extension of the theory S21 by instances of the dual (onto) weak pigeonhole principle for p-time functions, dWPHP(PV)xx². We propose a natural framework for formalization of randomized algorithms in bounded arithmetic, and use it to provide a strengthening of Wilkie’s witnessing theorem for S21 + dWPHP(PV).

Then we show that dWPHP(PV) is (over S21) equivalent to a statement asserting the existence of a family of Boolean functions with exponential circuit complexity. Building on this result, we formalize the Nisan–Wigderson construction (conditional derandomization of probabilistic p-time algorithms) in a conservative extension of S21 + dWPHP(PV). We also develop in S21 the algebraic machinery needed for implicit list-decoding of Reed–Muller error-correcting codes (including some results on a modification of Soltys’ theory LAP), and use it to formalize the Impagliazzo–Wigderson strengthening of the Nisan–Wigderson theorem.

We construct a propositional proof system WF (based on a reformulation of Extended Frege in terms of Boolean circuits), which captures the ∀Πb1-consequences of S21 + dWPHP(PV). As an application, we show that WF and G2 p-simulate the Unstructured Extended Nullstellensatz proof system.

We also consider two theories which have explicit counting facilities in their language. The first one is the Impagliazzo–Kapron logic; we propose a modification of the theory, and prove a generalization of the Impagliazzo–Kapron soundness theorem to ∀∃-consequences of the theory. The second one is a feasible theory of approximate counting, formulated in a variant of Kleene’s 3-valued logic. We introduce the theory, and prove a witnessing theorem for its existential consequences.


Admissible rules of modal logics

Journal of Logic and Computation 15 (2005), no. 4, pp. 411–431. [DOI] [PDF, PS] [BIB]

We construct explicit bases of admissible rules for a representative class of normal modal logics (including the systems K4, GL, S4, Grz, and GL.3), by extending the methods of S. Ghilardi and R. Iemhoff. We also investigate the notion of admissible multiple conclusion rules.


Complexity of admissible rules

Archive for Mathematical Logic 46 (2007), no. 2, pp. 73–92. [DOI] [PDF, PS] [BIB]

We investigate the computational complexity of deciding whether a given inference rule is admissible for some modal and superintuitionistic logics. We state a broad condition under which the admissibility problem is coNEXP-hard. We also show that admissibility in several well-known systems (including GLS4, and IPC) is in coNE, thus obtaining a sharp complexity estimate for admissibility in these systems.


Frege systems for extensible modal logics

Annals of Pure and Applied Logic 142 (2006), pp. 366–379. [DOI] [PDF, PS] [BIB]

By a well-known result of Cook and Reckhow [1,4], all Frege systems for the Classical Propositional Calculus (CPC) are polynomially equivalent. Mints and Kojevnikov [3] have recently shown p-equivalence of Frege systems for the Intuitionistic Propositional Calculus (IPC) in the standard language, building on a description of admissible rules of IPC by Iemhoff [2]. We prove a similar result for an infinite family of normal modal logics, including K4, GL, S4, and S4Grz.

  1. Stephen A. Cook and Robert A. Reckhow, The relative efficiency of propositional proof systems, Journal of Symbolic Logic 44 (1979), no. 1, pp. 36–50.
  2. Rosalie Iemhoff, On the admissible rules of intuitionistic propositional logic, Journal of Symbolic Logic 66 (2001), no. 1, pp. 281–294.
  3. Grigori Mints and Arist Kojevnikov, Intuitionistic Frege systems are polynomially equivalent, Zapiski Nauchnyh Seminarov POMI 316 (2004), pp. 129–146.
  4. Robert A. Reckhow, On the lengths of proofs in the propositional calculus, Ph.D. thesis, Department of Computer Science, University of Toronto, 1976.

Approximate counting in bounded arithmetic

Journal of Symbolic Logic 72 (2007), no. 3, pp. 959–993. [DOI] [PDF, PS] [BIB]

We develop approximate counting of sets definable by Boolean circuits in bounded arithmetic using the dual weak pigeonhole principle (dWPHP(PV)), as a generalization of results from [1]. We discuss applications to formalization of randomized complexity classes (such as BPP, APP, MAAM) in PV1 + dWPHP(PV).

  1. Emil Jeřábek, Dual weak pigeonhole principle, Boolean complexity, and derandomization, Annals of Pure and Applied Logic 129 (2004), pp. 1–37.

The strength of sharply bounded induction

Mathematical Logic Quarterly 52 (2006), no. 6, pp. 613–624. [DOI] [PDF, PS] [BIB]

We prove that the sharply bounded arithmetic T20 in a language containing the function symbol x / 2y (often denoted by MSP) is equivalent to PV1.


On independence of variants of the weak pigeonhole principle

Journal of Logic and Computation 17 (2007), no. 3, pp. 587–604. [DOI] [PDF, PS] [BIB]

The principle sPHPab(PV(α)) states that no oracle circuit can compute a surjection of a onto b. We show that sPHPρ(a)Ρ(a)(PV(α)) is independent of PV1(α) + sPHPπ(a)Π(a)(PV(α)) for various choices of the parameters π, Π, ρΡ. We also improve the known separation of iWPHP(PV) from S21 + sWPHP(PV) under cryptographic assumptions.


Independent bases of admissible rules

Logic Journal of the IGPL 16 (2008), no. 3, pp. 249–267. [DOI] [PDF, PS] [BIB]

We show that IPC, K4, GL, and S4, as well as all logics inheriting their admissible rules, have independent bases of admissible rules.


Substitution Frege and extended Frege proof systems in non-classical logics

Annals of Pure and Applied Logic 159 (2009), no. 1–2, pp. 1–48. [DOI] [PDF, PS] [BIB]

We investigate the substitution Frege (SF) proof system and its relationship to extended Frege (EF) in the context of modal and superintuitionistic (si) propositional logics. We show that EF is p-equivalent to tree-like SF, and we develop a “normal form” for SF-proofs. We establish connections between SF for a logic L, and EF for certain bimodal expansions of L.

We then turn attention to specific families of modal and si logics. We prove p-equivalence of EF and SF for all extensions of KB, all tabular logics, all logics of finite depth and width, and typical examples of logics of finite width and infinite depth. In most cases, we actually show an equivalence with the usual EF system for classical logic with respect to a naturally defined translation.

On the other hand, we establish exponential speed-up of SF over EF for all modal and si logics of infinite branching, extending recent lower bounds by P. Hrubeš. We develop a model-theoretical characterization of maximal logics of infinite branching to prove this result.


Approximate counting by hashing in bounded arithmetic

Journal of Symbolic Logic 74 (2009), no. 3, pp. 829–860. [DOI] [PDF, PS] [BIB]

We show how to formalize approximate counting via hash functions in subsystems of bounded arithmetic, using variants of the weak pigeonhole principle. We discuss several applications, including a proof of the tournament principle, and an improvement on the known relationship of the collapse of the bounded arithmetic hierarchy to the collapse of the polynomial-time hierarchy.


Proof complexity of the cut-free calculus of structures

Journal of Logic and Computation 19 (2009), no. 2, pp. 323–339. [DOI] [PDF, PS] [BIB]

We investigate the proof complexity of analytic subsystems of the deep inference proof system SKSg (the calculus of structures). Exploiting the fact that the cut rule (i) of SKSg corresponds to the ¬-left rule in the sequent calculus, we establish that the “analytic” system KSg + c has essentially the same complexity as the monotone Gentzen calculus MLK. In particular, KSg + c quasipolynomially simulates SKSg, and admits polynomial-size proofs of some variants of the pigeonhole principle.


Canonical rules

Journal of Symbolic Logic 74 (2009), no. 4, pp. 1171–1205. [DOI] [PDF, PS] [BIB]

We develop canonical rules capable of axiomatizing all systems of multiple-conclusion rules over K4 or IPC, by extension of the method of canonical formulas by Zakharyaschev [1]. We use the framework to give an alternative proof of the known analysis of admissible rules in basic transitive logics, which additionally yields the following dichotomy: any canonical rule is either admissible in the logic, or it is equivalent to an assumption-free rule. Other applications of canonical rules include a generalization of the Blok–Esakia theorem and the theory of modal companions to systems of multiple-conclusion rules or (finitary structural global) consequence relations, and a characterization of splittings in the lattices of consequence relations over monomodal or superintuitionistic logics with the finite model property.

  1. Michael Zakharyaschev, Canonical formulas for K4. Part I: Basic results, Journal of Symbolic Logic 57 (1992), no. 4, pp. 1377–1402.

Abelian groups and quadratic residues in weak arithmetic

Mathematical Logic Quarterly 56 (2010), no. 3, pp. 262–278. [DOI] [PDF, PS] [BIB]

We investigate the provability of some properties of abelian groups and quadratic residues in variants of bounded arithmetic. Specifically, we show that the structure theorem for finite abelian groups is provable in S22 + iWPHP1b), and use it to derive Fermat’s little theorem and Euler’s criterion for the Legendre symbol in S22 + iWPHP(PV) extended by the pigeonhole principle PHP(PV). We prove the quadratic reciprocity theorem (including the supplementary laws) in the arithmetic theories T20 + Count2(PV) and IΔ0 + Count20) with modulo-2 counting principles.


On theories of bounded arithmetic for NC1

Annals of Pure and Applied Logic 162 (2011), no. 4, pp. 322–340. [DOI] [PDF, PS] [BIB]

We develop an arithmetical theory VNC1* and its variant VNC1*, corresponding to “slightly nonuniform” NC1. Our theories sit between VNC1 and VL, and allow evaluation of log-depth bounded fan-in circuits under limited conditions. Propositional translations of Σ0B(LVNC1*)-formulas provable in VNC1* admit L-uniform polynomial-size Frege proofs.


A sorting network in bounded arithmetic

Annals of Pure and Applied Logic 162 (2011), no. 4, pp. 341–355. [DOI] [PDF, PS] [BIB]

We formalize the construction of Paterson’s variant of the Ajtai–Komlós–Szemerédi sorting network of logarithmic depth in the bounded arithmetical theory VNC1* (an extension of VNC1), under the assumption of existence of suitable expander graphs. We derive a conditional p-simulation of the propositional sequent calculus in the monotone sequent calculus MLK.


Admissible rules of Łukasiewicz logic

Journal of Logic and Computation 20 (2010), no. 2, pp. 425–447. [DOI] [PDF, PS] [BIB]

We investigate admissible rules of Łukasiewicz multi-valued propositional logic. We show that admissibility of multiple-conclusion rules in Łukasiewicz logic, as well as validity of universal sentences in free MV-algebras, is decidable (in PSPACE).


Bases of admissible rules of Łukasiewicz logic

Journal of Logic and Computation 20 (2010), no. 6, pp. 1149–1163. [DOI] [PDF, PS] [BIB]

We construct explicit bases of single-conclusion and multiple-conclusion admissible rules of propositional Łukasiewicz logic, and we prove that every formula has an admissibly saturated approximation. We also show that Łukasiewicz logic has no finite basis of admissible rules.


Proofs with monotone cuts

Mathematical Logic Quarterly 58 (2012), no. 3, pp. 177–187. [DOI] [PDF, PS] [BIB]

Atserias, Galesi, and Pudlák [1] have shown that the monotone sequent calculus MLK quasipolynomially simulates proofs of monotone sequents in the full sequent calculus LK (or equivalently, in Frege systems). We generalize the simulation to the fragment MCLK of LK which can prove arbitrary sequents, but restricts cut-formulas to be monotone. We also show that MLK as a refutation system for CNFs quasipolynomially simulates LK.

  1. Albert Atserias, Nicola Galesi, and Pavel Pudlák, Monotone simulations of non-monotone proofs, Journal of Computer and System Sciences 65 (2002), no. 4, pp. 626–638.

Simulating non-prenex cuts in quantified propositional calculus

Emil Jeřábek and Phuong Nguyen
Mathematical Logic Quarterly 57 (2011), no. 5, pp. 524–532. [DOI] [PDF, PS] [BIB]

We show that the quantified propositional proof systems Gi are polynomially equivalent to their restricted versions that require all cut formulas to be prenex Σqi (or prenex Πqi). Previously this was known only for the treelike systems Gi*.


Real closures of models of weak arithmetic

Emil Jeřábek and Leszek Aleksander Kołodziejczyk
Archive for Mathematical Logic 52 (2013), no. 1–2, pp. 143–157. [DOI] [PDF, PS] [BIB]

D’Aquino et al. [1] have recently shown that every real-closed field with an integer part satisfying the arithmetic theory IΣ4 is recursively saturated, and that this theorem fails if IΣ4 is replaced by IΔ0. We prove that the theorem holds if IΣ4 is replaced by weak subtheories of Buss’ bounded arithmetic: PV or Σb1-IND|x|k. It also holds for IΔ0 (and even its subtheory IE2) under a rather mild assumption on cofinality. On the other hand, it fails for the extension of IOpen by an axiom expressing the Bézout property, even under the same assumption on cofinality.

  1. Paola D’Aquino, Julia F. Knight, and Sergei Starchenko, Real closed fields and models of Peano arithmetic, Journal of Symbolic Logic 75 (2010), no. 1, pp. 1–11.

The ubiquity of conservative translations

Review of Symbolic Logic 5 (2012), no. 4, pp. 666–678. [DOI, arXiv] [PDF, PS] [BIB]

We study the notion of conservative translation between logics introduced by Feitosa and D’Ottaviano [1]. We show that classical propositional logic (CPC) is universal in the sense that every finitary consequence relation over a countable set of formulas can be conservatively translated into CPC. The translation is computable if the consequence relation is decidable. More generally, we show that one can take instead of CPC a broad class of logics (extensions of a certain fragment of full Lambek calculus FL) including most nonclassical logics studied in the literature, hence in a sense, (almost) any two reasonable deductive systems can be conservatively translated into each other. We also provide some counterexamples, in particular the paraconsistent logic LP is not universal.

  1. Hércules A. Feitosa and Itala M. Loffredo D’Ottaviano, Conservative translations, Annals of Pure and Applied Logic 108 (2001), pp. 205–227.

Blending margins: The modal logic K has nullary unification type

Journal of Logic and Computation 25 (2015), no. 5, pp. 1231–1240. [DOI, arXiv] [PDF, PS] [BIB]

We investigate properties of the formula p → □p in the basic modal logic K. We show that K satisfies an infinitary weaker variant of the rule of margins φ → □φ / φ, ¬φ, and as a consequence, we obtain various negative results about admissibility and unification in K. We describe a complete set of unifiers (i.e., substitutions making the formula provable) of p → □p, and use it to establish that K has the worst possible unification type: nullary. In well-behaved transitive modal logics, admissibility and unification can be analyzed in terms of projective formulas, introduced by Ghilardi; in particular, projective formulas coincide for these logics with form ulas that are admissibly saturated (i.e., derive all their multiple-conclusion admissible consequences) or exact (i.e., axiomatize a theory of a substitution). In contrast, we show that in K, the formula p → □p is admissibly saturated, but neither projective nor exact. All our results for K also apply to the basic description logic ALC.


The complexity of admissible rules of Łukasiewicz logic

Journal of Logic and Computation 23 (2013), no. 3, pp. 693–705. [DOI, arXiv] [PDF, PS] [BIB]

We investigate the computational complexity of admissibility of inference rules in infinite-valued Łukasiewicz propositional logic (Ł). It was shown in [1] that admissibility in Ł is checkable in PSPACE. We establish that this result is optimal, i.e., admissible rules of Ł are PSPACE-complete. In contrast, derivable rules of Ł are known to be coNP-complete.

  1. Emil Jeřábek, Admissible rules of Łukasiewicz logic, Journal of Logic and Computation 20 (2010), no. 2, pp. 425–447.

Root finding with threshold circuits

Theoretical Computer Science, Theoretical Computer Science 462 (2012), pp. 59–69. [DOI, arXiv] [PDF, PS] [BIB]

We show that for any constant d, complex roots of degree d univariate rational (or Gaussian rational) polynomials—given by a list of coefficients in binary—can be computed to a given accuracy by a uniform TC0 algorithm (a uniform family of constant-depth polynomial-size threshold circuits). The basic idea is to compute the inverse function of the polynomial by a power series. We also discuss an application to the theory VTC0 of bounded arithmetic.


Sequence encoding without induction

Mathematical Logic Quarterly 58 (2012), no. 3, pp. 244–248. [DOI, arXiv] [PDF, PS] [BIB]

We show that the universally axiomatized, induction-free theory PA is a sequential theory in the sense of Pudlák [1], in contrast to the closely related Robinson’s arithmetic.

  1. Pavel Pudlák, Cuts, consistency statements and interpretations, Journal of Symbolic Logic 50 (1985), no. 2, pp. 423–441.

Integer factoring and modular square roots

Journal of Computer and System Sciences 82 (2016), no. 2, pp. 380–394. [DOI, arXiv] [PDF, PS] [BIB]

Buresh-Oppenheim proved that the NP search problem to find nontrivial factors of integers of a special form belongs to Papadimitriou’s class PPA, and is probabilistically reducible to a problem in PPP. In this paper, we use ideas from bounded arithmetic to extend these results to arbitrary integers. We show that general integer factoring is reducible in randomized polynomial time to a PPA problem and to the problem WeakPigeon ∈ PPP. Both reductions can be derandomized under the assumption of the generalized Riemann hypothesis. We also show (unconditionally) that PPA contains some related problems, such as square root computation modulo n, and finding quadratic nonresidues modulo n.


Rules with parameters in modal logic I

Annals of Pure and Applied Logic 166 (2015), no. 9, pp. 881–933. [DOI, arXiv] [PDF, PS] [BIB]

We study admissibility of inference rules and unification with parameters in transitive modal logics (extensions of K4), in particular we generalize various results on parameter-free admissibility and unification to the setting with parameters.

Specifically, we give a characterization of projective formulas generalizing Ghilardi’s characterization in the parameter-free case, leading to new proofs of Rybakov’s results that admissibility with parameters is decidable and unification is finitary for logics satisfying suitable frame extension properties (called cluster-extensible logics in this paper). We construct explicit bases of admissible rules with parameters for cluster-extensible logics, and give their semantic description. We show that in the case of finitely many parameters, these logics have independent bases of admissible rules, and determine which logics have finite bases.

As a sideline, we show that cluster-extensible logics have various nice properties: in particular, they are finitely axiomatizable, and have an exponential-size model property. We also give a rather general characterization of logics with directed (filtering) unification.

In the sequel, we will use the same machinery to investigate the computational complexity of admissibility and unification with parameters in cluster-extensible logics, and we will adapt the results to logics with unique top cluster (e.g., S4.2) and superintuitionistic logics.


Cluster expansion and the boxdot conjecture

Mathematical Logic Quarterly 62 (2016), no. 6, pp. 608–614. [DOI, arXiv] [PDF, PS] [BIB]

The boxdot conjecture asserts that every normal modal logic that faithfully interprets T by the well-known boxdot translation is in fact included in T. We confirm that the conjecture is true. More generally, we present a simple semantic condition on modal logics L0 which ensures that the largest logic where L0 embeds faithfully by the boxdot translation is L0 itself. In particular, this natural generalization of the boxdot conjecture holds for S4, S5, and KTB in place of T.


The foundation axiom and elementary self-embeddings of the universe

Ali Sadegh Daghighi, Mohammad Golshani, Joel David Hamkins, and Emil Jeřábek
Infinity, Computability, and Metamathematics: Festschrift celebrating the 60th birthdays of Peter Koepke and Philip Welch (S. Geschke, B. Löwe, and P. Schlicht, eds.), College Publications, London, 2014, pp. 89–112. [arXiv] [PDF, PS] [BIB]

We consider the role of the foundation axiom and various anti-foundation axioms in connection with the nature and existence of elementary self-embeddings of the set-theoretic universe.


Open induction in a bounded arithmetic for TC0

Archive for Mathematical Logic 54 (2015), no. 3–4, pp. 359–394. [DOI, arXiv] [PDF, PS] [BIB]

The elementary arithmetic operations +,⋅,≤ on integers are well-known to be computable in the weak complexity class TC0, and it is a basic question what properties of these operations can be proved using only TC0-computable objects, i.e., in a theory of bounded arithmetic corresponding to TC0. We will show that the theory VTC0 extended with an axiom postulating the totality of iterated multiplication (which is computable in TC0) proves induction for quantifier-free formulas in the language ⟨+,⋅,≤⟩ (IOpen), and more generally, minimization for Σb0 formulas in the language of Buss’s S2.


A note on the substructural hierarchy

Mathematical Logic Quarterly 62 (2016), no. 1–2, pp. 102–110. [DOI, arXiv] [PDF, PS] [BIB]

We prove that all axiomatic extensions of the full Lambek calculus with exchange can be axiomatized by formulas on the N3 level of the substructural hierarchy.


Proof complexity of intuitionistic implicational formulas

Annals of Pure and Applied Logic 168 (2017), no. 1, pp. 150–190. [DOI, arXiv] [PDF, PS] [BIB]

We study implicational formulas in the context of proof complexity of intuitionistic propositional logic (IPC). On the one hand, we give an efficient transformation of tautologies to implicational tautologies that preserves the lengths of intuitionistic extended Frege (EF) or substitution Frege (SF) proofs up to a polynomial. On the other hand, EF proofs in the implicational fragment of IPC polynomially simulate full intuitionistic logic for implicational tautologies. The results also apply to other fragments of other superintuitionistic logics under certain conditions.

In particular, the exponential lower bounds on the length of intuitionistic EF proofs by Hrubeš [1], generalized to exponential separation between EF and SF systems in superintuitionistic logics of unbounded branching by Jeřábek [2], can be realized by implicational tautologies.

  1. Pavel Hrubeš, A lower bound for intuitionistic logic, Annals of Pure and Applied Logic 146 (2007), no. 1, pp. 72–90.
  2. Emil Jeřábek, Substitution Frege and extended Frege proof systems in non-classical logics, Annals of Pure and Applied Logic 159 (2009), no. 1–2, pp. 1–48.

Division by zero

Archive for Mathematical Logic 55 (2016), no. 7, pp. 997–1013. [DOI, arXiv] [PDF, PS] [BIB]

For any sufficiently strong theory of arithmetic, the set of Diophantine equations provably unsolvable in the theory is algorithmically undecidable, as a consequence of the MRDP theorem. In contrast, we show decidability of Diophantine equations provably unsolvable in Robinson’s arithmetic Q. The argument hinges on an analysis of a particular class of equations, hitherto unexplored in Diophantine literature. We also axiomatize the universal fragment of Q in the process.


Galois connection for multiple-output operations

Algebra Universalis 79 (2018), article no. 17, 37 pp. [DOI, arXiv] [PDF, PS] [BIB]

It is a classical result from universal algebra that the notions of polymorphisms and invariants provide a Galois connection between suitably closed classes (clones) of finitary operations f: BnB, and classes (coclones) of relations rBk. We will present a generalization of this duality to classes of (multi-valued, partial) functions f: BnBm, employing invariants valued in partially ordered monoids instead of relations. In particular, our set-up encompasses the case of permutations f: BnBn, motivated by problems in reversible computing.


Recursive functions and existentially closed structures

Journal of Mathematical Logic 20 (2020), no. 1, article no. 2050002, 52 pp. [DOI, arXiv] [PDF, PS] [BIB]

The purpose of this paper is to clarify the relationship between various conditions implying essential undecidability: our main result is that there exists a theory T in which all partially recursive functions are representable, yet T does not interpret Robinson’s theory R. To this end, we borrow tools from model theory—specifically, we investigate model-theoretic properties of the model completion of the empty theory in a language with function symbols. We obtain a certain characterization of ∃∀ theories interpretable in existential theories in the process.


Rigid models of Presburger arithmetic

Mathematical Logic Quarterly 65 (2019), no. 1, pp. 108–115. [DOI, arXiv] [PDF, PS] [BIB]

We present a description of rigid models of Presburger arithmetic (i.e., -groups). In particular, we show that Presburger arithmetic has rigid models of all infinite cardinalities up to the continuum, but no larger.


Induction rules in bounded arithmetic

Archive for Mathematical Logic 59 (2020), no. 3, pp. 461–501. [DOI, arXiv] [PDF, PS] [BIB]

We study variants of Buss’s theories of bounded arithmetic axiomatized by induction schemes disallowing the use of parameters, and closely related induction inference rules. We put particular emphasis on Π̂bi induction schemes, which were so far neglected in the literature. We present inclusions and conservation results between the systems (including a witnessing theorem for T2i and S2i of a new form), results on numbers of instances of the axioms or rules, connections to reflection principles for quantified propositional calculi, and separations between the systems.


Rules with parameters in modal logic II

Annals of Pure and Applied Logic 171 (2020), no. 10, article no. 102829, 59 pp. [DOI, arXiv] [PDF, PS] [BIB]

We analyze the computational complexity of admissibility and unifiability with parameters in transitive modal logics. The class of cluster-extensible (clx) logics was introduced in the first part of this series of papers [1]. We completely classify the complexity of unifiability or inadmissibility in any clx logic as being complete for one of Σ2exp, NEXP, coNEXP, PSPACE, or Π2p. In addition to the main case where arbitrary parameters are allowed, we consider restricted problems with the number of parameters bounded by a constant, and the parameter-free case.

Our upper bounds are specific to clx logics, but we also include similar results for logics of bounded depth and width. In contrast, our lower bounds are very general: they apply each to a class of all transitive logics whose frames allow occurrence of certain finite subframes.

We also discuss the baseline problem of complexity of derivability: it is coNP-complete or PSPACE-complete for each clx logic. In particular, we prove PSPACE-hardness of derivability for a broad class of transitive logics that includes all logics with the disjunction property.

  1. Emil Jeřábek, Rules with parameters in modal logic I, Annals of Pure and Applied Logic 166 (2015), no. 9, pp. 881–933.

On the complexity of the clone membership problem

Theory of Computing Systems 65 (2021), no. 5, pp. 839–868. [DOI, arXiv] [PDF, PS] [BIB]

We investigate the complexity of the Boolean clone membership problem (CMP): given a set of Boolean functions F and a Boolean function f, determine if f is in the clone generated by F, i.e., if it can be expressed by a circuit with F-gates. Here, f and elements of F are given as circuits or formulas over the usual De Morgan basis. Böhler and Schnoor [1] proved that for any fixed F, the problem is coNP-complete, with a few exceptions where it is in P. Vollmer [2] incorrectly claimed that the full problem CMP is also coNP-complete. We prove that CMP is in fact ϴ2P-complete, and we complement Böhler and Schnoor’s results by showing that for fixed f, the problem is NP-complete unless f is a projection.

More generally, we study the problem B-CMP where F and f are given by circuits using gates from B. For most choices of B, we classify the complexity of B-CMP as being ϴ2P-complete (possibly under randomized reductions), coDP-complete, or in P.

  1. Elmar Böhler and Henning Schnoor, The complexity of the descriptiveness of Boolean circuits over different sets of gates, Theory of Computing Systems 41 (2007), no. 4, pp. 753–777.
  2. Heribert Vollmer, The complexity of deciding if a Boolean function can be computed by circuits over a restricted basis, Theory of Computing Systems 44 (2009), no. 1, pp. 82–90.

On the proof complexity of logics of bounded branching

Annals of Pure and Applied Logic 174 (2023), no. 1, article no. 103181, 54 pp. [DOI, arXiv] [PDF, PS] [BIB]

We investigate the proof complexity of extended Frege (EF) systems for basic transitive modal logics (K4, S4, GL, …) augmented with the bounded branching axioms BBk. First, we study feasibility of the disjunction property and more general extension rules in EF systems for these logics: we show that the corresponding decision problems reduce to total coNP search problems (or equivalently, disjoint NP pairs, in the binary case); more precisely, the decision problem for extension rules is equivalent to a certain special case of interpolation for the classical EF system. Next, we use this characterization to prove superpolynomial (or even exponential, with stronger hypotheses) separations between EF and substitution Frege (SF) systems for all transitive logics contained in S4.2GrzBB2 or GL.2BB2 under some assumptions weaker than PSPACE ≠ NP. We also prove analogous results for superintuitionistic logics: we characterize the decision complexity of multi-conclusion Visser’s rules in EF systems for Gabbay–de Jongh logics Tk, and we show conditional separations between EF and SF for all intermediate logics contained in T2 + KC.


Iterated multiplication in VTC0

Archive for Mathematical Logic 61 (2022), no. 5–6, pp. 705–767. [DOI, arXiv] [PDF, PS] [BIB]

We show that VTC0, the basic theory of bounded arithmetic corresponding to the complexity class TC0, proves the IMUL axiom expressing the totality of iterated multiplication satisfying its recursive definition, by formalizing a suitable version of the TC0 iterated multiplication algorithm by Hesse, Allender, and Barrington [1]. As a consequence, VTC0 can also prove the integer division axiom, and (by results of [2]) the RSUV-translation of induction and minimization for sharply bounded formulas. Similar consequences hold for the related theories Δb1-CR and C02.

As a side result, we also prove that there is a well-behaved Δ0 definition of modular powering in IΔ0+WPHP0).

  1. William Hesse, Eric Allender, and David A. Mix Barrington, Uniform constant-depth threshold circuits for division and iterated multiplication, Journal of Computer and System Sciences 65 (2002), no. 4, pp. 695–716.
  2. Emil Jeřábek, Open induction in a bounded arithmetic for TC0, Archive for Mathematical Logic 54 (2015), no. 3–4, pp. 359–394.

The theory of hereditarily bounded sets

Mathematical Logic Quarterly 68 (2022), no. 2, pp. 243–256. [DOI, arXiv] [PDF, PS] [BIB]

We show that for any k ∈ ω, the structure Hk,∈⟩ of sets that are hereditarily of size at most k is decidable. We provide a transparent complete axiomatization of its theory, a quantifier elimination result, and tight bounds on its computational complexity. This stands in stark contrast to the structure Vω = ⋃kHk of hereditarily finite sets, which is well known to be bi-interpretable with the standard model of arithmetic ⟨ℕ,+,⋅⟩.


Elementary analytic functions in VTC0

Annals of Pure and Applied Logic 174 (2023), no. 6, article no. 103269, 50 pp. [DOI, arXiv] [PDF, PS] [BIB]

It is known that rational approximations of elementary analytic functions (exp, log, trigonometric, and hyperbolic functions, and their inverse functions) are computable in the weak complexity class TC0. We show how to formalize the construction and basic properties of these functions in the corresponding theory of bounded arithmetic, VTC0.


Models of VTC0 as exponential integer parts

Mathematical Logic Quarterly 69 (2023), no. 2, pp. 244–260. [DOI, arXiv] [PDF, PS] [BIB]

We prove that (additive) ordered group reducts of nonstandard models of the bounded arithmetical theory VTC0 are recursively saturated in a rich language with predicates expressing the integers, rationals, and logarithmically bounded numbers. Combined with our previous results on the construction of the real exponential function on completions of models of VTC0, we show that every countable model of VTC0 is an exponential integer part of a real-closed exponential field.


A simplified lower bound for implicational logic

Preprint, 2023, 31 pp. [arXiv] [PDF, PS] [BIB]

We present a streamlined and simplified exponential lower bound on the length of proofs in intuitionistic implicational logic, adapted to Gordeev and Haeusler’s dag-like natural deduction.


A note on the complexity of addition

Preprint, 2023, 5 pp. [arXiv] [PDF, PS] [BIB]

We show that the sum of a sequence of integers can be computed in linear time on a Turing machine. In particular, the most obvious algorithm for this problem, which appears to require quadratic time due to carry propagation, actually runs in linear time by amortized analysis.


Back to publications