arXiv subjects

Ondřej Ježil

Publications and source records attributed to Ondřej Ježil.

4 recordsLinked to original sources

arXiv2026

Prime Factorization in Models of PV$_1$

Assuming that no family of polynomial-size Boolean circuits can factorize a constant fraction of all products of two $n$-bit primes, we show that the bounded arithmetic theory $\text{PV}_1$, even when augmented by the sharply bounded choice scheme $BB(Σ^b_0)$, cannot prove that every number has some prime divisor. By the completeness theorem, it follows that under this assumption there is a model $M$ of $\text{PV}_1$ that contains a nonstandard number $m$ which has no prime factorization.

math.LO↗

arXiv2026

Parallelism and Adaptivity in Student-Teacher Witnessing

Student-Teacher Games are a model of computation in which a computationally restricted Student attempts to produce a string satisfying a refutable property, while an all-powerful Teacher refutes incorrect candidates by providing counterexamples. By the classical result of Krajíček, Pudlák, and Takeuti [KPT90], such games capture the witnessing of $\forall\exists\forall$-formulas in bounded arithmetic. In this paper, we introduce subclasses of total search problems in the polynomial hierarchy, classified by the number of rounds and candidate answers per round required for a Student at the corresponding level to solve them. Assuming the polynomial hierarchy does not collapse, we separate these classes for different number of rounds and queries. As applications we obtain the following results: (a) We study theories of bounded arithmetic axiomatized by fine-grained variants of length induction and bounded collection. We prove a general witnessing theorem connecting their $\forall\exists\forall$-consequences to the appropriate classes of Student-Teacher Games. Under the non-collapse of the polynomial hierarchy, we separate these theories. (b) These conditional separations resolve two open problems in bounded arithmetic: one by Buss and Ressayre [Bus85, CK93] on the strength of bounded collection, and one by Pollett [Pol97] on the difference between strict and non-strict double length induction. (c) Finally, we extend the unprovability of circuit upper bounds due to Krajíček and Oliveira [KO17] to the theory $PV_1+BB(Σ^b_1)$, and the unprovability of strong co-nondeterministic circuit lower bounds due to Pich and Santhanam [PS21] to the theory $PV_1+LLIND(sΣ^b_1)$. By the preceding separations, both theories strictly extend $PV_1$ assuming $NP\nsubseteq P/poly$.

cs.CC↗

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↗

arXiv2024

Limits of structures and Total NP Search Problems

For an infinite class of finite graphs of unbounded size, we define a limit object, to be called a $\textit{wide limit}$, relative to some computationally restricted class of functions. The limit object is a first order Boolean-valued structure. The first order properties of the wide limit then reflect how a computationally restricted viewer "sees" a generic member of the class. The construction uses arithmetic forcing with random variables [Krajíček, Forcing with random variables and proof complexity 2011]. We give sufficient conditions for universal and existential sentences to be valid in the limit, provide several examples, and prove that such a limit object can then be expanded to a model of weak arithmetic. To illustrate the concept we give an example in which the wide limit relates to total NP search problems. In particular, we take the wide limit of all maps from $\{0,\dots,k-1\}$ to $\{0,\dots,\lfloor k/2\rfloor-1\}$ to obtain a model of $\forall \text{PV}_1(f)$ where the problem $\textbf{RetractionWeakPigeon}$ is total but $\textbf{WeakPigeon}$, the complete problem for $\textbf{PWPP}$, is not. Thus, we obtain a new proof of this unprovability and show it implies that $\textbf{WeakPigeon}$ is not many-one reducible to $\textbf{RetractionWeakPigeon}$ in the oracle setting.

math.LO↗