A simplified lower bound for implicational logic
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.
cs.LO↗
arXiv subjects
Emil Jeřábek
Publications and source records attributed to Emil Jeřábek.
On the theory of exponential integer parts
We axiomatize the first-order theories of exponential integer parts of real-closed exponential fields in a language with $2^x$, in a language with a predicate for powers of 2, and in the basic language of ordered rings. In particular, the last theory extends IOpen by sentences expressing the existence of winning strategies in a certain game on integers; we show that it is a proper extension of IOpen, and give upper and lower bounds on the required number of rounds needed to win the game.
math.LO↗
A note on the theory of well orders
We give a simple proof that the first-order theory of well orders is axiomatized by transfinite induction, and that it is decidable.
math.LO↗
Models of $VTC^0$ as exponential integer parts
We prove that (additive) ordered group reducts of nonstandard models of the bounded arithmetical theory $\mathsf{VTC^0}$ 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 $\mathsf{VTC^0}$, we show that every countable model of $\mathsf{VTC^0}$ is an exponential integer part of a real-closed exponential field.
math.LO↗
A note on the complexity of addition
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.
cs.CC↗
Elementary analytic functions in $VTC^0$
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 $\mathrm{TC}^0$. We show how to formalize the construction and basic properties of these functions in the corresponding theory of bounded arithmetic, $\mathsf{VTC}^0$.
cs.LO↗
On the proof complexity of logics of bounded branching
We investigate the proof complexity of extended Frege (EF) systems for basic transitive modal logics (K4, S4, GL, ...) augmented with the bounded branching axioms $\mathbf{BB}_k$. 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 $\mathbf{S4.2GrzBB_2}$ or $\mathbf{GL.2BB_2}$ under some assumptions weaker than $\mathrm{PSPACE \ne 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 $\mathbf T_k$, and we show conditional separations between EF and SF for all intermediate logics contained in $\mathbf{T_2 + KC}$.
cs.LO↗
The theory of hereditarily bounded sets
We show that for any $k\inω$, the structure $(H_k,\in)$ 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_ω=\bigcup_k H_k$ of hereditarily finite sets, which is well known to be bi-interpretable with the standard model of arithmetic $(\mathbb N,+,\cdot)$.
math.LO↗
Iterated multiplication in $VTC^0$
We show that $VTC^0$, the basic theory of bounded arithmetic corresponding to the complexity class $\mathrm{TC}^0$, proves the $IMUL$ axiom expressing the totality of iterated multiplication satisfying its recursive definition, by formalizing a suitable version of the $\mathrm{TC}^0$ iterated multiplication algorithm by Hesse, Allender, and Barrington. As a consequence, $VTC^0$ can also prove the integer division axiom, and (by our previous results) the RSUV-translation of induction and minimization for sharply bounded formulas. Similar consequences hold for the related theories $Δ^b_1$-$CR$ and $C^0_2$. As a side result, we also prove that there is a well-behaved $Δ_0$ definition of modular powering in $IΔ_0+WPHP(Δ_0)$.
cs.LO↗
On the complexity of the clone membership problem
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 (2007) proved that for any fixed $F$, the problem is coNP-complete, with a few exceptions where it is in P. Vollmer (2009) incorrectly claimed that the full problem CMP is also coNP-complete. We prove that CMP is in fact $Θ^P_2$-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 $Θ^P_2$-complete (possibly under randomized reductions), coDP-complete, or in P.
cs.CC↗
Rules with parameters in modal logic II
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. We completely classify the complexity of unifiability or inadmissibility in any clx logic as being complete for one of $Σ^{\exp}_2$, NEXP, coNEXP, PSPACE, or $Π^p_2$. 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.
cs.LO↗
Induction rules in bounded arithmetic
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 $\hatΠ^b_i$ induction schemes, which were so far neglected in the literature. We present inclusions and conservation results between the systems (including a witnessing theorem for $T^i_2$ and $S^i_2$ 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.
math.LO↗
Recursive functions and existentially closed structures
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 $\exists\forall$ theories interpretable in existential theories in the process.
math.LO↗
Rigid models of Presburger arithmetic
We present a description of rigid models of Presburger arithmetic (i.e., Z-groups). In particular, we show that Presburger arithmetic has rigid models of all infinite cardinalities up to the continuum, but no larger.
math.LO↗
Galois connection for multiple-output operations
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\colon B^n\to B$, and classes (coclones) of relations $r\subseteq B^k$. We will present a generalization of this duality to classes of (multi-valued, partial) functions $f\colon B^n\to B^m$, employing invariants valued in partially ordered monoids instead of relations. In particular, our set-up encompasses the case of permutations $f\colon B^n\to B^n$, motivated by problems in reversible computing.
math.LO↗
Division by zero
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.
math.LO↗
Proof complexity of intuitionistic implicational formulas
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š \cite{hru:lbint}, generalized to exponential separation between EF and SF systems in superintuitionistic logics of unbounded branching by Jeřábek \cite{ej:sfef}, can be realized by implicational tautologies.
cs.LO↗
A note on the substructural hierarchy
We prove that all axiomatic extensions of the full Lambek calculus with exchange can be axiomatized by formulas on the $\mathcal N_3$ level of the substructural hierarchy.
cs.LO↗