# An independence of the MIN principle from the PHP principle
Preliminary version

Mykyta Narusevych111Supported by the Charles University project
PRIMUS/21/SCI/014, Charles University Research Centre program No.
UNCE/24/SCI/022 and GA UK project No. 246223

(Faculty of Mathematics and Physics
Charles University222Sokolovská 83, Prague, 186 75, The Czech Republic)

###### Abstract

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

##  1 Introduction

The MIN principle was introduced in bounded arithmetic in [4] while studying
definable search problems and witnessing theorems. It is a
$\Sigma^{b}_{2}$-formula $\text{MIN}(\prec)$ expressing that if $\prec$ is a
linear ordering of $\\{0,\dots,n-1\\}$, then it must have the minimal element.
It defines a total $\Sigma^{p}_{2}$ search problem: either certify that
$\prec$ is not a strict linear order or find the minimum (in fact, this
problem can be easily reduced to the same one for $\prec^{\prime}$ defined
uniformly from $\prec$ that is always a strict linear ordering).

An intriguing open question is whether the relativized theory
$T^{1}_{2}(\alpha)$ augmented by instances of the MIN principle stated for all
$\Delta^{b}_{1}(\alpha)$-formulas proves $T^{2}_{2}(\alpha)$ (cf. Section 2 or
[7] for definitions of these notions).

By [4] MIN($\prec$) is not provable in $T^{1}_{2}(\prec)$, while it is
provable in $T^{2}_{2}(\prec)$, in particular implying
$T^{2}_{2}(\alpha)\vdash\text{MIN}(\varphi(x,y))$ for $\varphi(x,y)$ an
arbitrary $\Delta^{b}_{1}(\alpha)$-formula.

The above question is generally motivated by open problems in bounded
arithmetic and in proof complexity (cf. the $d$ vs $d+1$ problem and the
R(log) problem in [7]). We do not solve this here but instead, we show that
the theory $T^{1}_{2}(\prec)+\text{MIN}(\prec)$ is much stronger than
$T^{1}_{2}(\prec)$ alone: $T^{1}_{2}(\prec)$ even augmented by all instances
of the PHP principle for all $\Delta^{b}_{1}(\prec)$ relations does not prove
MIN.

Note that, if one replaces the PHP principle with the weak PHP principle, the
above separation follows directly from [11], which establishes the
unprovability of any strong combinatorial principle (MIN in our case) from any
weak combinatorial principle (WPHP in our case) over $T^{1}_{2}(PV(\alpha))$.

As a further demonstration of the applicability of here presented techniques,
we outline some more limitations of the theory
$T^{1}_{2}(\alpha)+\text{PHP}(\Delta^{b}_{1}(\alpha))$. In particular, we show
that this theory cannot prove either the dual weak pigeonhole principle or the
tournament principle (see Section 5 for definitions).

The paper is organized as follows:

In Section 2 we introduce all the notions and key results relevant to the
content of the paper. This includes the theory of bounded arithmetic
$T^{1}_{2}$ (and its relativized version $T^{1}_{2}(\prec)$) and the
combinatorial principles MIN and PHP.

In Section 3 we outline a game-theoretic method of constructing a model
satisfying
$T^{1}_{2}(\prec)+\text{PHP}(\Delta^{b}_{1}(\prec))+\neg\text{MIN}(\prec)$. We
add a short discussion on how one can view here presented construction through
the lens of the forcing method at the end of the section.

In Section 4 we prove two combinatorial theorems towards finishing model
construction presented in the previous section. We then show how to build a
rather pathological model by a slight modification to the construction.

In Section 5 we sketch additional separations using machinery developed in the
previous sections. In particular, we deal with the tournament principle and
the dual weak pigeonhole principle. We also extend the $\prec$ total ordering
with no endpoints to a discrete ordering. Finally, we formulate an open
problem related to the methods used in the paper.

##  2 Preliminaries

###  2.1 Bounded Arithmetic

The paper studies relativized bounded arithmetic theory $T^{1}_{2}(\prec)$
with $\prec$-a binary relation symbol. Readers familiar with Bounded
Arithmetic may skip the next two subsections and head straight to 2.3.

Recall that the above (unrelativized) theory belongs to a well-known family of
sound axiomatizations of natural numbers collectively known as Bounded
Arithmetic (see [3] or [7] for a detailed exposition). These theories contain
axioms in the Buss’s language $L_{S_{2}}$ composed of

  * •

constant symbols $0$ and $1$,

  * •

unary operations $\lfloor\frac{x}{2}\rfloor$ and $|x|$,

  * •

binary operations $x+y$, $x\cdot y$ and $x\\#y$,

  * •

binary relation $x\leq y$.

The intended meanings of $0,1,\lfloor\frac{x}{2}\rfloor,x+y,x\cdot y,x\leq y$
are obvious. Symbol $|x|$ denotes bit-length of $x$, i.e.
$|x|=\lfloor\log_{2}x\rfloor+1$, and $x\\#y$ stands for binary smash function
which is standardly interpreted as $2^{|x|\cdot|y|}$.

An important bounded arithmetic theory is a theory known as $S^{1}_{2}$. It is
axiomatized by a finite number of true statements expressing the most basic
properties of $L_{S_{2}}$-symbols jointly forming the so-called BASIC theory
plus a single axiom scheme PIND accepted for all $\Sigma^{b}_{1}$-formulas
(i.e. NP-predicates).

To give more details, we start with the notion of a bounded formula. Recall
that $L_{S_{2}}$-formula $\varphi$ is called bounded if it (is logically
equivalent to a formula that) contains only bounded occurrences of all the
quantifiers, i.e. each quantifier is either $\forall x\leq t$ or $\exists
x\leq t$ with $t$ being a term not containing $x$.

A formula $\varphi$ is called sharply bounded if it is bounded and the
bounding terms are all wrapped by the $|x|$-symbol, i.e. each such term $t$ is
of the form $|s|$ with $s$ an arbitrary $L_{S_{2}}$-term.

The class of sharply bounded formulas is denoted as $\Delta^{b}_{0}$.

The class $\Sigma^{b}_{1}$ is defined as (the tautological closure of) the
smallest set of bounded formulas extending $\Delta^{b}_{0}$ and satisfying the
below closure properties

  * •

given $\varphi,\psi\in\Sigma^{b}_{1}$ both $\varphi\land\psi$ and
$\varphi\lor\psi$ are in $\Sigma^{b}_{1}$,

  * •

given $\varphi\in\Sigma^{b}_{1}$ and $t$ an $L_{S_{2}}$-term, both $\forall
x\leq|t|\varphi$ and $\exists x\leq|t|\varphi$ are in $\Sigma^{b}_{1}$,

  * •

given $\varphi\in\Sigma^{b}_{1}$ and $t$ an $L_{S_{2}}$-term, $\exists x\leq
t\varphi$ is in $\Sigma^{b}_{1}$.

The class $\Pi^{b}_{1}$ is defined as the set of formulas $\varphi$ such that
$\neg\varphi\in\Sigma^{b}_{1}$. It is easy to see that in the standard model,
$\Sigma^{b}_{1}$ defines exactly NP predicates, while $\Pi^{b}_{1}$ \- coNP
predicates.

For a formula $\varphi(x)$ we denote PIND($\varphi$) as the following
statement

$\displaystyle(\varphi(0)\land\forall
x(\varphi(\lfloor\frac{x}{2}\rfloor)\to\varphi(x)))\to\forall x\varphi(x)$

PIND is called polynomial induction scheme. The usual induction scheme is
denoted as IND.

We omit the detailed treatment of BASIC here. Interested readers may consult
[3] or [7].

Theory $S^{1}_{2}$ is defined as BASIC with PIND($\varphi$) for all
$\varphi\in\Sigma^{b}_{1}$. Theory $T^{1}_{2}$ is defined as BASIC with
IND($\varphi$) for all $\varphi\in\Sigma^{b}_{1}$. Straightforward argument
shows $T^{1}_{2}\vdash S^{1}_{2}$, while the opposite direction is among the
deepest problems of the area.

The class $\Delta^{b}_{1}$ denotes all formulas $\varphi\in\Sigma^{b}_{1}$ for
which one can find another $\Sigma^{b}_{1}$-formula $\psi$ so that
$S^{1}_{2}\vdash\varphi\leftrightarrow\neg\psi$. Note that replacing
“$S^{1}_{2}\vdash$” with “$\mathbb{N}\vDash$” gives exactly NP $\cap$ coNP.

######  Theorem 2.1 (Buss [3]).

A relation $R(\overline{x})$ on numbers is in P if and only if it is definable
by a $\Delta^{b}_{1}$-formula $\varphi(\overline{x})$.

In fact, the above holds (and originally was proven) in a stronger sense, see
[3] or [7, Thm.7.2.3].

###  2.2 Relativized theories

Along with the theories $S^{1}_{2}$ and $T^{1}_{2}$ described in the previous
subsection, there are their so-called relativized cousins $S^{1}_{2}(\alpha)$
and $T^{1}_{2}(\alpha)$. They are formed by extending $L_{S_{2}}$ by arbitrary
relation symbols without specifying any new particular axioms. However, all
new symbols may appear inside IND/PIND instances.

Relativized theories are most notably related to constant-depth Frege systems.
We omit discussing such connections and interested readers may find all the
details and much more in [8] and [7].

Below we give a more formal treatment of $T^{1}_{2}(\alpha)$ and
$S^{1}_{2}(\alpha)$ together with $\Delta^{b}_{1}(\alpha)$. In our case,
however, we are dealing with a single additional binary relation $\prec$ and
accordingly, we will denote the resulting theories $S^{1}_{2}(\prec)$ and
$T^{1}_{2}(\prec)$.

The notion of bounded and sharply bounded formulas remains the same, now with
formulas possibly containing $\prec$. Since $\prec$ is a relation, it does not
interfere with the term bounds of the quantifiers.

The classes $\Sigma^{b}_{1}(\prec)$ and $\Pi^{b}_{1}(\prec)$ are defined
exactly as before, the only difference being that $\Delta^{b}_{0}(\prec)$ now
contains sharply bounded formulas in the extended language. Theory
$S^{1}_{2}(\prec)$ is defined as BASIC together with the PIND scheme accepted
for $\Sigma^{b}_{1}(\prec)$ formulas. To get $T^{1}_{2}(\prec)$ replace PIND
with IND.

As before, $T^{1}_{2}(\prec)\vdash S^{1}_{2}(\prec)$ by a straightforward
argument. This time, however, we know that $S^{1}_{2}(\prec)\nvdash
T^{1}_{2}(\prec)$ [7, Sec.10.4].

Finally, the class $\Delta^{b}_{1}(\prec)$ is defined as the set of all
$\Sigma^{b}_{1}(\prec)$-formulas equivalent to $\Pi^{b}_{1}(\prec)$-formulas
provably in $S^{1}_{2}(\prec)$.

Below is essentially a corollary to the Theorem 2.1.

######  Corollary 2.2.

Let $\varphi(\overline{x})$ a $\Delta^{b}_{1}(\prec)$-formula with all free
variables exposed. There exists a poly-time algorithm $A$ which on input
$\overline{a}$ decides the truth value of $\varphi(\overline{a})$ given black-
box access to $\prec$.

Black-box access means $A$ can check in a unit-time whether $a\prec b$ holds
for arbitrary numbers $a,b$, while the full relation $\prec$ is unknown to
$A$.

###  2.3 MIN and PHP principles

We denote the set $\\{0,\dots,m-1\\}$ as $[0,\dots,m)$

The following formula expresses that, assuming $\prec$ defines a total strict
linear ordering on an initial interval of numbers $[0,\dots,n)$, there exists
a number $a_{min}<n$ which is a minimum of $\prec$ on $[0,\dots,n)$:

$\displaystyle\exists a<n\>(a\prec a)$ $\displaystyle\lor$
$\displaystyle\exists a\neq b<n\>(a\nprec b\land b\nprec a)$
$\displaystyle\lor$ $\displaystyle\exists a,b,c<n\>(a\prec b\land b\prec
c\land a\nprec c)$ $\displaystyle\lor$ $\displaystyle\exists
a_{min}<n\>\forall b\neq a_{min}<n\>(a_{min}\prec b)$

The above expression (known as minimization principle) was introduced in
bounded arithmetic in [4] where it was shown that it is provable in
$T^{2}_{2}(\prec)$ but not in $T^{1}_{2}(\prec)$.

In our paper, we show that a theory much stronger than $T^{1}_{2}(\prec)$
still does not prove MIN($\prec$).

Given a $\Delta^{b}_{1}(\prec)$-formula $\varphi(x,y)$ (possibly with free
variables other than $x,y$) and numbers $p>h$, the following formula expresses
that, assuming $\varphi(x,y)$ defines a binary relation that is the graph of
an injective function with domain $[0,\dots,p)$ and range $[0,\dots,h)$,
$\varphi(x,y)$ cannot be total:

$\displaystyle\exists a\neq b<p\>\exists c<h\>(\varphi(a,b)\land\varphi(a,c))$
$\displaystyle\lor$ $\displaystyle\exists a<p\>\exists b\neq
c<h\>(\varphi(a,b)\land\varphi(a,c))$ $\displaystyle\lor$
$\displaystyle\exists a<p\>\forall b<h\>(\neg\varphi(a,b))$

The above is a variant of a well-known pigeonhole principle here denoted as
$\text{PHP}^{p}_{h}(\varphi(x,y))$.

Replacing $\varphi(x,y)$ above with a binary relation symbol $R(x,y)$ and
letting $p,h$ be $n+1,n$, respectively, results in a formula
$\text{PHP}^{n+1}_{n}(R(x,y))$ famously known to be unprovable in the bounded
arithmetic $S_{2}(R)$ [1, 9, 15].

We denote the set of formulas $\text{PHP}^{p}_{h}(\varphi(x,y))$ for each
$\Delta^{b}_{1}(\prec)$-formula $\varphi(x,y)$ and $p>h$ as
PHP($\Delta^{b}_{1}(\prec)$). The main result of the current paper can now be
expressed formally as

######  Theorem 2.3.

$\displaystyle
T^{1}_{2}(\prec)+\text{PHP}(\Delta^{b}_{1}(\prec))\nvdash\text{MIN}(\prec)$

##  3 Model construction

###  3.1 Game $G_{\mathbb{O}}$

The main result is proven by constructing a model of

$\displaystyle T^{1}_{2}(\prec)+\text{PHP}(\Delta^{b}_{1}(\prec))+\exists
n\>\neg\text{MIN}(\prec)$

We start with a countable non-standard model of true arithmetic in
$L_{S_{2}}$-language $\mathbb{M}$. Pick $n$ \- a non-standard number in
$\mathbb{M}$ and let $\mathbb{I}$ be a substructure with domain

$\displaystyle\\{m\>|\>m<2^{|n|^{c}}\text{ for a standard }c\\}$

Our goal is to suitably interpret $\prec$ in $\mathbb{I}$ to satisfy all the
properties we need. This is achieved by a suitable step-by-step construction
which we view as a game played between three parties denoted here as
$P_{\text{MIN}},P_{\text{IND}},P_{\text{PHP}}$.

Players start with $\prec$ being the empty relation, and subsequently extend
it each by $\leq|n|^{c}$-large part with $c$ a standard constant (not
necessarily uniform). The only invariant they maintain is $\prec$ always being
total (on the current domain) strict ordering.

Players do not communicate with each other and so must be able to react to any
of the previous’ players moves.

######  Definition 3.1.

We denote $\mathbb{O}$ the set of $\leq|n|^{c}$-large sequences of distinct
numbers from $[0,\dots,n)$ with $c$ \- arbitrary standard constant.

Each $o\in\mathbb{O}$ induces strict partial ordering of $[0,\dots,n)$ denoted
$\prec_{o}$ in an obvious way: the domain are the numbers in $o$ and their
ordering is the order in which they are listed in $o$.

We say $o^{\prime}\in\mathbb{O}$ extends $o\in\mathbb{O}$ (denoted
$o^{\prime}\geq o$ or $o\leq o^{\prime}$) if
$\prec_{o^{\prime}}\supseteq\prec_{o}$ (note this tacitly assumes
$\prec_{o^{\prime}}$ and $\prec_{o}$ are compatible strict orderings).

We say $o^{\prime}\in\mathbb{O}$ is compatible to $o\in\mathbb{O}$ (denoted
$o^{\prime}\|o$) if $\prec_{o^{\prime}}$ is compatible to $\prec_{o}$ as
string orderings. This is equivalent to $\exists
o^{\prime\prime}\in\mathbb{O}$ so that $o^{\prime\prime}\geq o^{\prime},o$.

We say $o^{\prime}\in\mathbb{O}$ is incompatible with $o\in\mathbb{O}$
(denoted $o^{\prime}\perp o$) if $o^{\prime}$ is not compatible with $o$.

######  Definition 3.2.

A game $G_{\mathbb{O}}$ is played by three players
$P_{\text{MIN}},P_{\text{IND}},P_{\text{PHP}}$.

$P_{\text{MIN}}$ plays each $k$th step, with $k\equiv 0\mod 3$. Similarly,
$P_{\text{IND}}$ plays each $k$th step for $k\equiv 1\mod 3$ and
$P_{\text{PHP}}$ plays each $k$th step for $k\equiv 2\mod 3$.

Let $o_{0}$ be the empty sequence. In the $k$th step, being presented with
$o_{k}\in\mathbb{O}$, a player chooses $o_{k+1}\geq o_{k}$ from $\mathbb{O}$
and ends their turn, passing $o_{k+1}$ to the next player.

A strategy $\mathcal{S}$ is a function which on input $o\in\mathbb{O}$ outputs
$o^{\prime}\in\mathbb{O}$ so that $o^{\prime}\geq o$.

Fixing strategies
$\mathcal{S}_{\text{MIN}},\mathcal{S}_{\text{IND}},\mathcal{S}_{\text{PHP}}$
of respective players induces fixed chain $o_{0}\leq o_{1}\leq o_{2}\leq\dots$
produced by players utilizing their strategies. This, in turn, induces an
ordering denoted as
$\prec_{\mathcal{S}_{\text{MIN}},\mathcal{S}_{\text{IND}},\mathcal{S}_{\text{PHP}}}=\cup_{i}\prec_{o_{i}}$.
We drop subscripts if
$\mathcal{S}_{\text{MIN}},\mathcal{S}_{\text{IND}},\mathcal{S}_{\text{PHP}}$
are clear from the context.

$\mathbb{I}_{\prec_{\mathcal{S}_{\text{MIN}},\mathcal{S}_{\text{IND}},\mathcal{S}_{\text{PHP}}}}$
denotes $\mathbb{I}$ interpreting $\prec$-symbol as
$\prec_{\mathcal{S}_{\text{MIN}},\mathcal{S}_{\text{IND}},\mathcal{S}_{\text{PHP}}}$.

The goal of $P_{\text{MIN}}$ is for resulting $\prec$ to be a total linear
order of $[0,\dots,n)$ wit no minimal element no matter how other players pick
their moves.

The goal of $P_{\text{IND}}$ is for resulting $\mathbb{I}_{\prec}$ to satisfy
IND($\Sigma^{b}_{1}(\prec)$) no matter how other players pick their moves.

The goal of $P_{\text{PHP}}$ is for resulting $\mathbb{I}_{\prec}$ to satisfy
PHP($\Delta^{b}_{1}(\prec)$) no matter how other players pick their moves.

A strategy of the respective players is called winning if, no matter how other
players pick their moves, the goal of the respective player is achieved.

$G_{\mathbb{O}}$ should not be viewed as a competitive game. Players are in
fact ignorant of each other and follow their own agendas blindly.

###  3.2 Winning strategies

######  Proposition 3.3.

There exists a strategy $\mathcal{S}_{\text{MIN}}$ winning for
$P_{\text{MIN}}$.

###### Proof.

Notice that, no matter how the players proceed, the resulting $\prec$ is
necessary a strict (not necessarily total) ordering of $[0,\dots,n)$.

To make sure the resulting $\prec$ is total, $P_{\text{MIN}}$ maintains a
countable queue of all elements of $[0,\dots,n)$.

Being presented with a chain $o=(a_{1},\dots,a_{m})\in\mathbb{O}$,
$P_{\text{MIN}}$ removes all $a_{i}$s from the queue. They then pick the first
element from the updated queue $a$ and extend $o$ to
$o^{\prime}=(a,a_{1},\dots,a_{m})$.

Notice that the above move guarantees that an eventual $\prec$ will not have a
minimum, as well. ∎

######  Proposition 3.4.

There exists a strategy $\mathcal{S}_{\text{IND}}$ winning for
$P_{\text{IND}}$.

###### Proof.

This essentially is a variant of a well-known theorem of Paris and Wilkie [14]
(adapted to $L_{S_{2}}$ in [16]). We refer the reader to the mentioned paper,
or any of [7, 12, 13]. ∎

To finish the proof of 2.3 it is enough to prove

######  Theorem 3.5.

There exists a strategy $\mathcal{S}_{\text{PHP}}$ winning for
$P_{\text{PHP}}$.

###  3.3 MIN trees

Current subsection presents suitable sufficient conditions for 3.5 to hold.
The whole next section is devoted to proving such conditions.

######  Definition 3.6.

A smallest class of rooted labeled trees satisfying the following closure
properties is called the class of MIN $o$-trees with $o\in\mathbb{O}$

  * •

a single vertex $v$ labeled as $o$ is a MIN $o$-tree

  * •

for $a\in[0,\dots,n)$ not in $o$, a tree with root $v$ labeled as $o$ and
branching according to all possible extensions of $o$ to $o^{\prime}$ by a
single element $a$ and labeling each leaf by the corresponding extension
$o^{\prime}$ is a MIN $o$-tree

  * •

for a MIN $o$-tree with leaf $v$ labeled as $o^{\prime}$, replacing $v$ with
an arbitrary MIN $o^{\prime}$-tree gives a MIN $o$-tree

