An independence of the MIN principle from the PHP principle

Mykyta Narusevych

arxiv: 2406.14930 · v5 · pith:J3Y76S34new · submitted 2024-06-21 · 🧮 math.LO · cs.LO

An independence of the MIN principle from the PHP principle

Mykyta Narusevych This is my paper

Pith reviewed 2026-05-24 00:31 UTC · model grok-4.3

classification 🧮 math.LO cs.LO

keywords bounded arithmeticpigeonhole principleminimization principleindependenceT1_2 theoryDelta1 formulaslinear orderingfinite intervals

0 comments

The pith

Bounded arithmetic theory with pigeonhole principle does not prove minimization principle.

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

The paper shows that the theory T¹₂(◃) plus pigeonhole principle instances for all Δ^b₁(◃) formulas fails to prove the minimization principle MIN(◃). A sympathetic reader would care because this establishes a separation between two basic facts about finite sets inside a weak arithmetic system. If correct, the result means that proofs of the existence of minimal elements in orderings require logical resources beyond those supplied by the pigeonhole principle at this level. The distinction clarifies the relative strength of these principles without moving to stronger theories.

Core claim

The bounded arithmetic theory T¹₂(◃) augmented by instances of the pigeonhole principle for all Δ^b₁(◃) formulas does not prove MIN(◃).

What carries the argument

The theory T¹₂(◃) augmented by Δ^b₁(◃) pigeonhole principle instances, which fails to derive the minimization principle for strict linear orderings on finite intervals.

If this is right

MIN(◃) is not derivable from the given augmentation of T¹₂(◃).
The separation applies specifically to pigeonhole instances for Δ^b₁(◃) formulas.
The result provides a lower bound on the strength needed to prove minimization inside this theory.
Other instances of combinatorial principles remain independent at this level of arithmetic.

Where Pith is reading between the lines

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

The separation may extend to similar weak theories with different base languages or orderings.
It could inform questions about the minimal resources needed to find minimal elements versus to establish injections or surjections.
Testing stronger classes of formulas in the pigeonhole principle might collapse or preserve the independence.

Load-bearing premise

The formalization of T¹₂(◃), MIN(◃), and the Δ^b₁(◃) instances of PHP correctly captures the intended principles inside the language of bounded arithmetic.

What would settle it

A formal derivation of MIN(◃) inside T¹₂(◃) plus the Δ^b₁(◃) PHP instances, or an explicit model satisfying the augmented theory but violating MIN(◃).

read the original abstract

The minimization principle $\textsf{MIN}(\triangleleft)$ studied in bounded arithmetic says that a strict linear ordering $\triangleleft$ on any finite interval $[0,\dots,n)$ has the minimal element. We shall prove that bounded arithmetic theory $\textsf{T}^1_2(\triangleleft)$ augmented by instances of the pigeonhole principle for all $\Delta^b_1(\triangleleft)$ formulas does not prove $\textsf{MIN}(\triangleleft)$.

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

T¹₂(◃) + Δ^b₁(◃)-PHP does not prove MIN(◃); a direct independence that follows standard bounded-arithmetic conventions.

read the letter

T¹₂(◃) plus the pigeonhole principle restricted to Δ^b₁(◃) formulas does not prove MIN(◃). That is the independence result on offer. The language adds a new strict order symbol to the usual bounded-arithmetic signature, and the theory is the expected extension of T¹₂. The claim is that even with those PHP instances the minimization principle for the new order remains unprovable. The formalization sticks to existing conventions for these principles, which makes the separation easy to place against prior work on PHP and minimization in weak systems. The abstract presents the separation as new rather than a corollary of an older result, so the contribution is a concrete data point on the relative strength of the restricted PHP. The main limitation is that only the abstract is visible here, so the model or witnessing argument that establishes the independence cannot be checked directly. The statement itself shows no circularity or mismatched quantifiers, and the stress-test found no internal inconsistency in the claim. This work is aimed at readers who already follow bounded arithmetic, Buss-style theories, and independence results inside them. Someone mapping axiom strengths in T¹₂ and its variants will see the value; outsiders will not. It deserves peer review. The setup is standard enough that referees can focus on the technical steps without first untangling nonstandard definitions.

