Weak-Arithmetic Pigeonhole Principles

Definitions and mathematical statement

In the usual first-order arithmetic language with addition, multiplication, and order, $\Delta_0$ formulas have only bounded quantifiers. The theory $\mathrm I\Delta_0$ permits induction for these formulas, with parameters. The expanded theory $\mathrm I\Delta_0(f)$ ordinarily allows the additional function symbol $f$ in the bounded-induction scheme; this convention requires source confirmation.

For positive integers $m,n$, write $\mathrm{PHP}_n^m(f)$ for \[ \left(\forall i\le m\ (i\ge1\Rightarrow1\le f(i)\le n)\right) \ \Longrightarrow\ \exists i,j\ (1\le i<j\le m\ \text{and }f(i)=f(j)). \] Thus no function mapping the $m$ pigeons into the $n$ holes can be injective. The notation $\mathrm{PHP}_n^m(\Delta_0)$ denotes the schema for graphs defined by bounded formulas, with parameters: whenever such a graph defines a total single-valued map from $\{1,\ldots,m\}$ to $\{1,\ldots,n\}$, it has a collision. This is a definability schema, not quantification over arbitrary set-coded functions unless the report supplies such coding.

The restored statement asks four provability questions: \[ \mathrm I\Delta_0\ \vdash\ \mathrm{PHP}_n^{n+1}(\Delta_0)\ ? \qquad \mathrm I\Delta_0\ \vdash\ \mathrm{PHP}_n^{n^2}(\Delta_0)\ ? \] \[ \mathrm I\Delta_0(f)\ \vdash\ \mathrm{PHP}_n^{2n}(f)\ ? \qquad \mathrm I\Delta_0(f)\ \vdash\ \mathrm{PHP}_n^{n^2}(f)\ ? \] Provability is intended uniformly in the size parameter and any allowed formula parameters. For $n+1$ and $2n$, the nontrivial domain has $n\ge1$. For $n^2$, one must at least specify $n\ge2$ so that the number of pigeons exceeds the number of holes; the source omits this small-parameter qualification. These are proof-strength questions, not a denial of the ordinary finite pigeonhole principle.

The retained original has different superscripts: it writes $n$ in both "or even" clauses and $n^2$ in the first expanded-language clause, whereas the restored statement uses $n^2$ in the former and $2n$ in the latter. The original $m=n$ clauses do not express a no-injection pigeonhole assertion. This substantive restoration must be checked against the report; it is not merely delimiter normalization. No version is silently identified with another.

Short English statement

The question asks whether bounded-induction arithmetic proves four pigeonhole schemes for definable maps or an added function symbol. The restored pigeon counts are retained, while conflicting original superscripts, small values of $n$, and the expanded induction convention are flagged.

Sources

• Local UnsolvedMath registry, permanent ID 30000618, code catalogue entry, "Weak-Arithmetic Pigeonhole Principles." Proposed year 2006; proposer unspecified.
• Mini-workshop: Logic, Combinatorics and Independence Results (2007), Oberwolfach Reports, pp. 3087--3130, DOI 10.4171/owr/2006/52; https://doi.org/10.4171/owr/2006/52. The displayed report year 2007 differs from the DOI and proposed year 2006. This is the sole supplied literature reference.
• Statement status corrected_verified; the supplied verification claims official-report checking and normalization without changing source-level content. The explicit superscript differences between original and restored fields nevertheless require review.
• Literature triage checked 2026-08-21: open. It generically describes an unresolved problem/conjecture/direction and says no authoritative complete resolution was located in the supplied check. It does not assess each scheme separately. Created 2026-08-25; updated 2026-09-16. Current status and exact formulations require independent verification.
• Registry curation by Ulam AI / UnsolvedMath Contributors, CC BY 4.0; the underlying report retains its supplied provenance. Unreviewed statement-only draft.