A depth of a tree is the maximum size of labels of the leaves. A tree is
uniform if all the leaves are labeled by chains of the same size.

We abuse the notation and at times view the tree as the corresponding set of
labels of leaves, i.e. the set of chains. A size of tree is the number of
chains in the mentioned set, equivalently the number of leaves.

The following proposition is a straightforward corollary of the definitions.

######  Proposition 3.7.

Let $T$ be MIN $o$-tree for $o\in\mathbb{O}$.

  1. 1.

$\forall o^{\prime}\neq o^{\prime\prime}\in T\>o^{\prime}\perp
o^{\prime\prime}$

  2. 2.

$\forall o^{\prime}\in\mathbb{O}\>(o^{\prime}\|o\to\exists o^{\prime\prime}\in
T\>o^{\prime\prime}\|o^{\prime})$

  3. 3.

if the depth of $T$ is $\leq d$, then size of $T$ is
$\leq\frac{(|o|+d)!}{(|o|)!}$ with equality achieved iff $T$ is uniform of
depth exactly $d$

Below is a suitable restatement of 2.2.

######  Theorem 3.8.

Let $\varphi(x,y)\in\Delta^{b}_{1}(\prec),\>p,h\in\mathbb{I}$ and
$o\in\mathbb{O}$. There exist uniform MIN $o$-trees $T_{a,b}$ for
$(a,b)\in[0,\cdots,p)\times[0,\cdots,h)$ of depths $\leq|n|^{c}$ for a
standard $c$ deciding the truth value of $\varphi(a,b)$ assuming the resulting
$\prec$ is a strict total ordering of $[0,\dots,n)$ extending $o$.

There are various ways how one can prove 3.8. Arguably the most natural one is
to define $T_{a,b}$ from the oracle queries a poly-time machine deciding the
truth value of $\varphi(a,b)$ makes to an oracle interpreting $\prec$. A
number of such queries is $\leq(|a|+|b|)^{c}$ for a standard constant $c$,
which can be upper bounded by $|n|^{c^{\prime}}$ for a suitable standard
$c^{\prime}\geq c$.

Since $\mathbb{M}$ models true arithmetic $Th(\mathbb{N})$, the above argument
can be made uniform in $a,b$ without any apparent complications.

For $T_{a,b}$ as above let $T^{+}_{a,b}$ be the set of chains of $T_{a,b}$
accepting $\varphi(a,b)$.

######  Definition 3.9.

Let $\varphi(x,y)\in\Delta^{b}_{1}(\prec),\>p,h\in\mathbb{I}$ and
$o\in\mathbb{O}$. We denote $A^{o}_{\varphi(x,y),p,h}$ the array of elements
of $\mathbb{O}$ indexed by $[0,\cdots,p)\times[0,\cdots,h)$ defined as
$A[a,b]=T^{+}_{a,b}$. We leave out sup/sub-scripts if they are clear from the
context.

######  Theorem 3.10.

Let $\varphi(x,y)\in\Delta^{b}_{1}(\prec),\>p,h\in\mathbb{I}$ and
$o\in\mathbb{O}$. Assume $A$ as above satisfies at least one of the following
properties

  * •

$\exists a\neq b<p\>\exists c<h\>(\exists o^{\prime}\in A[a,c]\>\exists
o^{\prime\prime}\in A[b,c]\>o^{\prime}\|o^{\prime\prime})$

  * •

$\exists a<p\>\exists b\neq c<h\>(\exists o^{\prime}\in A[a,b]\>\exists
o^{\prime\prime}\in A[a,c]\>o^{\prime}\|o^{\prime\prime})$

  * •

$\exists o^{\prime}\geq o\in\mathbb{O}\>\exists a<p\>\forall b<h\>(\forall
o^{\prime\prime}\in A[a,b]\>o^{\prime}\perp o^{\prime\prime})$

Then, there exists $o^{*}\in\mathbb{O}$ extending $o$ so that, assuming
$\prec$ is a total strict ordering of $[0,\dots,n)$ extending $o^{*}$,

$\displaystyle\mathbb{I}_{\prec}\vDash\text{PHP}^{p}_{h}(\varphi(x,y))$

###### Proof.

In case either of the first two bullets holds, let $o^{*}$ be
$o^{\prime}+o^{\prime\prime}$ with $+$ an arbitrary union of two compatible
chains into a single extension.

In case the third bullet holds, let $o^{*}$ be $o^{\prime}$. We claim that in
such case

$\displaystyle\mathbb{I}_{\prec}\vDash\exists a<p\>\forall
b<h\>(\neg\varphi(a,b))$

Clearly it is enough to show

$\displaystyle\mathbb{I}_{\prec}\vDash\forall b<h\>(\neg\varphi(a,b))$

with $a$ given by the third bullet which in turn is equivalent to

$\displaystyle\forall b<h\>\mathbb{I}_{\prec}\vDash\neg\varphi(a,b)$

For the sake of contradiction, assume there is $b<h$ and $\prec$ a total
strict ordering of $[0,\dots,n)$ extending $o^{*}$ so that

$\displaystyle\mathbb{I}_{\prec}\vDash\varphi(a,b)$

By 3.8 we can find $o^{\prime\prime}\in T^{+}_{a,b}$ so that $\prec$ extends
$o^{\prime\prime}$. This, however, implies $o^{\prime\prime}\in A[a,b]$ is
compatible with $o^{*}$, contradicting the assumption of the third bullet. ∎

At this point, the winning strategy $\mathcal{S}_{\text{PHP}}$ for
$P_{\text{PHP}}$ is clear: enumerate all $\Delta^{b}_{1}(\prec)$-formulas and
elements $p>h\in\mathbb{I}$ into countable queues. Then, being presented with
$o\in\mathbb{O}$, pick first $\varphi(x,y)$ and $p>h$ from respected queues.
Use Theorem 3.10, extend $o$ to $o^{*}$ and end the turn.

###  3.4 A note on Forcing

It is possible to view the construction presented in this paper as forcing.
For this, it suffices to define a notion of a generic object with a poset of
conditions being $\mathbb{O}$.

One then proves that any generic object interpreting $\prec$ does satisfy all
the conditions we seek. This, in turn, is achieved by density argument, i.e.
that each property we seek is forced by a dense set of conditions.

A more detailed presentation can be found in [13] with an application to a
rather similar problem as in the current paper.

More information on this type of forcing in bounded arithmetic can be found in
[7, 2, 11].

##  4 Combinatorial analysis

###  4.1 MIN arrays

Below is a definition adapted from [13, 12]. As it turns out, combinatorial
analysis is almost the same as in the case of PHP-arrays in [13].

######  Definition 4.1.

Let $o\in\mathbb{O}$ and $p,h\in\mathbb{I}$. Let $A\in\mathbb{M}$ be an array
indexed by $[0,\dots,p)\times[0,\dots,h)$ so that $A[a,b]\subset\mathbb{O}$.

We say $A$ is a MIN $(o,p,h)$-array if the following conditions are all
satisfied

  * •

$\forall a<p\>\forall b<h\>(\forall o^{\prime}\in A[a,b]\>o^{\prime}\geq o)$

  * •

$\forall a<p\>\forall b<h\>(\forall o^{\prime}\neq o^{\prime\prime}\in
A[a,b]\>o^{\prime}\perp o^{\prime\prime})$

  * •

$\forall a\neq b<p\>\forall c<h\>(\forall o^{\prime}\in A[a,c]\>\forall
o^{\prime\prime}\in A[b,c]\>o^{\prime}\perp o^{\prime\prime})$

  * •

$\forall a<p\>\forall b\neq c<h\>(\forall o^{\prime}\in A[a,b]\>\forall
o^{\prime\prime}\in A[a,c]\>o^{\prime}\perp o^{\prime\prime})$

  * •

$\forall o^{\prime}\geq o\in\mathbb{O}\>\forall a<p\>\exists b<h\>(\exists
o^{\prime\prime}\in A[a,b]\>o^{\prime}\|o^{\prime\prime})$

######  Remark.

Since $A\in\mathbb{M}$, it follows that there is a uniform standard constant
$c$ so that

$\displaystyle\forall a<p\>\forall b<h\>\forall o\in A[a,b]\>(|o|\leq|n|^{c})$

This follows from the overspill lemma [6, 6.1].

######  Corollary 4.2.

Let $\varphi(x,y)\in\Delta^{b}_{1}(\prec),\>p,h\in\mathbb{I}$ and
$o\in\mathbb{O}$. Assume $A^{o}_{\varphi(x,y),p,h}$ does not satisfy any of
the properties as in 3.10.

Then, $A^{o}_{\varphi(x,y),p,h}$ is a MIN $(o,p,h)$-array.

######  Definition 4.3.

Let $A$ be MIN $(o,p,h)$-array. We define the size of $A$ as

$\displaystyle\sum_{a<p,b<h}|A[a,b]|$

######  Proposition 4.4.

For $A$ a MIN $(o,p,h)$-array the size of $A$ equals

$\displaystyle\sum_{a<p}|\cup_{b<h}A[a,b]|=\sum_{b<h}|\cup_{a<p}A[a,b]|$

###### Proof.

Equalities follow directly from the fact that each two chains from two
different cells of the same row/column of $A$ are necessarily different. ∎

We denote $A[a,:]$ and $A[:,b]$ rows, resp. columns of $A$. We abuse the
notation and at times let $A[a,:]$ be $\cup_{b<h}A[a,b]$ and similarly for
$A[:,b]$.

Given two MIN $(o,p,h)$-arrays $A$ and $A^{\prime}$, we say $A^{\prime}$
extends $A$, iff for each $a,b$ and $o^{\prime}\in A^{\prime}[a,b]$, it holds
that $o^{\prime}\geq o$ for some $o\in A[a,b]$.

######  Theorem 4.5.

Let $A$ a MIN $(o,p,h)$-array. There exists a MIN $(o,p,h)$-array $A^{\prime}$
extending $A$ so that each $A^{\prime}[a,:]$ is a uniform MIN $o$-tree of
depth $d=|n|^{c}$ with $c$ a uniform standard constant.

###### Proof.

We adapt the proof of [13, Thm.4.11].

Let $d^{\prime}=|n|^{c^{\prime}}$ with $c^{\prime}$ a standard constant so
that each chain in $A$ is of size $\leq d^{\prime}$.

We construct $A^{\prime}$ by first creating $\leq(d^{\prime})^{2}$-deep MIN
$o$-trees for each row of $A$ simultaneously. We then describe how to
distribute chains of the trees among the cells of $A^{\prime}$ so that the
resulting structure satisfies the conditions we need.

Pick $a<p$. A tree $T_{a}$ is created by induction.

For $i=0$ let $o_{0}\geq o$ an arbitrary element of $A[a,:]$. Denote
$el(o_{0})$ elements of $o_{0}$ viewed as a set. We say that a MIN $o$-tree
$T$ captures $o_{0}$ relative to $o$ if leaves of $T$ are labeled by all
possible orderings of $el(o_{0})$ that extend $o$.

By a straightforward observation, one can show the existence of a uniform
$|o_{0}|$-deep MIN $o$-tree capturing $o_{0}$. Denote such tree $T_{0}$.

Given any $o^{\prime}\in T_{0}$ and $o^{\prime\prime}\in A[a,:]$, note that
$o^{\prime}\|o^{\prime\prime}$ implies $|el(o^{\prime})\cap
el(o^{\prime\prime})|\geq|o|+1$. This follows since $el(o^{\prime})=el(o_{0})$
and either $o^{\prime\prime}=o_{0}$, or $o^{\prime\prime}\perp o_{0}$ by the
properties of $A$.

For $i+1$ let $T_{i}$ MIN $o$-tree of depth $\leq id^{\prime}$ satisfying

$\displaystyle\forall o^{\prime}\in T_{i}\>\forall o^{\prime\prime}\in
A[a,:]\>(o^{\prime}\|o^{\prime\prime}\to|el(o^{\prime})\cap
el(o^{\prime\prime})|\geq|o|+i+1)$

For $i\geq d^{\prime}$ it follows

$\displaystyle\forall o^{\prime}\in T_{i}\>\forall o^{\prime\prime}\in
A[a,:]\>(o^{\prime}\|o^{\prime\prime}\to o^{\prime}\geq o^{\prime\prime})$

Otherwise, since any $o^{\prime}\in T_{i}$ is in $\mathbb{O}$, it follows
$\exists o_{o^{\prime}}\in A[a,:]$ such that $o^{\prime}\|o_{o^{\prime}}$.

Let $T_{i}^{o_{o^{\prime}}}$ be MIN $o^{\prime}$-tree of depth $\leq
d^{\prime}$ capturing $o_{o^{\prime}}$ relative to $o^{\prime}$.

Given any $o^{\prime\prime}\in T_{i}^{o_{o^{\prime}}}$ and
$o^{\prime\prime\prime}\in A[a,:]$, note that
$o^{\prime\prime}\|o^{\prime\prime\prime}$ implies $|el(o^{\prime\prime})\cap
el(o^{\prime\prime\prime})|\geq|o^{\prime}|+1$. This follows since
$el(o^{\prime\prime})=el(o_{o^{\prime}})$ and either
$o^{\prime\prime\prime}=o_{o^{\prime}}$, or $o^{\prime\prime\prime}\perp
o_{o^{\prime}}$ by properties of $A$.

Let $T_{i+1}$ be MIN $o$-tree of depth $\leq(i+1)d^{\prime}$ obtained by
extending each $o^{\prime}$ in $T_{i}$ by $T_{i}^{o_{o^{\prime}}}$. As we have
just shown, given $o^{\prime}\in T_{i+1}$ and $o^{\prime\prime}\in A[a,:]$,
assuming $o^{\prime}\|o^{\prime\prime}$ implies $|el(o^{\prime})\cap
el(o^{\prime\prime})|\geq|o|+(i+2)$.

In $d^{\prime}$-steps we get a MIN $o$-tree $T_{a}$ of depth
$\leq(d^{\prime})^{2}$ satisfying

$\displaystyle\forall o^{\prime}\in T_{a}\>\forall o^{\prime\prime}\in
A[a,:]\>(o^{\prime}\|o^{\prime\prime}\to o^{\prime}\geq o^{\prime\prime})$ (1)

Extend $T_{a}$ to a uniform $(d^{\prime})^{2}$-depth MIN $o$-tree also denoted
$T_{a}$ arbitrarily. Note that the above condition (1) is still preserved.

Finally, for $b<h$ define $A^{\prime}[a,b]$ as containing such chains of
$T_{a}$ which extend some chains of $A[a,b]$. Since $A$ is a MIN
$(o,p,h)$-array, each chain of $T_{a}$ extends exactly one chain of $T_{a}$.

Let’s verify that $A^{\prime}$ is a MIN $(o,p,h)$-array.

$\displaystyle\forall a<p\>\forall b<h\>(\forall o^{\prime}\in
A^{\prime}[a,b]\>o^{\prime}\geq o)$

holds since each chain of $T_{a}$ extends $o$.

$\displaystyle\forall a<p\>\forall b<h\>(\forall o^{\prime}\neq
o^{\prime\prime}\in A^{\prime}[a,b]\>o^{\prime}\perp o^{\prime\prime})$

holds since any two different chains of $T_{a}$ are pairwise incompatible.

$\displaystyle\forall a\neq b<p\>\forall c<h\>(\forall o^{\prime}\in
A[a,c]\>\forall o^{\prime\prime}\in A^{\prime}[b,c]\>o^{\prime}\perp
o^{\prime\prime})$

holds since $o^{\prime}$ extends a chain of $A[a,c]$ and $o^{\prime\prime}$ a
chain of $A[b,c]$ which themselves were incompatible originally.

$\displaystyle\forall a<p\>\forall b\neq c<h\>(\forall o^{\prime}\in
A[a,b]\>\forall o^{\prime\prime}\in A[a,c]\>o^{\prime}\perp o^{\prime\prime})$

holds since $o^{\prime}$ extends a chain of $A[a,b]$ and $o^{\prime\prime}$ a
chain of $A[a,c]$ which themselves were incompatible originally.

$\displaystyle\forall o^{\prime}\geq o\in\mathbb{O}\>\forall a<p\>\exists
b<h\>(\exists o^{\prime\prime}\in A[a,b]\>o^{\prime}\|o^{\prime\prime}))$

holds since $T_{a}$ is a MIN $o$-tree.

Let $d$ be $(d^{\prime})^{2}=|n|^{2c^{\prime}}$ and $c=2c^{\prime}$ a standard
constant. ∎

######  Corollary 4.6.

A min $(o,p,h)$-array $A$ is extendable to a MIN $(o,p,h)$-array $A^{\prime}$
of size exactly

$\displaystyle p\frac{(|o|+d)!}{(|o|)!}$

with $d=|n|^{c}$ for a standard $c$ being the size of each chain of
$A^{\prime}$.

Comparing with [13, 4.11] note that we are able to get the exact size instead
of a lower bound as in the case of PHP-trees.

######  Theorem 4.7.

Let $A$ a MIN $(o,p,h)$-array containing chains of size $\leq d$. The size of
$A$ is

$\displaystyle\leq h\frac{(|o|+d)!}{(|o|)!}$

###### Proof.

The proof is an adapted [13, 4.12] which itself bears resemblance to [5].

As a first step extend each chain to make it of size exactly $d$ arbitrarily.
Note that the resulting structure $A^{\prime}$ is no longer an
$(o,p,h)$-array, although the size defined as in 4.3 remains the same.

Each $A^{\prime}[:,b]$ is a set of pairwise incompatible chains each of size
exactly $d$. We claim

$\displaystyle|A^{\prime}[:,b]|\leq\frac{(|o|+d)!}{(|o|)!}$

There exists a number $m$ so that for each chain $o^{\prime}\in
A^{\prime}[:,b]$ it holds $el(o^{\prime})\subseteq[0,\dots,m)$.

There are exactly $\frac{(m)!}{(|o|)!}$ strict linear orderings of
$[0,\dots,m)$ extending $o$. Each $o^{\prime}\in A^{\prime}[:,b]$ is
extendable to exactly $\frac{(m)!}{(|o|+d)!}$ strict linear orderings of
$[0,\dots,m)$ extending $o$.

Any two such extensions of different $o^{\prime},o^{\prime\prime}\in
A^{\prime}[:,b]$ are necessarily different, since $o^{\prime}\perp
o^{\prime\prime}$. Upper bound then follows directly. ∎

######  Corollary 4.8.

Let $A$ a MIN $(o,p,h)$-array. Then, $p\leq h$.

###### Proof.

Extend $A$ to $A^{\prime}$ as in 4.6. The size of $A^{\prime}$ is exactly
$p\frac{(|o|+d)!}{(|o|)!}$ with $d$ being size of each chain of $A^{\prime}$.

By 4.7 the size of $A^{\prime}$ is $\leq h\frac{(|o|+d)!}{(|o|)!}$. Thus, we
derive $p\leq h$. ∎

Combining the above with 4.2 and 3.10 we finally derive that 3.5 holds, i.e.
there exists a strategy $\mathcal{S}_{\text{PHP}}$ winning for
$P_{\text{PHP}}$.

###  4.2 Densely ordered model

Model-theoretically, an interpretation of $\prec$ we have just constructed can
be strenghtened substantially. Namely, given a countable collection of large
enough subsets $X$ of $\mathbb{I}$, we can arrange that $\prec$ simultaneously
orders all of them densely, i.e. $(X,\prec)$ is a dense linear ordering. The
qualification large enough means that there is an injective mapping
$f\in\mathbb{M}$ that maps $[0,\dots,|n|^{d})$ into $X$, for some nonstandard
$d$.

$\text{DLO}(\prec|_{X})$ denotes the following formal expression:

$\displaystyle\forall a\in X\>(a\nprec a)$ $\displaystyle\land$
$\displaystyle\forall a\neq b\in X\>(a\prec b\lor b\prec a)$
$\displaystyle\land$ $\displaystyle\forall a,b,c\in X\>(a\nprec b\lor b\nprec
c\lor a\prec c)$ $\displaystyle\land$ $\displaystyle\forall a\in X\>\exists
b\neq a\in X\>(b\prec a)$ $\displaystyle\land$ $\displaystyle\forall a\in
X\>\exists b\in X\>(a\prec b)$ $\displaystyle\land$ $\displaystyle\forall
a\prec b\in X\>\exists c\in X\>(a\prec c\prec b)$

######  Theorem 4.9.

Assume that $\\{X_{i}\\}_{i\in\mathbb{N}}$ is a countable collection of
subsets of $\mathbb{I}$ such that for each $X\in\\{X_{i}\\}_{i\in\mathbb{N}}$
there exists an injective mapping $f\in\mathbb{M}$ that maps
$[0,\dots,|n|^{d})$ into $X$, for some nonstandard $d$.

Then, there exists an expansion of $\mathbb{I}$ to a model of

$\displaystyle T^{1}_{2}(\prec)+\text{PHP}(\Delta^{b}_{1}(\prec))$

which moreover satisfies $\text{DLO}(\prec|_{X})$ for all
$X\in\\{X_{i}\\}_{i\in\mathbb{N}}$.

###### Proof.

Model is constructed in a very similar way to 2.3. The set $\mathbb{O}$ is
replaced by $\mathbb{O}^{\prime}$ consisting of arbitrary $|n|^{c}$-large
chains of elements of $\mathbb{I}$ with $c$ an arbitrary standard constant.

Players $P_{\text{IND}}$ and $P_{\text{PHP}}$ are defined analogously as
before and existence for their winning strategies is proven in the exact same
way.

For $\mathcal{S}_{\text{PHP}}$ note that computations of lower and upper
bounds on the sizes of MIN $(o,p,h)$-arrays were deliberately done in a way
avoiding ever using the fact that we were building an ordering on
$[0,\dots,n)$.

$P_{\text{MIN}}$ must, however, be changed.

We introduce a countable sequence of new players $P^{X}_{\text{DLO}}$ one for
each $X\in\\{X_{i}\\}_{i\in\mathbb{N}}$.

The game proceeds in a way so that $P_{\text{IND}},P_{\text{PHP}}$ and each
$P^{X}_{\text{DLO}}$ play infinitely often.

A winning strategy $\mathcal{S}^{X}_{\text{DLO}}$ is as follows.

Player $P^{X}_{\text{DLO}}$ maintains a countable queue of all elements of
$X$. For a chain $o=(a_{1},\dots,a_{m})\in\mathbb{O}^{\prime}$ let
$o^{\prime}=(a_{i_{1}},\dots,a_{i_{m}})\leq o$ a subchain containing numbers
from $X$. Being presented with such a chain $o$, $P^{X}_{\text{DLO}}$ first
removes elements of $o^{\prime}$ from the queue. They then pick first not yet
removed elements $b_{1},\dots,b_{m+1}$, extend $o^{\prime}$ to
$o^{\prime\prime}=(b_{1},a_{1},\dots,b_{m},a_{m},b_{m+1})$ and finally put
$o^{*}$ a common extension of $o$ and $o^{\prime\prime}$. ∎

##  5 Variants of the construction

At this point, a general recipe for building a model of
$T^{1}_{2}(\alpha)+\text{PHP}(\Delta^{b}_{1}(\alpha))$ where $\alpha$ witness
failure of some combinatorial principle $C$ can be summarized as follows

  1. 1.

Define a poset $\mathbb{P}_{C}$ to be used as a source of conditions for
building an interpretation of $\alpha$ so that the player $P_{C}$ aiming at
falsifying $C$ would have a winning strategy.

  2. 2.

Verify that $P_{\text{IND}}$ player would also have a winning strategy which
amounts to proving a theorem similar to the result of Paris and Wilkie [14]; a
general treatment of this type of problem in the forcing framework can be
found in [2].

  3. 3.

Finally, verify that the player $P_{\text{PHP}}$ also has a winning strategy;
this, in turn, is achieved by following the steps below

    1. (a)

Consider a $C$ $(c,p,h)$-array defined similarly as in 4.1; show that assuming
one cannot derive a winning strategy for $P_{\text{PHP}}$, such an array
exists for suitable parameters $c,p,h$.

    2. (b)

Define a suitable notion of a query tree as in 3.6 and use an argument similar
to 4.6 so as to extend given $C$ $(c,p,h)$-array to a one with rows being
leaves of the full query tree; use the structural properties of the defined
query tree to give lower bounds on size of the resulting $C$ $(c,p,h)$-array.

    3. (c)

Arguing similarly as in 4.7 derive upper bounds on the size of a set of
pairwise incompatible conditions of $\mathbb{P}_{C}$.

    4. (d)

Combining the above upper and lower bounds derive restrictions on the
dimensionality of any $C$ $(c,p,h)$-array contradicting (a).

The outlined approach, albeit in a slightly different language, was taken in
[13] separating principles $\text{WPHP}(\Delta^{b}_{1}(R))$ and $\forall m\leq
n^{\epsilon}\>\text{PHP}^{m+1}_{m}(\Delta^{b}_{1}(R))$ from
$\text{ontoPHP}^{n+1}_{n}(R)$ over $T^{1}_{2}(R)$.

In the following subsections, we sketch some more separations that can be
obtained using the developed machinery.

###  5.1 TOUR principle

######  Definition 5.1.

A tournament is a directed graph $(V,E)$ with exactly one directed edge
between any two nodes.

A set $X\subseteq V$ is said to be dominating, if for any vertex $w\in
V\setminus X$ there is a $v\in X$ so that $(v,w)\in E$.

A well-know fact is that a tournament on $n$ vertices contains a dominating
set of size $\leq|n|+1$ (see, e.g. [10, 2.5]).

Given binary relation $E$ the following formal statement expresses the
previous fact:

$\displaystyle\exists x\neq y<n\>(\neg E(x,y)\land\neg E(y,x))$
$\displaystyle\lor$ $\displaystyle\exists x\neq y<n\>(E(x,y)\land E(y,x))$
$\displaystyle\lor$ $\displaystyle\exists
X\subseteq[0,\dots,n)(|X|\leq|n|+1)\>\forall x<n\>\exists y<n\>(x\notin X\to
y\in X\land E(y,x))$

and is denoted as $\text{TOUR}(E)$ with $n$ implicit.

Sets $X$ quantified in the above expression are taken to be ones codable in
the ground model $\mathbb{M}$.

Following the recipe outlined at the beginning of this section we start with
defining $\mathbb{T}$ \- a set of $|n|^{c}$-large tournaments on subsets of
$[0,\dots,n)$. Ordering is taken to be the usual inclusion.

A rather simple argument establishes existence of a winning strategy for
$P_{\text{DOM}|_{X}}$ whose goal is to ensure that $X$ is not a dominating set
in the resulting tournament: given $t\in\mathbb{T}$, pick
$x\in[0,\dots,n)\setminus X$ and extend $t$ by adding $x$ with edges directed
from $x$ towards each element of $X$.

Notice that in the above argument, we have not really used the exact size
bound of $X$ being $|n|+1$. It is sufficient for $X$ to be of size
$\leq|n|^{c}$ for a standard $c$ similarly as in 4.2.

To make sure $E$ is indeed a tournament on the full $[0,\dots,n)$, we add an
additional player $P_{\text{TOUR}}$ who maintains a countable queue of
elements of $[0,\dots,n)$ not yet put into a tournament. Being presented with
$t$, $P_{\text{TOUR}}$ chooses the first member of the queue and puts it into
$t$ arbitrarily.

We skip the treatment of $P_{\text{IND}}$ since the proof is very much the
same as in [14].

The definition of TOUR $t$-trees is as one expects it to be: choosing an
element $x$ we branch according to all possible ways how one may extend
current $t$ by including $x$. It is then not too hard to see that the size of
a uniform TOUR $t$-tree of depth $d$ is exactly $2^{|t|}\cdot 2^{|t|+1}\dots
2^{|t|+d-1}$.

As in 4.7, one can prove that a size of a set of pairwise incompatible
conditions extending $t$ of sizes $d$ is upper bounded by $2^{|t|}\cdot
2^{|t|+1}\dots 2^{|t|+d-1}$, the same bound as in the previous paragraph.

Combining the above bounds we get a desired dimensionality restriction for any
TOUR $(t,p,h)$-array, namely that $p\leq h$.

###  5.2 Discrete ordering

######  Definition 5.2.

Strict total ordering $\prec$ is called discrete, if $\forall x\>\exists
y\>\forall z\>(x\prec z\to x\prec y\preceq z)$.

To build a model of $T^{1}_{2}(\prec)+\text{PHP}(\Delta^{b}_{1}(\prec))$ with
$\prec$ total linear ordering on $[0,\dots,n)$ with no endpoints which is
moreover discrete, we play the game $G_{\mathbb{O}}$ as in 3 with a single
change. After a player makes their move, the resulting ordering
$o=(a_{1},\dots,a_{m})$ “freezes”, meaning the next player, after receiving
$o$, is not allowed to extend $o$ by inserting elements between any $a_{i}$
and $a_{i+1}$.

This simple change guarantees that $\prec$ is discrete, while at the same
time, all the results of 4 are preserved.

To be more precise, each player $P$ now receives a chain $o\in\mathbb{O}$ and
is allowed to extend $o$ to $o^{\prime}\in\mathbb{O}$ with the property that
$\forall a\in o^{\prime}\setminus o$, either $a\prec b$ for all $b\in o$ or
$b\prec a$ for all $b\in o$. The set of all such elements of $\mathbb{O}$ is
denoted as $\mathbb{O}_{o}$. When restricting the game to $\mathbb{O}_{o}$ we
say $o$ is frozen.

The notion of frozen MIN $(o,p,h)$-array is defined as in 4.1, with the
additional restriction that all the elements of such an array are from
$\mathbb{O}_{o}$. The same applies to the notion of frozen MIN $o$-tree.

Viewing a frozen $o$ as a single element, one can directly apply 4.7 and 4.6,
namely that each frozen MIN $(o,p,h)$-array is extendable to a uniform frozen
MIN $(o,p,h)$-array implying the size lower-bound of $p(d+1)!$ for suitable
$d$, and that each set of pairwise incompatible elements of $\mathbb{O}_{o}$
of sizes $d$ has total size $\leq p(d+1)!$.

The dimensionality restriction $p\leq h$ follows directly.

Note that the definition of frozen MIN $(o,p,h)$-array treats $o$ slightly
differently than in 4.1. To be in line with the original definition, one
should consider MIN $(f,o,p,h)$-arrays (and similarly MIN $(f,o)$-trees) with
$f$ frozen and $o\in\mathbb{O}_{f}$.

The drawback of the above more general notion is that establishing lower and
upper size bounds of the adapted arrays seems to be harder. We leave a
combinatorial analysis of MIN $(f,o,p,h)$-arrays open.

###  5.3 dWPHP principle

######  Definition 5.3.

For a relation $R\subseteq[0,\dots,n)\times[0,\dots,2n)$ the dual weak
pigeonhole principle for $R$ is a statement that $R$ cannot be the graph of a
surjective function.

Formally, the above is expressed as

$\displaystyle\exists x<n\>\exists y\neq z<2n\>(R(x,y)\land R(x,z))$
$\displaystyle\lor$ $\displaystyle\exists x<n\>\forall y<2n\>\neg R(x,y)$
$\displaystyle\lor$ $\displaystyle\exists y<2n\>\forall x<n\>\neg R(x,y)$

and is denoted as dWPHP($R$) with $n$ implicit.

To build a model of $T^{1}_{2}(R)$ which violates dWPHP($R$) we play a game as
before with $\mathbb{D}$ a set of $|n|^{c}$-large graphs of partial functions
on $[0,\dots,n)\times[0,\dots,2n)$. Ordering on $\mathbb{D}$ is the usual
inclusion.

The player $P_{\text{dWPHP}}$ maintains a queue of elements of $[0,\dots,2n)$
which are not yet in the image and subsequently extends given $d\in\mathbb{D}$
by such elements. $P_{\text{dWPHP}}$ also makes sure the resulting function is
well defined, which is achieved by the same strategy as above.

A winning strategy for $P_{\text{IND}}$ again follows from [14].

Finally, a winning strategy for $P_{\text{PHP}}$ follows by combinatorial
analysis similar to [13]. There, we considered the bijective pigeonhole
principle, hence query trees (called PHP-trees in the article) allowed for
questions of two types: either choose a pigeon $p$ and ask for its hole $h$,
or choose a hole $h$ and ask for a corresponding pigeon $p$. In the current
context, we allow queries only of the first type, i.e. given $p$ pigeon, ask
for a hole $h$.

The size of $d$-uniform tree as above is exactly $(2n)^{d}$. On the other
hand, the upper bound on the size of a $d$-uniform set of pairwise
incompatible elements of $\mathbb{D}$ is also $(2n)^{d}$, hence the winning
strategy for $P_{\text{PHP}}$ follows.

###  5.4 Open problem

Consider the following formal expression with $\varphi(x,y)$ a
$\Delta^{b}_{1}(\prec)$-formula and $p>h$:

$\displaystyle\exists a\neq b<p\>\exists c<h\>(\varphi(a,b)\land\varphi(a,c))$
$\displaystyle\lor$ $\displaystyle\exists a<p\>\forall
b<h\>(\neg\varphi(a,b))$

The above is a variant of a pigeonhole principle apparently stronger than
$\text{PHP}^{p}_{h}(\varphi(x,y))$ defined before.

Let $\text{PHP}^{\prime}(\Delta^{b}_{1}(\prec))$ denote a set of instances of
the above formal expression for all $\varphi(x,y)\in\Delta^{b}_{1}(\prec)$ and
$p>h\in\mathbb{I}$.

It is open whether one can build a model of

$\displaystyle
T^{1}_{2}(\prec)+\text{PHP}^{\prime}(\Delta^{b}_{1}(\prec))+\exists
n\>\neg\text{MIN}(\prec)$

or even

$\displaystyle
T^{1}_{2}(\prec)+\text{PHP}^{\prime}(\Delta^{b}_{1}(\prec))+\text{DLO}(\prec|_{X})$

as in the previous section using the present method. The seeming difficulty is
that one needs to be able to derive lower bounds on the size of a modified
version of MIN $(o,p,h)$-array, modification being that chains of the same row
are now not necessarily incompatible, or even different.

## Acknowledgements

I want to thank my supervisor Jan Krajíček for numerous valuable suggestions
and help with writing the paper. My gratitude goes to Ondřej Ježil, who helped
to clear out different technical arguments, especially in the final section.
Finally, I would like to thank Moritz Müller, without his suggestions the
final section might not have appeared at all.

## References

  * [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.
  * [2] A. Atserias and M. Müller.  Partially definable forcing and bounded arithmetic.  Archive for Mathematical Logic, 54:1–33, 2015.
  * [3] S. R. Buss.  Bounded Arithmetic.  PhD thesis, Princeton University, 1985.
  * [4] M. Chiari and J. Krajíček.  Witnessing Functions in Bounded Arithmetic and Search Problems.  Journal of Symbolic Logic, 63(3):1095–1115, 1998.
  * [5] G. O. H. Katona.  A simple proof of the Erdös-Chao Ko-Rado Theorem.  Journal of Combinatorial Theory, Series B, 13(2):183 – 184, 1972.
  * [6] R. Kaye.  Models of Peano Arithmetic.  Oxford Logic Guides. Oxford Science Publications, Oxford, 1991.
  * [7] J. Krajíček.  Bounded Arithmetic, Propositional Logic and Complexity Theory.  Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge, 1995.
  * [8] J. Krajíček.  Proof Complexity.  Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge, 2019.
  * [9] J. Krajíček, P. Pudlák, 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.
  * [10] N. Megiddo and U. Vishkin.  On finding a minimum dominating set in a tournament.  Theoretical Computer Science, 61(2):307–316, 1988.
  * [11] M. Müller.  Typical forcings, NP search problems and an extension of a theorem of Riis.  Annals of Pure and Applied Logic, 172(4):102930, 2021.
  * [12] M. Narusevych.  Models of bounded arithmetic.  Master’s thesis, Charles University, Prague, 2022.
  * [13] M. Narusevych.  Models of bounded arithmetic and variants of pigeonhole principle, 2024.
  * [14] J. Paris and A. J. Wilkie.  Counting problems in bounded arithmetic.  pages 332 – 334, 1985.
  * [15] T. Pitassi, P. Beame, and R. Impagliazzo.  Exponential lower bounds for the pigeonhole principle.  Random Structures and Algorithms, 7:15 – 39, 1995.
  * [16] S. Riis.  Making infinite structures finite in models of second order bounded arithmetic.  Arithmetic, proof theory and computational complexity, pages 289–319, 1993.