Prime Factorization in Models of PV$_1$

Ond\v{r}ej Je\v{z}il

arxiv: 2505.14516 · v5 · submitted 2025-05-20 · 🧮 math.LO · cs.LO

Prime Factorization in Models of PV₁

Ond\v{r}ej Je\v{z}il This is my paper

Pith reviewed 2026-05-22 14:09 UTC · model grok-4.3

classification 🧮 math.LO cs.LO

keywords bounded arithmeticPV1prime factorizationunprovabilitycryptographic assumptionsmodels of arithmeticsharply bounded choice

0 comments

The pith

Under a standard assumption about the hardness of factoring, PV1 cannot prove that every number has a prime divisor.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that if no polynomial-size circuit family factors a constant fraction of products of two n-bit primes, then the theory PV1 even with the sharply bounded choice scheme BB(Σ^b_0) fails to prove that every number has a prime divisor. By the completeness theorem this yields a model of PV1 containing a nonstandard element with no prime factorization at all. A sympathetic reader cares because the result ties a concrete computational hardness statement directly to the inability of a weak arithmetical theory to capture an elementary fact of number theory.

Core claim

Assuming that no family of polynomial-size Boolean circuits can factorize a constant fraction of all products of two n-bit primes, the bounded arithmetic theory PV₁, 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 PV₁ that contains a nonstandard number m which has no prime factorization.

What carries the argument

The cryptographic assumption that no polynomial-size circuit family factors a constant fraction of semiprimes, used via the completeness theorem to produce a model of PV1 containing a nonstandard element without prime factors.

If this is right

PV1 augmented by BB(Σ^b_0) does not prove that every number has a prime divisor.
There exist models of PV1 containing nonstandard numbers that possess no prime factorization.
The failure to prove the prime-divisor statement persists even after the addition of the sharply bounded choice scheme.
The unprovability is conditional on the stated circuit-complexity assumption about semiprimes.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The result links the computational difficulty of factoring to the logical strength of very weak arithmetical theories in a direct way.
Similar hardness assumptions could potentially be applied to other elementary number-theoretic statements inside PV1.
The existence of such models suggests that prime factorization may lie outside the reach of the proof methods available in PV1 even for nonstandard elements.

Load-bearing premise

The assumption that no polynomial-size circuit family factors a constant fraction of all products of two n-bit primes must hold; if it fails the unprovability result does not follow.

What would settle it

The construction of a polynomial-size circuit family that factors a constant fraction of products of two n-bit primes would make the hardness assumption false and thereby block the derivation that PV1 cannot prove the prime-divisor statement.

read the original abstract

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(\Sigma^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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper shows that under a semiprime factoring circuit assumption, PV1 plus BB cannot prove every number has a prime divisor, yielding a model with a nonstandard element lacking factors.

read the letter

The key point is that if no polynomial-size circuit family factors a constant fraction of n-bit semiprimes, then PV1 even with the sharply bounded choice scheme BB(Σ0b) fails to prove that every number has a prime divisor. Completeness then gives a model containing a nonstandard m with no prime factors at all. This is the central conditional independence result. The paper does a clean job linking the complexity assumption to the arithmetic theory. It appears to extract circuits from a supposed proof via witnessing or Herbrand-style methods, treating the BB choices as extra bounded witnesses that still keep the circuit size polynomial. That step looks handled without obvious gaps based on the available description. The specific choice of semiprime factoring as the hardness source also seems like a targeted addition rather than a generic restatement of earlier bounded-arithmetic limitations. The main soft spot is that everything rests on the external crypto assumption. If small circuits do factor enough semiprimes, the unprovability claim simply does not go through, and the paper makes no claim to unconditional independence. That is not a flaw in the reduction itself but does limit how far the result travels on its own. With only the abstract and summary in hand it is hard to inspect every derivation detail, yet the stress-test note indicates no load-bearing internal contradiction or circularity. Readers working on bounded arithmetic, proof complexity, or crypto lower bounds would get the most from this. It is the sort of targeted conditional result that deserves a serious referee rather than a desk rejection, even if the proofs will need close checking in review.

Referee Report

2 major / 2 minor

Summary. Assuming that no family of polynomial-size Boolean circuits can factorize a constant fraction of all products of two n-bit primes, the paper shows that the bounded arithmetic theory PV₁, 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 PV₁ that contains a nonstandard number m which has no prime factorization.

Significance. If the result holds, it establishes a conditional independence between a basic number-theoretic statement and a weak theory of bounded arithmetic, under a standard cryptographic hardness assumption on factoring. The explicit handling of the BB(Σ^b_0) scheme via witnessing extraction that preserves polynomial circuit size is a technical strength, extending prior work on factorization and provability in PV₁. The result is falsifiable in the sense that a polynomial-time factoring algorithm for a positive fraction of semiprimes would refute the unprovability claim.

major comments (2)

[§3.3] §3.3, Theorem 3.4: The witnessing argument for formulas involving BB(Σ^b_0) must explicitly bound the circuit size when the choice functions are extracted as additional witnesses; it is unclear whether the polynomial bound on circuit size remains uniform when the number of choices is itself bounded by a term in the language.
[§4.1] §4.1, Lemma 4.2: The reduction from a supposed proof of ∀x∃p (p|x ∧ Prime(p)) to a circuit family for semiprime factorization relies on the completeness theorem for the model construction; the paper should verify that the nonstandard element m is obtained without additional assumptions on the language or the theory beyond what is stated.

minor comments (2)

The definition of the scheme BB(Σ^b_0) is given only in §2; moving a brief reminder to the introduction would improve accessibility for readers outside bounded arithmetic.
[§3] Notation for the circuit family C_n in the cryptographic assumption should be introduced consistently with the witnessing functions extracted from proofs.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading of the manuscript and the constructive comments. We address the major comments below and will incorporate clarifications in a revised version.

read point-by-point responses

Referee: [§3.3] §3.3, Theorem 3.4: The witnessing argument for formulas involving BB(Σ^b_0) must explicitly bound the circuit size when the choice functions are extracted as additional witnesses; it is unclear whether the polynomial bound on circuit size remains uniform when the number of choices is itself bounded by a term in the language.

Authors: We appreciate this observation. In the proof of Theorem 3.4, the witnessing theorem for PV1 + BB(Σ^b_0) extracts polynomial-size circuits for the choice functions. Since the number of choices is bounded by a term t in the language, and t is evaluated in the standard model for the circuit size calculation, the resulting circuit family has size polynomial in the input length, with the degree uniform across the bounded number of choices. We will revise the text to explicitly state this bound and its uniformity. revision: yes
Referee: [§4.1] §4.1, Lemma 4.2: The reduction from a supposed proof of ∀x∃p (p|x ∧ Prime(p)) to a circuit family for semiprime factorization relies on the completeness theorem for the model construction; the paper should verify that the nonstandard element m is obtained without additional assumptions on the language or the theory beyond what is stated.

Authors: The application of the completeness theorem is standard: since PV1 + BB(Σ^b_0) does not prove the sentence ∀x∃p (p|x ∧ Prime(p)), by the completeness theorem there exists a model M of the theory in which the sentence fails. Thus, there is a nonstandard element m in M such that M ⊨ ¬∃p (p|m ∧ Prime(p)). The language is the standard language of PV1, and no additional assumptions are required beyond the consistency of the theory, which follows from the cryptographic assumption. We will add a brief clarification in the proof of Lemma 4.2 to emphasize this. revision: yes

Circularity Check

0 steps flagged

No significant circularity; result is conditional on independent cryptographic hypothesis via standard witnessing and completeness

full rationale

The derivation assumes an external complexity hypothesis (no poly-size circuit family factors a constant fraction of n-bit semiprimes) and shows that any proof of prime factorization in PV₁ + BB(Σ^b_0) would yield a contradicting circuit family via witnessing/Herbrand extraction (with bounded choices treated as additional witnesses). Completeness then produces the desired model. This chain does not reduce any claim to a self-definition, fitted parameter renamed as prediction, or load-bearing self-citation; the cryptographic assumption is independent and falsifiable outside the paper. No equations or steps in the abstract or described argument exhibit the enumerated circular patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the standard completeness theorem for first-order logic and the external cryptographic assumption; no free parameters or invented entities are introduced.

axioms (1)

standard math Completeness theorem for first-order logic
Invoked to obtain a model M from the unprovability of the prime-divisor statement.

pith-pipeline@v0.9.0 · 5608 in / 1091 out tokens · 42691 ms · 2026-05-22T14:09:42.300714+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/ArithmeticFromLogic.lean equivNat, recovery theorem (LogicNat ≃ Nat) unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

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 PV1, even when augmented by the sharply bounded choice scheme BB(Σ^b_0), cannot prove that every number has some prime divisor.
IndisputableMonolith/Foundation/ArithmeticOf.lean canonical_peanoSurface, extracted_peanoSurface unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

By the completeness theorem, it follows that under this assumption there is a model M of PV1 that contains a nonstandard number m which has no prime factorization.

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.