Referee Report

2 major / 1 minor

Summary. The paper claims to prove that the bounded arithmetic theory T¹₂(◃), when augmented by all instances of the pigeonhole principle for Δ^b₁(◃) formulas, does not prove the minimization principle MIN(◃) asserting that every strict linear ordering ◃ on a finite interval [0,…,n) has a least element.

Significance. If the result holds, it would separate MIN(◃) from a natural strengthening of T¹₂(◃) by restricted PHP, clarifying the relative strengths of these principles inside the language of bounded arithmetic with an additional ordering symbol. The result is of interest for the program of calibrating the proof-theoretic strength of combinatorial principles in weak arithmetics.

major comments (2)

The abstract states the independence but provides no indication of the model construction or the class of formulas for which PHP is assumed; without the details of the model or the inductive argument establishing that MIN fails while the PHP instances hold, it is impossible to verify that the formalization of T¹₂(◃) correctly captures the intended theory.
Section 1 (or the introduction) should explicitly define the language, the axioms of T¹₂(◃), the precise syntactic class Δ^b₁(◃), and the statement of MIN(◃); the current abstract leaves open whether the ordering symbol ◃ is treated as a new predicate or function and how the bounded quantifiers interact with it.

minor comments (1)

Notation: the symbol ◃ is used both for the ordering and inside the theory name; a brief clarification of whether T¹₂(◃) denotes the theory in the expanded language would improve readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for these comments on clarity. We address each point below and will make the indicated revisions to the abstract and introduction.

read point-by-point responses

Referee: The abstract states the independence but provides no indication of the model construction or the class of formulas for which PHP is assumed; without the details of the model or the inductive argument establishing that MIN fails while the PHP instances hold, it is impossible to verify that the formalization of T¹₂(◃) correctly captures the intended theory.

Authors: The full manuscript details the model construction (a suitable nonstandard model of the base theory) and the inductive argument in Sections 2–3. We agree the abstract is too terse on these points and will revise it to briefly indicate the model used and confirm that PHP is taken for all Δ^b₁(◃) formulas while showing MIN(◃) fails. revision: yes
Referee: Section 1 (or the introduction) should explicitly define the language, the axioms of T¹₂(◃), the precise syntactic class Δ^b₁(◃), and the statement of MIN(◃); the current abstract leaves open whether the ordering symbol ◃ is treated as a new predicate or function and how the bounded quantifiers interact with it.

Authors: We agree that explicit definitions belong in the introduction. The language is that of bounded arithmetic augmented by a new binary predicate symbol ◃; T¹₂(◃) consists of the BASIC axioms plus Σ¹₁ induction in this language; Δ^b₁(◃) denotes the class of formulas that are both Σ^b₁(◃) and Π^b₁(◃); and MIN(◃) asserts that every strict linear order on [0,n) has a least element. Bounded quantifiers are interpreted in the usual way with respect to the ordering ◃. We will insert these definitions at the start of Section 1. revision: yes

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper states a standard independence result: T¹₂(◃) + Δ^b₁(◃)-PHP does not prove MIN(◃). The language, theory, minimization principle, and restricted PHP instances are formalized using conventions standard in bounded arithmetic (Buss-style languages with an added ordering symbol). The derivation is a mathematical non-provability argument whose steps are independent of the target statement; no self-definitional reductions, fitted inputs renamed as predictions, or load-bearing self-citations appear in the abstract or described claim. The result is self-contained against external benchmarks in the field.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The result rests on the standard axiomatization of bounded arithmetic T¹₂ together with the usual definitions of MIN and PHP; no new free parameters or invented entities are introduced in the abstract.

axioms (2)

standard math Standard axioms and induction schema of T¹₂(◃) in the language of bounded arithmetic with an additional order symbol
Invoked as the base theory in the first sentence of the abstract.
domain assumption Correct formalization of Δ^b₁(◃) formulas and the pigeonhole principle schema for them
The claim concerns instances of PHP restricted to this formula class.

pith-pipeline@v0.9.0 · 5590 in / 1185 out tokens · 23722 ms · 2026-05-24T00:31:02.061992+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 LogicNat.equivNat, embed_injective, realization_initial unclear

?

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

T¹₂(◃) + PHP(Δ^b₁(◃)) ⊬ ∀n MIN(◃)n (Thm 2.2); model via game GO on O-sequences with winning strategies for PIND/PPHP (Sec. 3–4)
IndisputableMonolith/Foundation/ArithmeticOf.lean PeanoObject.IsInitial, extracted_peanoSurface unclear

?

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

PHP-arrays and uniform o-trees of depth |n|^c; size bounds p(|o|+d)!/|o|! vs h(|o|+d)!/|o|! force p ≤ h (Cor. 4.9)

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.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

The Proof Analysis Problem
cs.CC 2025-06 unverdicted novelty 8.0

Short Resolution refutations of Ref(φ) yield satisfying assignments for φ in polynomial time via a PV1-formalizable construction, and the Proof Analysis Problem is NP-complete for Extended Frege.

Reference graph

Works this paper leans on

16 extracted references · 16 canonical work pages · cited by 1 Pith paper

[1]

M. Ajtai. The complexity of the pigeonhole principle. In Proceedings of the IEEE 29th Annual Symposium on Foundations of Computer Science , pages 346 – 355, 1988

work page 1988
[2]

Atserias and M

A. Atserias and M. M¨ uller. Partially definable forcing and bounded arith- metic. Archive for Mathematical Logic , 54:1–33, 2015

work page 2015
[3]

S. R. Buss. Bounded Arithmetic. PhD thesis, Princeton University, 1985

work page 1985
[4]

Chiari and J

M. Chiari and J. Kraj´ ıˇ cek. Witnessing Functions in Bounded Arithmetic and Search Problems. Journal of Symbolic Logic , 63(3):1095–1115, 1998. 16

work page 1998
[5]

Jeˇ r´ abek

E. Jeˇ r´ abek. Approximate counting by hashing in bounded arithmetic.Jour- nal of Symbolic Logic , 74(3):829 – 860, 2009

work page 2009
[6]

G. O. H. Katona. A simple proof of the Erd¨ os-Chao Ko-Rado Theorem. Journal of Combinatorial Theory, Series B , 13(2):183 – 184, 1972

work page 1972
[7]

Models of Peano Arithmetic

Richard Kaye. Models of Peano Arithmetic . Oxford University Press, 1991

work page 1991
[8]

Kraj´ ıˇ cek, P

J. Kraj´ ıˇ cek, P. Pudl´ ak, and A. Woods. Exponential lower bound to the size of bounded depth frege proofs of the pigeonhole principle. Random Structures and Algorithms , 7:15 – 39, 1995

work page 1995
[9]

Encyclopedia of Mathematics and its Applications

Jan Kraj´ ıˇ cek.Bounded Arithmetic, Propositional Logic and Complexity Theory. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1995

work page 1995
[10]

Encyclopedia of Mathematics and its Applications

Jan Kraj´ ıˇ cek.Proof Complexity . Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2019

work page 2019
[11]

Megiddo and U

N. Megiddo and U. Vishkin. On finding a minimum dominating set in a tournament. Theoretical Computer Science, 61(2):307–316, 1988

work page 1988
[12]

M¨ uller

M. M¨ uller. Typical forcings, NP search problems and an extension of a theorem of Riis. Annals of Pure and Applied Logic , 172(4):102930, 2021

work page 2021
[13]

Models of bounded arithmetic and variants of pigeon- hole principle, 2024

Mykyta Narusevych. Models of bounded arithmetic and variants of pigeon- hole principle, 2024

work page 2024
[14]

Paris and A

J. Paris and A. Wilkie. Counting problems in bounded arithmetic. In Carlos Augusto Di Prisco, editor, Methods in Mathematical Logic , pages 317–340, Berlin, Heidelberg, 1985. Springer Berlin Heidelberg

work page 1985
[15]

Pitassi, P

T. Pitassi, P. Beame, and R. Impagliazzo. Exponential lower bounds for the pigeonhole principle. Computational Complexity , 3:97 – 140, 1993

work page 1993
[16]

S. Riis. Making infinite structures finite in models of second order bounded arithmetic. Arithmetic, proof theory and computational complexity , pages 289–319, 1993. 17

work page 1993

[1] [1]

M. Ajtai. The complexity of the pigeonhole principle. In Proceedings of the IEEE 29th Annual Symposium on Foundations of Computer Science , pages 346 – 355, 1988

work page 1988

[2] [2]

Atserias and M

A. Atserias and M. M¨ uller. Partially definable forcing and bounded arith- metic. Archive for Mathematical Logic , 54:1–33, 2015

work page 2015

[3] [3]

S. R. Buss. Bounded Arithmetic. PhD thesis, Princeton University, 1985

work page 1985

[4] [4]

Chiari and J

M. Chiari and J. Kraj´ ıˇ cek. Witnessing Functions in Bounded Arithmetic and Search Problems. Journal of Symbolic Logic , 63(3):1095–1115, 1998. 16

work page 1998

[5] [5]

Jeˇ r´ abek

E. Jeˇ r´ abek. Approximate counting by hashing in bounded arithmetic.Jour- nal of Symbolic Logic , 74(3):829 – 860, 2009

work page 2009

[6] [6]

G. O. H. Katona. A simple proof of the Erd¨ os-Chao Ko-Rado Theorem. Journal of Combinatorial Theory, Series B , 13(2):183 – 184, 1972

work page 1972

[7] [7]

Models of Peano Arithmetic

Richard Kaye. Models of Peano Arithmetic . Oxford University Press, 1991

work page 1991

[8] [8]

Kraj´ ıˇ cek, P

J. Kraj´ ıˇ cek, P. Pudl´ ak, and A. Woods. Exponential lower bound to the size of bounded depth frege proofs of the pigeonhole principle. Random Structures and Algorithms , 7:15 – 39, 1995

work page 1995

[9] [9]

Encyclopedia of Mathematics and its Applications

Jan Kraj´ ıˇ cek.Bounded Arithmetic, Propositional Logic and Complexity Theory. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1995

work page 1995

[10] [10]

Encyclopedia of Mathematics and its Applications

Jan Kraj´ ıˇ cek.Proof Complexity . Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2019

work page 2019

[11] [11]

Megiddo and U

N. Megiddo and U. Vishkin. On finding a minimum dominating set in a tournament. Theoretical Computer Science, 61(2):307–316, 1988

work page 1988

[12] [12]

M¨ uller

M. M¨ uller. Typical forcings, NP search problems and an extension of a theorem of Riis. Annals of Pure and Applied Logic , 172(4):102930, 2021

work page 2021

[13] [13]

Models of bounded arithmetic and variants of pigeon- hole principle, 2024

Mykyta Narusevych. Models of bounded arithmetic and variants of pigeon- hole principle, 2024

work page 2024

[14] [14]

Paris and A

J. Paris and A. Wilkie. Counting problems in bounded arithmetic. In Carlos Augusto Di Prisco, editor, Methods in Mathematical Logic , pages 317–340, Berlin, Heidelberg, 1985. Springer Berlin Heidelberg

work page 1985

[15] [15]

Pitassi, P

T. Pitassi, P. Beame, and R. Impagliazzo. Exponential lower bounds for the pigeonhole principle. Computational Complexity , 3:97 – 140, 1993

work page 1993

[16] [16]

S. Riis. Making infinite structures finite in models of second order bounded arithmetic. Arithmetic, proof theory and computational complexity , pages 289–319, 1993. 17

work page 1993