26 found
Order:
  1. Complexity of Admissible Rules.Emil Jeřábek - 2007 - Archive for Mathematical Logic 46 (2):73-92.
    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 GL, S4, and IPC) is in coNE, thus obtaining a sharp complexity estimate for admissibility in these systems.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   14 citations  
  2.  20
    Independent Bases of Admissible Rules.Emil Jerábek - 2008 - Logic Journal of the IGPL 16 (3):249-267.
    We show that IPC, K4, GL, and S4, as well as all logics inheriting their admissible rules, have independent bases of admissible rules.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   15 citations  
  3.  11
    Canonical Rules.Emil Jeřábek - 2009 - Journal of Symbolic Logic 74 (4):1171 - 1205.
    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 [37]. 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 (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   11 citations  
  4.  19
    The Strength of Sharply Bounded Induction.Emil Jeřábek - 2006 - Mathematical Logic Quarterly 52 (6):613-624.
    We prove that the sharply bounded arithmetic T02 in a language containing the function symbol ⌊x /2y⌋ is equivalent to PV1.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   11 citations  
  5.  10
    Dual Weak Pigeonhole Principle, Boolean Complexity, and Derandomization.Emil Jeřábek - 2004 - Annals of Pure and Applied Logic 129 (1-3):1-37.
    We study the extension 123) of the theory S21 by instances of the dual weak pigeonhole principle for p-time functions, dWPHPx2x. 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. We construct a propositional proof system WF , which captures the Π1b-consequences of S21+dWPHP. We also show that WF p-simulates the Unstructured Extended Nullstellensatz proof system of Buss et al. 256). We prove that (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   13 citations  
  6.  9
    Recursive Functions and Existentially Closed Structures.Emil Jeřábek - forthcoming - Journal of Mathematical Logic:2050002.
    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 [Formula: see text] in which all partially recursive functions are representable, yet [Formula: see text] does not interpret Robinson’s theory [Formula: see text]. 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 (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  7. Approximate Counting in Bounded Arithmetic.Emil Jeřábek - 2007 - Journal of Symbolic Logic 72 (3):959 - 993.
    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 [15]. We discuss applications to formalization of randomized complexity classes (such as BPP, APP, MA, AM) in PV₁ + dWPHP(PV).
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  8.  11
    On Theories of Bounded Arithmetic for NC 1.Emil Jeřábek - 2011 - Annals of Pure and Applied Logic 162 (4):322-340.
    We develop an arithmetical theory and its variant , corresponding to “slightly nonuniform” . Our theories sit between and , and allow evaluation of log-depth bounded fan-in circuits under limited conditions. Propositional translations of -formulas provable in admit L-uniform polynomial-size Frege proofs.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  9.  10
    Frege Systems for Extensible Modal Logics.Emil Jeřábek - 2006 - Annals of Pure and Applied Logic 142 (1):366-379.
    By a well-known result of Cook and Reckhow [S.A. Cook, R.A. Reckhow, The relative efficiency of propositional proof systems, Journal of Symbolic Logic 44 36–50; R.A. Reckhow, On the lengths of proofs in the propositional calculus, Ph.D. Thesis, Department of Computer Science, University of Toronto, 1976], all Frege systems for the classical propositional calculus are polynomially equivalent. Mints and Kojevnikov [G. Mints, A. Kojevnikov, Intuitionistic Frege systems are polynomially equivalent, Zapiski Nauchnyh Seminarov POMI 316 129–146] have recently shown p-equivalence of (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  10.  14
    Sequence Encoding Without Induction.Emil Jeřábek - 2012 - Mathematical Logic Quarterly 58 (3):244-248.
    We show that the universally axiomatized, induction-free theory equation image is a sequential theory in the sense of Pudlák's 5, in contrast to the closely related Robinson's arithmetic.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  11.  20
    Substitution Frege and Extended Frege Proof Systems in Non-Classical Logics.Emil Jeřábek - 2009 - Annals of Pure and Applied Logic 159 (1-2):1-48.
    We investigate the substitution Frege () proof system and its relationship to extended Frege () in the context of modal and superintuitionistic propositional logics. We show that is p-equivalent to tree-like , and we develop a “normal form” for -proofs. We establish connections between for a logic L, and for certain bimodal expansions of L.We then turn attention to specific families of modal and si logics. We prove p-equivalence of and for all extensions of , all tabular logics, all logics (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  12.  24
    A Sorting Network in Bounded Arithmetic.Emil Jeřábek - 2011 - Annals of Pure and Applied Logic 162 (4):341-355.
    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 , under the assumption of the existence of suitable expander graphs. We derive a conditional p-simulation of the propositional sequent calculus in the monotone sequent calculus.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  13. Approximate Counting by Hashing in Bounded Arithmetic.Emil Jeřábek - 2009 - Journal of Symbolic Logic 74 (3):829-860.
    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.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  14.  13
    A Note on the Substructural Hierarchy.Emil Jeřábek - 2016 - Mathematical Logic Quarterly 62 (1-2):102-110.
  15.  12
    Proof Complexity of Intuitionistic Implicational Formulas.Emil Jeřábek - 2017 - Annals of Pure and Applied Logic 168 (1):150-190.
  16.  13
    Fragment of Nonstandard Analysis with a Finitary Consistency Proof.Michal Rössler & Emil Jeřábek - 2007 - Bulletin of Symbolic Logic 13 (1):54-70.
    We introduce a nonstandard arithmetic $NQA^-$ based on the theory developed by R. Chuaqui and P. Suppes in [2] (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\Delta_0 + EXP$ , and on the other hand, $NQA^+$ interprets the theories IΣ1 and $WKL_0$.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  17.  8
    Rigid Models of Presburger Arithmetic.Emil Jeřábek - 2019 - Mathematical Logic Quarterly 65 (1):108-115.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  18.  29
    The Ubiquity of Conservative Translations.Emil Jeřábek - 2012 - Review of Symbolic Logic 5 (4):666-678.
    We study the notion of conservative translation between logics introduced by (Feitosa & D’Ottaviano2001). 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 (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  19.  12
    Real Closures of Models of Weak Arithmetic.Emil Jeřábek & Leszek Aleksander Kołodziejczyk - 2013 - Archive for Mathematical Logic 52 (1-2):143-157.
    D’Aquino et al. (J Symb Log 75(1):1–11, 2010) 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 ${\Sigma^b_1-IND^{|x|_k}}$ . It also holds for IΔ0 (and even its subtheory IE 2) under a rather mild assumption on cofinality. On the other hand, (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  20.  13
    Rules with Parameters in Modal Logic I.Emil Jeřábek - 2015 - Annals of Pure and Applied Logic 166 (9):881-933.
  21.  8
    Cluster Expansion and the Boxdot Conjecture.Emil Jeřábek - 2016 - Mathematical Logic Quarterly 62 (6):608-614.
    No categories
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  22.  14
    A Note on Grzegorczyk's Logic.Emil Jeřábek - 2004 - Mathematical Logic Quarterly 50 (3):295-296.
    Grzegorczyk's modal logic 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 to a class of frames, which does not provably coincide with upwards well-founded posets in ZF alone.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  23.  10
    Open Induction in a Bounded Arithmetic for TC0.Emil Jeřábek - 2015 - Archive for Mathematical Logic 54 (3-4):359-394.
  24.  11
    Abelian Groups and Quadratic Residues in Weak Arithmetic.Emil Jeřábek - 2010 - Mathematical Logic Quarterly 56 (3):262-278.
    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 + iWPHP, and use it to derive Fermat's little theorem and Euler's criterion for the Legendre symbol in S22 + iWPHP extended by the pigeonhole principle PHP. We prove the quadratic reciprocity theorem in the arithmetic theories T20 + Count2 and I Δ0 + Count2 with modulo-2 counting (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  25.  8
    Proofs with Monotone Cuts.Emil Jeřábek - 2012 - Mathematical Logic Quarterly 58 (3):177-187.
    Atserias, Galesi, and Pudlák have shown that the monotone sequent calculus MLK quasipolynomially simulates proofs of monotone sequents in the full sequent calculus LK . 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.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark  
  26.  7
    Simulating Non-Prenex Cuts in Quantified Propositional Calculus.Emil Jerábek & Phuong Nguyen - 2011 - Mathematical Logic Quarterly 57 (5):524-532.
    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 . Previously this was known only for the treelike systems G*i. © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark