# Models of Bounded Arithmetic and variants of Pigeonhole Principle

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

We give elementary proof that theory $T^{1}_{2}(R)$ augmented by the weak
pigeonhole principle for all $\Delta^{b}_{1}(R)$-definable relations does not
prove the bijective pigeonhole principle for $R$. This can be derived from
known more general results but our proof yields a model of $T^{1}_{2}(R)$ in
which $ontoPHP^{n+1}_{n}(R)$ fails for some nonstandard element $n$ while
$PHP^{m+1}_{m}$ holds for all $\Delta^{b}_{1}(R)$-definable relations and all
$m\leq n^{1-\epsilon}$, where $\epsilon>0$ is a fixed standard rational
parameter. This can be seen as a step towards solving an open question posed
by M. Ajtai in [2, Page 3].

##  1 Introduction

This paper studies first-order bounded arithmetic theories in a language
extended by an unspecified relation symbol $R$ (such theories are often called
relativized). The main theories we are to inspect all contain theory
$T^{1}_{2}(R)$, a subtheory of a theory $T_{2}(R)$, and are augmented by
instances of (variants of) the pigeonhole principle. Several separations among
bounded arithmetic theories and unprovability of various combinatorial
principles are known (see [7, Chapter 10]). What is not known is whether the
consecutive theories $T^{i}_{2}(R)$ and $T^{i+1}_{2}(R)$ (subtheories of
$T_{2}(R)$ with induction restricted to $\Sigma^{b}_{i}(R)$-formulas and
$\Sigma^{b}_{i+1}(R)$-formulas, respectively) can be separated by principles
of a fixed quantifier complexity independent of $i$. This problem relates to
the depth $d$ versus $d+1$ problem in proof complexity (see [8, Problem
14.3.2]). It is only known that if we weaken the theories by excluding the
smash function $x\\#y$ (the resulting theories are denoted $T^{i}_{1}(R)$)
such a separation is possible (see [5]).

We think that to make progress on this problem it may be useful to have stand-
alone and elementary proofs of various separation results that can be obtained
by more general methods aiming at a large variety of stronger theories. For
example, the random restriction method using the $PHP$ switching lemma [1]
applies to the whole theory $T_{2}(R)$ and in a sense blurs the distinction
between its fragments.

The main technical result is a new and elementary proof of the following
statement:

$\displaystyle T^{1}_{2}(R)+WPHP^{2m}_{m}(\Delta^{b}_{1}(R))\nvdash
ontoPHP^{n+1}_{n}(R),$ (1)

where $ontoPHP^{n+1}_{n}(R)$ denotes the bijective pigeonhole principle stated
for a binary relation symbol $R$ and $WPHP^{2m}_{m}(\Delta^{b}_{1}(R))$
denotes the weak pigeonhole principle stated for all
$\Delta^{b}_{1}(R)$-definable relations.

The qualification “elementary” means that the proof does not refer to any
general frameworks aiming at a larger class of theories or a too-strong method
aiming at stronger theories. For example, we can note that (1) can be shown
indirectly by the following argument. Firstly, it is known that $T_{2}(R)$
(and even $T^{2}_{2}(R)$) proves $WPHP^{2m}_{m}(R)$ (see [13]). This can be
used to derive $T_{2}(R)\vdash WPHP^{2m}_{m}(\Delta^{b}_{1}(R)))$ (the same is
true even for $T^{2}_{2}(R)$). Secondly, using the restrictions technique and
applying the already mentioned $PHP$ switching lemma one can show that
$T_{2}(R)\nvdash ontoPHP^{n+1}_{n}(R)$ (see [1], [9] and [14]). Combining
these results we can derive the mentioned statement. Another general method is
that of [10] which extends an original construction of [15]. The statement (1)
is then an instance of a more general theorem showing, in short, that over
$T^{1}_{2}(R)$ any $weak$ combinatorial principle cannot prove a $strong$ one
(see [10] for details).

Our method has the advantage that its simple variant can be used to construct
a model of:

$\displaystyle T^{1}_{2}(R)+\exists n(\forall m\leq
n^{1-\epsilon}PHP^{m+1}_{m}(\Delta^{b}_{1}(R))+\neg ontoPHP^{n+1}_{n}(R)),$
(2)

with $\epsilon>0$ being an arbitrarily small standard rational parameter.
Neither of the two mentioned general methods that can be used to prove (1)
seem to be modifiable to prove (2).

As mentioned in the abstract, (2) can be seen as a step towards an open
question posed by M. Ajtai in [2, Page 3]. The full problem can be stated as
follows.

######  Problem (M. Ajtai [2]).

Does the theory:

$\displaystyle T_{2}(R)+\forall m\leq
n/2(PHP_{m}^{m+1}(\Sigma_{\infty}^{b}(R)))$

prove $PHP_{n}^{n+1}(R)$?

##  2 Preliminaries

The family of theories we are studying in this paper are all sound
axiomatizations of true arithmetic over a first-order language denoted simply
as $L$. This language consists 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$, and binary relation $x<y$. The intended meanings of
$0,1,\lfloor\frac{x}{2}\rfloor,x+y,x\cdot y,x<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|}$.

The main theory for $L$ is the bounded arithmetic $T_{2}$ which is axiomatized
by a finite universal theory $BASIC$ together with the induction scheme for
all bounded formulas. Recall that a formula is said to be bounded if all
quantifiers occurring in it are of the form $\forall x<t$ or $\exists x<t$
with an $L$-term $t$ not containing $x$ (see [4] or [8] for a comprehensive
treatment of $T_{2}$ and its fragments).

To define theories $S^{1}_{2}$ and $T^{1}_{2}$ and $\Delta^{b}_{1}$-formulas
we need to recall the class $\Sigma^{b}_{1}$ of bounded $L$-formulas. These
are formulas formed from atomic ones using connectives, any sharply bounded
quantifiers, and bounded existential quantifiers at the front. The class
$\Pi^{b}_{1}$ is defined dually using bounded universal quantifiers. Sharply
bounded quantifiers are of the form $\forall x<|t|$ and $\exists x<|t|$ with
an $L$-term $t$ not containing $x$.

Theory $S^{1}_{2}$ extends the already mentioned $BASIC$ by the scheme of
polynomial induction $PIND$ of the form:

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

for all $\Sigma^{b}_{1}$-formulas, while $T^{1}_{2}$ has ordinary induction
$IND$ for all $\Sigma^{b}_{1}$-formulas. The induction formulas may contain,
as is usual, other free variables than the induction variable.

A $\Sigma^{b}_{1}$-formula $\phi(x)$ is said to be $\Delta^{b}_{1}$ in
$S^{1}_{2}$ iff there is a $\Pi^{b}_{1}$-formula $\psi(x)$ so that
$S^{1}_{2}\vdash\phi(x)\equiv\psi(x)$. We often leave out the reference “in
$S^{1}_{2}$” and consider it automatically included. It can be shown that
$\Delta^{b}_{1}$-definable sets on $\mathbb{N}$ are exactly those decidable by
polynomial-time algorithms [4, page 64, Theorem 2].

Already the weakest of the mentioned theories $S^{1}_{2}$ is strong enough to
talk about bounded sets or sequences, i.e. this theory is sequential (consult
[7, Lemma 5.1.5]).

This paper focuses on the unprovability of a particular combinatorial
statement in a relativized version of $T^{1}_{2}$ denoted as $T^{1}_{2}(R)$
(and in a particular extension of the mentioned theory). To obtain such a
theory we first expand the language $L$ by a single binary relation $R(x,y)$.
One can naturally define classes $\Sigma^{b}_{1}(R)$ and $\Pi^{b}_{1}(R)$.
$T^{1}_{2}(R)$ is axiomatized by $BASIC$ together with the induction scheme
for all $\Sigma^{b}_{1}(R)$-formulas. Theories $S^{1}_{2}(R),T_{2}(R)$ and the
class $\Delta^{b}_{1}(R)$ in $S^{1}_{2}(R)$ are defined analogously. Similarly
as before, one can show that $\Delta^{b}_{1}(R)$-definable sets on
$\mathbb{N}$ are exactly those decidable by polynomial time algorithms with
oracle access to $R$.

It is a well-known fact that the least number principle axiom scheme is
equivalent to induction when stated for all formulas. The same is true for
$\Sigma^{b}_{1}$-formulas, i.e. theories $LNP(\Sigma_{1}^{b})$ and $T^{1}_{2}$
are equivalent (see [7, Lemma 5.2.7]). The situation is the same in the
relativized case.

######  Definition 2.1.

For parameters $n,m$ we define $PHP^{n}_{m}(R)$ as a disjunction of the
following formulas:

  * •

$\exists a<n\>\forall b<m:\neg R(a,b)$,

  * •

$\exists a\neq a^{\prime}<n\>\exists b<m:R(a,b)\land R(a^{\prime},b)$,

  * •

$\exists a<n\>\exists b\neq b^{\prime}<m:R(a,b)\land R(a,b^{\prime})$.

We define $ontoPHP_{n}^{m}(R)$ as a disjunction of $PHP^{n}_{m}(R)$ with the
formula:

  * •

$\exists b<m\>\forall a<n:\neg R(a,b)$.

We denote $PHP^{2m}_{m}(R)$ as $WPHP^{2m}_{m}(R)$ for cosmetic reasons.
$PHP^{n}_{m}(\Delta^{b}_{1}(R))$ stands for a set of instances of the above
disjunction with $R$ substituted for all $\Delta^{b}_{1}(R)$-formulas. As
usual, those formulas may contain additional free variables than $a$ and $b$.
Similarly, we denote $PHP^{2m}_{m}(\Delta^{b}_{1}(R))$ as
$WPHP^{2m}_{m}(\Delta^{b}_{1}(R))$.

##  3 Forcing

We show the statement (1) by constructing a model of:

$\displaystyle T^{1}_{2}(R)+\forall mWPHP^{2m}_{m}(\Delta^{b}_{1}(R))+\exists
n\neg ontoPHP^{n+1}_{n}(R),$

employing forcing.

Forcing is a generic name for a class of methods and its various formal
variants for bounded arithmetic were developed, cf. [12, 1, 7, 3, 15, 10]. We
want to keep the presentation elementary and as self-contained as possible and
hence we do not refer to any of the general expositions. Our approach is
pretty much the same as the one in [12] or [15].

Throughout the following two sections, $\mathbb{M}$ is a countable non-
standard model of $Th(\mathbb{N})$ in the $L$-language, and $n$ is a non-
standard number from $\mathbb{M}$. We denote the set
$\\{m\in\mathbb{M}\>|\>m<n\\}$ as $[n]$.

We let $\mathbb{I}$ be a substructure of $\mathbb{M}$ with the domain $I$
defined as $\\{m\>|\>m<2^{|n|^{c}}\text{for some standard }c\\}$. $\mathbb{I}$
will eventually play the role of the universe of a structure where $R$ will be
suitably interpreted, although all the arguments through the following
sections are done inside $\mathbb{M}$. The main reason behind choosing such
$\mathbb{I}$ is that numbers of magnitude $2^{n}$ are absent from
$\mathbb{I}$, while they do exist in $\mathbb{M}$.

Since all the formulas representing various combinatorial principles discussed
in the previous section may contain free variables, whenever we mention
$L(R)$-formulas or $L(R)$-sentences in the current context we allow them to
contain parameters from $\mathbb{I}$.

######  Definition 3.1.

Let $\mathbb{P}$ be the set of all partial injective functions in $\mathbb{M}$
of size $\leq|n|^{c}$ for standard $c$ between the sets $[n+1]$ and $[n]$. We
call members of $\mathbb{P}$ conditions and we assume $\mathbb{P}$ is
partially ordered by inclusion. The relation $\sigma\supseteq\rho$ is also
denoted $\sigma\leq\rho$.

We say that $\sigma$ and $\tau$ from $\mathbb{P}$ are compatible (denoted
$\sigma\|\tau$), if there is $\delta\in\mathbb{P}$ so that $\delta\leq\sigma$
and $\delta\leq\tau$, otherwise $\sigma$ and $\tau$ are called incompatible
(denoted $\sigma\perp\tau$).

We say that a set $D\subseteq\mathbb{P}$ is $\mathbb{P}$-definable, if it is
definable in $(\mathbb{M},\mathbb{P})$, the expansion of $\mathbb{M}$ by
predicate for $\mathbb{P}$. We say that $D\subseteq\mathbb{P}$ is dense, if
for all $\sigma\in\mathbb{P}$ there is $\tau\in D$ so that $\tau\leq\sigma$.

Note that conditions $\sigma$ and $\tau$ are compatible iff
$\sigma\cup\tau\in\mathbb{P}$.

######  Definition 3.2.

A $G\subseteq\mathbb{P}$ is a filter, if all the conditions from $G$ are
pairwise compatible and for any $\sigma\in G$ and $\tau\in\mathbb{P}$ so that
$\tau\geq\sigma$ it holds that $\tau\in G$ (i.e. $G$ is upwards closed).

We say that a filter $G$ is generic if for any dense and
$\mathbb{P}$-definable $D$ it holds that $G\cap D\neq\emptyset$.

The following statement is well-known.

######  Proposition 3.3.

For any $\sigma\in\mathbb{P}$ there exists a generic filter $G$ containing
$\sigma$.

######  Proposition 3.4.

Let $G$ be any generic filter. Then $\bigcup G$ is a bijective function
between the sets $[n+1]$ and $[n]$. We will denote such function as $R_{G}$.

###### Proof.

It is clear that for any filter $F$ the set $\bigcup F$ is a partial injective
function between the sets $[n+1]$ and $[n]$. To show the totality of $R_{G}$
let $a\in[n+1]$ and let $D_{a}$ be the set of all conditions defined on $a$.
Such $D_{a}$ is dense and $\mathbb{P}$-definable and so $R_{G}$ is defined on
$a$. One then shows the surjectivity of $R_{G}$ in a similar way by
considering the set $D^{b}$ of all conditions having $b\in[n]$ in their range.
∎

For $R_{G}$ as above we denote the $L(R)$-structure with the domain
$\mathbb{I}$ where $R_{G}$ interprets $R$ as $(\mathbb{I},R_{G})$.

######  Definition 3.5.

Let $\sigma\in\mathbb{P}$ and $\phi$ be an $L(R)$-sentence. We say that
$\sigma$ forces $\phi$ or $\phi$ is forced by $\sigma$ (denoted as
$\sigma\Vdash\phi$) if for any generic filter $G$ containing $\sigma$ it holds
that $(\mathbb{I},R_{G})\vDash\phi$.

Note that if sigma forces $\phi$ and $\tau\leq\sigma$, then $\tau$ forces
$\phi$ too.

######  Corollary 3.6.

Any condition $\sigma$ (or, equivalently, the empty condition
$\sigma=\emptyset$) forces $\neg ontoPHP^{n+1}_{n}(R)$.

We now discuss the forcing of various types of formulas. What is needed for
the main results can be summarized as follows.

######  Theorem 3.7.

Let $\sigma\in\mathbb{P}$. Then the following holds:

  1. 1.

for $a\in[n+1]$ and $b\in[n]$ it holds that $\sigma\Vdash R(a,b)$ iff
$\\{(a,b)\\}\subseteq\sigma$;

  2. 2.

for $a\in[n+1]$ and $b\in[n]$ it holds that $\sigma\Vdash\neg R(a,b)$ iff
$\\{(a,b)\\}\perp\sigma$;

  3. 3.

for any two $L(R)$-sentences $\phi$ and $\theta$ it holds that
$\sigma\Vdash\phi\land\theta$ iff $\sigma\Vdash\phi$ and $\sigma\Vdash\theta$;

  4. 4.

for any $L(R)$-formula $\phi(x)$ it holds that $\sigma\Vdash\forall
x\>\phi(x)$ iff $\forall a\in\mathbb{I}\>:\>\sigma\Vdash\phi(a)$;

  5. 5.

for any sharply bounded $L(R)$-sentence $\phi$ it holds that
$\sigma\Vdash\neg\phi$ iff $\forall\tau\leq\sigma$ it holds that
$\tau\nVdash\phi$.

  6. 6.

for any two sharply bounded $L(R)$-sentences $\phi$ and $\theta$ it holds that
$\sigma$ forces $\phi\lor\theta$ if and only if
$\forall\tau\leq\sigma\>\exists\rho\leq\tau\>:\>\rho\Vdash\phi$ or
$\rho\Vdash\theta$;

  7. 7.

for sharply bounded formula $\phi(\overline{x})$ it holds that $\sigma$ forces
$\exists\overline{x}\>\phi(\overline{x})$ if and only if
$\forall\tau\leq\sigma\>\exists\rho\leq\tau\>\exists\overline{a}\in\mathbb{I}\>:\>\rho\Vdash\phi(\overline{a})$.

We split the proof of the above result into separate lemmas.

######  Definition 3.8.

We say that $L(R)$-sentences $\phi$ and $\theta$ are forcing-equivalent (or,
simply f-equivalent) if for any $\sigma\in\mathbb{P}$ it holds that
$\sigma\Vdash\phi$ iff $\sigma\Vdash\theta$.

Logical equivalence implies f-equivalence. So we may safely assume all the
$L(R)$-formulas we are discussing are in prenex normal forms. Furthermore,
evaluating all the $L$-subformulas and all the $L$-subterms in $\mathbb{M}$ of
some $L(R)$-sentence leads to an f-equivalent sentence and so we may further
assume that all the atomic subformulas are of the form $R(a,b)$ or $\neg
R(a,b)$ for some $a,b\in\mathbb{M}$ (actually in $\mathbb{I}$ since we allow
parameters from $\mathbb{I}$ only).

######  Lemma 3.9.

Let $\sigma\in\mathbb{P}$, $a\in[n+1]$ and $b\in[n]$. Then, $\sigma\Vdash
R(a,b)$ iff $\\{(a,b)\\}\subseteq\sigma$ and $\sigma\Vdash\neg R(a,b)$ iff
$\\{(a,b)\\}\perp\sigma$.

###### Proof.

Assuming $\\{(a,b)\\}\subseteq\sigma$ it is clear that $\sigma\Vdash R(a,b)$.
So assume that $\\{(a,b)\\}\nsubseteq\sigma$. We can extend $\sigma$ to $\tau$
so that $(a^{\prime},b)\in\tau$ or $(a,b^{\prime})\in\tau$ for $a^{\prime}\neq
a$ and $b^{\prime}\neq b$. Such $\tau$ forces $\neg R(a,b)$ implying
$\sigma\nVdash R(a,b)$.

The equivalence for $\neg R(a,b)$ is done similarly. ∎

######  Lemma 3.10.

Let $\sigma\in\mathbb{P}$. For any two $L(R)$-sentences $\phi$ and $\theta$ it
holds that $\sigma\Vdash\phi\land\theta$ iff $\sigma\Vdash\phi$ and
$\sigma\Vdash\theta$. For any $L(R)$-formula $\psi(x)$ it holds that
$\sigma\Vdash\forall x\psi(x)$ iff for all
$a\in\mathbb{I}:\sigma\Vdash\psi(a)$.

###### Proof.

Both equivalences follow immediately from a more general statement that
$\sigma\Vdash\bigwedge_{i}\phi_{i}$ iff $\forall i\>\sigma\Vdash\phi_{i}$. The
statement itself easily follows from the definitions. ∎

######  Lemma 3.11.

Let $\sigma\in\mathbb{P}$ and $\phi$ be a sharply bounded $L(R)$-sentence.
Then $\sigma\Vdash\neg\phi$ iff $\forall\tau\leq\sigma$ it holds that
$\tau\nVdash\phi$.

###### Proof.

The left-to-right direction is clear. Assume now that $\sigma\nVdash\neg\phi$.
The statement then follows from an auxiliary observation: given a structure
$(\mathbb{I},R_{G})$ satisfying $\phi$ one can find for a suitable standard
$c$ a $|n|^{c}$-large subset $\tau$ in $\mathbb{M}$ of $R_{G}$ which forces
$\phi$. This, in turn, can be established by induction on logical complexity
of $\phi$. Below we show a sketch of the proof.

For atomic or negated atomic $\phi$ the claim follows from 3.9. Cases for
conjunction and disjunction are shown in the exact same way as the ones for
sharply bounded quantifiers below.

Let $\phi$ be of the form $\forall x\leq|n|^{c}\>\psi(x)$. By induction
hypothesis we find $\tau_{x}$ for each $x\leq|n|^{c}$ so that
$\tau_{x}\Vdash\psi(x)$. Note that all $\tau_{x}$ are pairwise compatible and
so we can define $\tau=\bigcup_{x}\tau_{x}$ which satisfies
$|\tau|\leq|n|^{c^{\prime}}$ for a suitable $c^{\prime}$ and
$\tau\Vdash\forall x\leq|n|^{c}\psi(x)$.

Finally, let $\phi$ be of the form $\exists x\leq|n|^{c}\>\psi(x)$. Similarly
as above, we pick particular $x$ so that $\tau_{x}\Vdash\psi(x)$ and let
$\tau=\tau_{x}$. ∎

######  Lemma 3.12.

Let $\sigma\in\mathbb{P}$. For any two sharply bounded $L(R)$-sentences $\phi$
and $\theta$ it holds that $\sigma\Vdash\phi\lor\theta$ iff
$\forall\tau\leq\sigma\>\exists\rho\leq\tau\>:\>\rho\Vdash\phi$ or
$\rho\Vdash\theta$.

###### Proof.

Let $\sigma$ force $\phi\lor\theta$ and let $\tau\leq\sigma$. Assume for
contradiction that $\forall\rho\leq\tau$ $\rho\nVdash\phi$ and
$\rho\nVdash\theta$. Since both $\phi$ and $\theta$ are sharply bounded we use
Lemma 3.11 to derive $\tau\Vdash\neg\phi$ and $\tau\Vdash\neg\theta$ which is
equivalent to $\tau\Vdash\neg\phi\land\neg\theta$ by Lemma 3.10. This,
however, contradicts the fact that $\sigma\Vdash\phi\lor\theta$ and
$\tau\leq\sigma$.

Now assume $\sigma\nVdash\phi\lor\theta$. Note that Lemma 3.11 can be
formulated as $\pi\nVdash\psi$ iff $\exists\delta\leq\pi$ so that
$\delta\Vdash\neg\psi$ for $\psi$ a sharply bounded formula. Since
$\phi\lor\theta$ is sharply bounded, we can use the above statement to extend
$\sigma$ to $\tau$ so that $\tau\Vdash\neg\phi\land\neg\theta$. Such $\tau$
can not be extended to $\rho$ forcing $\phi$ or $\theta$. ∎

Before we prove the last part of Theorem 3.7 we state the following
proposition which is readily established by induction on logical complexity
together with the previously proved lemmas.

######  Proposition 3.13.

Let $\phi(\overline{x})$ be a sharply bounded formula. The set of all pairs
$(\sigma,\overline{c})$ so that $\sigma\Vdash\phi(\overline{c})$ is
$\mathbb{P}$-definable.

######  Lemma 3.14.

For any sharply bounded $L(R)$-formula $\phi(\overline{x})$ it holds that
$\sigma\Vdash\exists\overline{x}\psi(\overline{x})$ iff
$\forall\tau\leq\sigma\>\exists\rho\leq\tau\>\exists\overline{a}\in\mathbb{I}:\>\rho\Vdash\phi(\overline{a})$.

###### Proof.

Assume $\sigma\Vdash\exists\overline{x}\phi(\overline{x})$ and let
$\tau\leq\sigma$. Note that $\tau\Vdash\exists\overline{x}\phi(\overline{x})$,
too. Let $G$ be a generic filter containing $\tau$ such that it holds
$(\mathbb{I},R_{G})\vDash\exists\overline{x}\phi(\overline{x})$. We can then
find $\overline{a}$ so that $(\mathbb{I},R_{G})\vDash\phi(\overline{a})$ and
as in the proof of Lemma 3.11 we can take a $|n|^{c}$-large subset $\rho$ in
$\mathbb{M}$ of $R_{G}$ so that $\rho\leq\tau$ and
$\rho\Vdash\phi(\overline{a})$.

Conversely, assume
$\forall\tau\leq\sigma\>\exists\rho\leq\tau\>\exists\overline{a}\in\mathbb{I}:\>\rho\Vdash\phi(\overline{a})$.
Note that this means the set $D$ of all conditions $\rho$ for which there is
$\overline{a}$ so that $\rho\Vdash\phi(\overline{a})$ is dense relative to
$\sigma$, i.e. the density condition is satisfied for all $\tau$ extending
$\sigma$.

By Proposition 3.13 it follows that the set $D$ is also
$\mathbb{P}$-definable. Thus any generic filter $G$ containing $\sigma$ must
contain some condition $\rho$ forcing $\phi(\overline{a})$ for some
$\overline{a}$ proving $\sigma\Vdash\exists\overline{x}\phi(\overline{x})$.
The latter is true since any generic filter containing $\sigma$ must intersect
any $\mathbb{P}$-definable set $D$ which is dense relative to $\sigma$. This
can be shown by considering the set
$D^{\prime}=D\cup\\{\rho\>|\>\rho\perp\sigma\\}$ which is dense and
$\mathbb{P}$-definable and so for any generic $G$ there is some $\rho\in G\cap
D^{\prime}$. But if $G$ contains $\sigma$, such $\rho$ must be compatible with
$\sigma$ and so is necessary a member of $D$. ∎

The following theorem is a fundamental fact regarding $T^{1}_{2}(R)$ and
forcing construction. The first version of the theorem appeared in [12] for
closely related theory $I\exists_{1}(R)$ and its modification for
$T^{1}_{2}(R)$ was shown in [15]. We skip the proof, the reader can find
details in [7, pp. 273 - 274].

######  Theorem 3.15.

For any sharply bounded $L(R)$-sentence $\phi(x,\overline{y})$ it holds that:

$\displaystyle\emptyset\Vdash LNP(\exists\overline{y}\phi(x,\overline{y})).$

######  Corollary 3.16.

For any generic filter $G$ it holds that:

$\displaystyle(\mathbb{I},R_{G})\vDash T^{1}_{2}(R)+\exists n\neg
ontoPHP^{n+1}_{n}(R).$

##  4 WPHP-Arrays

This whole section is devoted to the proof of:

$\displaystyle\emptyset\Vdash WPHP^{2m}_{m}(\Delta^{b}_{1}(R)),$

where $m\in\mathbb{I}$.

The argument is as follows: assuming $\emptyset\nVdash
WPHP^{2m}_{m}(\phi(x,y))$ for a $\Delta^{b}_{1}(R)$-formula $\phi(x,y)$ we
construct a certain combinatorial structure. Then, by using two different
arguments we establish upper and lower bounds on the size of such structure
resulting in a contradiction, thus showing that $\emptyset\Vdash
WPHP^{2m}_{m}(\Delta^{b}_{1}(R))$.

The following concepts are defined in the ground model $\mathbb{M}$.

######  Definition 4.1.

Let $\sigma\in\mathbb{P}$ and $m,k\in\mathbb{M}$ with $k\leq|n|^{c}$ for
standard $c$. We define an $(m,k,\sigma)$-WPHP-array (or just
$A^{k}_{m,\sigma}$-array ) as an array $A$ indexed by $[2m]\times[m]$ so that
each entry is a set of conditions of sizes bounded from above by $k$ and
satisfying the following properties:

  1. 1.

$\forall a\neq a^{\prime}\in[2m]\>\forall b\neq
b^{\prime}\in[m]\>:\>A(a,b)\cap A(a^{\prime},b)=A(a,b)\cap
A(a,b^{\prime})=\emptyset$;

  2. 2.

$\forall a,a^{\prime}\in[2m]\>\forall b\in[m]\>\forall\tau\in
A(a,b)\>\forall\tau^{\prime}\in
A(a^{\prime},b)\>:\>\tau\neq\tau^{\prime}\to\tau\perp\tau^{\prime}$;

  3. 3.

$\forall a\in[2m]\>\forall b,b^{\prime}\in[m]\>\forall\tau\in
A(a,b)\>\forall\tau^{\prime}\in
A(a,b^{\prime})\>:\>\tau\neq\tau^{\prime}\to\tau\perp\tau^{\prime}$;

  4. 4.

$\forall\rho\leq\sigma\>\forall a\in[2m]\>\exists b\in[m]\>\exists\tau\in
A(a,b)\>:\>\tau\|\rho$.

We require that each $\tau\in A(a,b)$ is compatible with $\sigma$ and does not
intersect $\sigma$.

######  Proposition 4.2.

Let $A$ be $A^{k}_{m,\sigma}$-array . Define the size of $A$ as the number
$N=\sum_{a,b}|A(a,b)|$, where $|A(a,b)|$ is a number of conditions in
$A(a,b)$. Then:

$\displaystyle N=\sum_{a}|\bigcup_{b}A(a,b)|=\sum_{b}|\bigcup_{a}A(a,b)|.$

###### Proof.

This follows from the first property of $A_{m,\sigma}^{k}$-arrays. ∎

It is hard to compute non-trivial lower and upper bounds on the size of a
general $A^{k}_{m,\sigma}$-array $A$. The way to proceed is to create a
related array $A^{\prime}$ with nicer combinatorial properties.

######  Definition 4.3.

An $A^{k}_{m,\sigma}$-array $A$ is called $k^{\prime}$-uniform (or just
uniform in case $k^{\prime}=k$), if all the conditions from the set
$\bigcup_{a,b}A(a,b)$ are of the size $k^{\prime}$.

As we will show later, uniformity alone is enough to compute non-trivial upper
bounds on the size of a $A^{k}_{m,\sigma}$-array . However, it is not enough
to calculate meaningful lower bounds.

######  Definition 4.4.

Let $D\subseteq[n+1]$ and $R\subseteq[n]$. A PHP-tree over $D$ and $R$ is
defined inductively as follows:

  * •

a single node (a root) is a $PHP\text{-tree}$ over any $D$ and $R$;

  * •

for every $a\in D$ the following is a $PHP$-tree over $D$ and $R$:

    * –

at the root the tree branches according to all $b\in R$, labeling the
corresponding edge $(a,b)$;

    * –

at the end-point of the edge labeled by $(a,b)$ the tree continues as a
$PHP\text{-tree}$ over $D\setminus\\{a\\}$ and $R\setminus\\{b\\}$;

  * •

for every $b\in R$ the following is a $PHP\text{-tree}$ over $D$ and $R$:

    * –

at the root the tree branches according to all $a\in D$, labeling the
corresponding edge $(a,b)$;

    * –

at the end-point of the edge labeled by $(a,b)$ the tree continues as a
$PHP\text{-tree}$ over $D\setminus\\{a\\}$ and $R\setminus\\{b\\}$.

We further label each node of a $PHP\text{-tree}$ by the set of pairs labeling
edges leading to the given node from the root (the root itself is labeled as
$\emptyset$).

For $\sigma\in\mathbb{P}$ we define $PHP^{\sigma}\text{-tree}$ as a
$PHP\text{-tree}$ over $[n+1]\setminus D_{\sigma}$ and $[n]\setminus
R_{\sigma}$, where $D_{\sigma}$ is the domain of $\sigma$ and $R_{\sigma}$ is
the range of $\sigma$.

For $\sigma,\tau\in\mathbb{P}$ which are compatible we define
$PHP^{\sigma}_{\tau}\text{-tree}$ as a $PHP^{\sigma}\text{-tree}$ with the
property that for each $(a,b)\in\tau\setminus\sigma$ every leaf in the given
tree is labeled by a set either containing $(a,b)$ or containing
$(a^{\prime},b)$ and $(a,b^{\prime})$ for $a\neq a^{\prime}$ and $b\neq
b^{\prime}$.

We say that a $PHP\text{-tree}$ is $k$-uniform if all its maximal paths
(starting from the root) have the same length equal to $k$.

For a detailed discussion about $PHP$-trees and their applications consult [8,
Chapter 15.1].

Since each $\sigma\in\mathbb{P}$ is an element of $\mathbb{M}$ we can talk
about the size of $\sigma$ (denoted as $|\sigma|$) which may be non-standard.

######  Proposition 4.5.

Let $\sigma\in\mathbb{P}$ and $P$ a $k$-uniform
$PHP^{\sigma}\text{-tree}$-tree. The number of maximal paths (i.e. the number
of leaves) in $P$ is lower-bounded by $\frac{(n-|\sigma|)!}{(n-|\sigma|-k)!}$.

###### Proof.

The minimal number of paths is achieved for a $PHP^{\sigma}\text{-tree}$ with
nodes labeled by elements of the larger set (initially $[n+1]\setminus
D_{\sigma}$ of size $n+1-|\sigma|$) and branching according to elements from
the smaller set (initially $[n]\setminus R_{\sigma}$ which has size
$n-|\sigma|$). ∎

######  Definition 4.6.

We say that a set of conditions $T\in\mathbb{M}$ is realized by a PHP-tree if
there is a $PHP\text{-tree}$ $P$ so that $T$ equals the set of labels of
leaves of $P$. Similarly, we define realizations by
$PHP^{\sigma}\text{-tree}$, $PHP^{\sigma}_{\tau}\text{-tree}$ and uniform
versions of the previous notions.

######  Corollary 4.7.

If $T\in\mathbb{M}$ is realized by a $k$-uniform $PHP^{\sigma}\text{-tree}$,
then $|T|\geq\frac{(n-|\sigma|)!}{(n-|\sigma|-k)!}$.

######  Proposition 4.8.

Let $T\in\mathbb{M}$ be realized by a $PHP^{\sigma}\text{-tree}$. It then
holds:

  1. 1.

$\forall\tau,\tau^{\prime}\in
T\>:\>\tau\neq\tau^{\prime}\to\tau\perp\tau^{\prime}$;

  2. 2.

$\forall\rho\leq\sigma\>\exists\tau\in T\>:\>\tau\|\rho$.

###### Proof.

The first property follows from the fact that any two labelings of the leaves
in any $PHP\text{-tree}$ are incompatible. The second property follows from
the definitions. ∎

We now state a lemma which allows us to glue together various $PHP$-trees to
get a bigger one. The idea is rather simple, every $PHP\text{-tree}$ can be
extended to a deeper one by simply appending another $PHP\text{-tree}$ to a
leaf in the original tree, assuming that the tree we are inserting is
compatible with the path leading to such a leaf. Of course, one needs to
ensure that the tree we get is definable in $\mathbb{M}$. An immediate
corollary is that every $PHP\text{-tree}$ can be extended to a $k$-uniform one
for a suitable $k$.

######  Lemma 4.9.

Let $P$ be a $PHP^{\sigma}_{\tau}\text{-tree}$. Let
$(S_{\lambda})_{\lambda}\in\mathbb{M}$ a collection of $PHP$-trees where
$\lambda$ ranges over all labels of the leaves of $P$. For any such $\lambda$
we assume $S_{\lambda}$ is a $PHP^{\sigma\cup\lambda}\text{-tree}$.

We define a tree $P\triangleleft S$ as an extension of $P$ by
$(S_{\lambda})_{\lambda}$ where we append $S_{\lambda}$ to the leaf of $P$
labeled by $\lambda$. It

Then, $P\triangleleft S$ is a $PHP^{\sigma}_{\tau}\text{-tree}$ with the
property that each maximal path of $P\triangleleft S$ extends a unique maximal
path of $P$.

###### Proof.

$P\triangleleft S$ is definable in $\mathbb{M}$, since both $P$ and
$(S_{\lambda})_{\lambda}$ are in $\mathbb{M}$.

The fact that each $S_{\lambda}$ is a $PHP^{\sigma\cup\lambda}\text{-tree}$
implies $P\triangleleft S$ is a $PHP\text{-tree}$.

Since $P$ is a $PHP\text{-tree}$ over $[n+1]\setminus D_{\sigma}$ and
$[n]\setminus R_{\sigma}$ and $S_{\lambda}$ is a $PHP\text{-tree}$ over
$[n+1]\setminus D_{\sigma\cup\lambda}$ and $[n]\setminus
R_{\sigma\cup\lambda}$ it follows that $P\triangleleft S$ is $PHP\text{-tree}$
over $[n+1]\setminus D_{\sigma}$ and $[n]\setminus R_{\sigma}$ and thus is a
$PHP^{\sigma}\text{-tree}$.

Each maximal path of $P\triangleleft S$ extends a unique maximal path of $P$
by the definition of extension.

Finally, since any label $\pi\in\mathbb{P}$ of a leaf of $P\triangleleft S$ is
a superset of the label of a leaf of $P$ it follows that $\pi$ does contain
$(a,b)$ or $(a^{\prime},b)$ and $(a,b^{\prime})$ with $a\neq a^{\prime}$ and
$b\neq b^{\prime}$ for all $(a,b)\in\tau\setminus\sigma$. This implies
$P\triangleleft S$ is a $PHP^{\sigma}_{\tau}\text{-tree}$. ∎

In general, one can consider appending $PHP$-trees to leaves of another
$PHP\text{-tree}$ the above assumptions, namely that each $S_{\lambda}$ is a
$PHP^{\lambda}\text{-tree}$ (we are ignoring the initial condition $\sigma$
here). In such a case one needs to ensure that the resulting tree is a
$PHP\text{-tree}$ by first removing all branches of $S_{\lambda}$ which are
incompatible with $\lambda$. We then shrink all nodes of the resulting tree
which have only a single edge going outwards.

In the above Lemma 4.9 we overcome this complication by assuming that
$S_{\lambda}$ already takes into account the label of the leaf it is being
appended to which is formally expressed as $S_{\lambda}$ being a
$PHP^{\lambda}\text{-tree}$.

When $P^{\prime}$ is a tree obtained from a tree $P$ by the above process of
appending trees to leaves we say that $P^{\prime}$ extends $P$.

######  Corollary 4.10.

For every $k^{\prime}\geq k\in\mathbb{M}$ with $k^{\prime}\leq n+1$ a
$PHP^{\sigma}_{\tau}\text{-tree}$ of depth $k$ can be extended to a
$k^{\prime}$-uniform $PHP^{\sigma}_{\tau}\text{-tree}$.

In the next theorem, we identify $PHP$-trees with the labelings of their
leaves or, in other words, with the labelings of their maximal paths.

######  Theorem 4.11.

Let $A$ be an $A^{k}_{m,\sigma}$-array for $\sigma\in\mathbb{P}$. There exists
$k^{\prime}\geq k$ enjoying $k^{\prime}\leq|n|^{c}$ for a suitable standard
$c$ and a $k^{\prime}$-uniform $A^{k^{\prime}}_{m,\sigma}$-array of size
$N\geq 2m\cdot\frac{(n-|\sigma|)!}{(n-|\sigma|-k^{\prime})!}$.

###### Proof.

We construct an $A^{k^{\prime}}_{m,\sigma}$-array $A^{\prime}$ in two stages.
Firstly, we specify the contents of each row. Then, we specify how to
distribute created content among the columns so that the result is an
$A^{k^{\prime}}_{m,\sigma}$-array .

Let $A_{a}$ be $\bigcup_{b}A(a,b)$ for $a\in[2m]$. We construct
$A^{\prime}_{a}$ (i.e. the contents of the $a$-th row of $A^{\prime}$) by the
following procedure which takes $k$ steps.

At first, pick $\tau\in A_{a}$. Note that $\tau\cap\sigma=\emptyset$ and
$|\tau|\leq k$, implying existence of a $PHP^{\sigma}_{\tau}\text{-tree}$ of
depth $\leq 2k$. Extend such a tree to a uniform $PHP^{\sigma}\text{-tree}$
$P_{1}$ of depth exactly $2k$ which is achieved utilizing Corollary 4.10.

Note that $P_{1}$ satisfies the following properties:

  * •

$\forall\rho\in P_{1}\>\exists\pi\in A_{a}\>:\>\pi\|\rho$;

  * •

$\forall\rho\in P_{1}\>\forall\pi\in A_{a}\>:\>\pi\|\rho\to|\pi\cap\rho|\geq
1$.

The first property follows from the fact that $A$ is an
$A^{k}_{m,\sigma}$-array and any $\rho$ from $P_{1}$ is compatible with
$\sigma$.

The second property is proved by cases. Assuming $\pi=\tau$ it follows that
$\pi||\rho\to\pi\geq\rho$ and so $|\pi\cap\rho|=|\pi|\geq 1$. So let
$\pi\neq\tau$. In such a case it follows that $\pi\perp\tau$ and so must
contain a pair $(a,b)$ such that $\tau$ contains either $(a^{\prime},b)$ or
$(a,b^{\prime})$ for $a\neq a^{\prime}$ and $b\neq b^{\prime}$. In any case a
branch $\rho$ of $P_{1}$ compatible with $\pi$ must also contain $(a,b)$,
proving $|\pi\cap\rho|\geq|\\{(a,b)\\}|=1$. This finishes the first step of
the construction.

At the $i$-th step we are given a uniform $PHP^{\sigma}\text{-tree}$ $P_{i-1}$
of depth $2(i-1)k$ satisfying the following properties:

  * •

$\forall\rho\in P_{i-1}\>\exists\pi\in A_{a}\>:\>\pi\|\rho$;

  * •

$\forall\rho\in P_{i-1}\>\forall\pi\in
A_{a}\>:\>(\pi\|\rho\land|\pi|\geq(i-1))\to|\pi\cap\rho|\geq(i-1)$.

Using the first property of $P_{i-1}$ pick $\pi_{\rho}\in A_{a}$ for each
$\rho\in P_{i-1}$ so that $\pi_{\rho}\|\rho$. For such $\pi_{\rho}$ create a
$PHP^{\sigma\cup\rho}_{\pi_{\rho}}\text{-tree}$ of depth $\leq 2k$ and extend
it to a $2k$-uniform $PHP^{\sigma\cup\rho}\text{-tree}$ $P_{i}^{\rho}$.

Let $P_{i}$ be $P_{i-1}\triangleleft\\{P_{i}^{\rho}\>|\>\rho\in P_{i-1}\\}$.
By Lemma 4.9 we see that $P_{i}$ is a $2(i\cdot k)$-uniform
$PHP^{\sigma}\text{-tree}$.

Clearly:

  * •

$\forall\rho\in P_{i}\>\exists\pi\in A_{a}\>:\>\pi\|\rho$.

To prove the second desired property let $\rho\in P_{i}$ and $\pi\in A_{a}$ so
that $\pi\|\rho$ and $|\pi|\geq i$. Let $\rho_{*}$ be the unique maximal path
of $P_{i-1}$ so that $\rho_{*}\geq\rho$. Note that $\pi\|\rho_{*}$ and so
$|\pi\cap\rho|\geq|\pi\cap\rho_{*}|\geq(i-1)$. Assume $|\pi\cap\rho_{*}|=i-1$.
Let $\pi_{\rho_{*}}\in A_{a}$ be the condition chosen to create
$P_{i}^{\rho_{*}}$.

In case $\pi_{\rho_{*}}=\pi$ it follows that $|\pi\cap\rho|=|\pi|\geq i$. So
assume $\pi\neq\pi_{\rho_{*}}$. Then, $\pi\perp\pi_{\rho_{*}}$. But since both
$\pi$ and $\pi_{\rho_{*}}$ are compatible with $\rho_{*}$ it follows that
$(\pi\setminus\rho_{*})\perp(\pi_{\rho_{*}}\setminus\rho_{*})$ and so
$|(\pi\setminus\rho_{*})\cap(\rho\setminus\rho_{*})|\geq 1$, implying
$|\pi\cap\rho|\geq i$.

So, after the end of the $k$-th step we get a $2k^{2}$-uniform
$PHP^{\sigma}\text{-tree}$ $P_{k}$ satisfying the following properties:

  * •

$\forall\rho\in P_{k}\>\exists\pi\in A_{a}\>:\>\pi\|\rho$;

  * •

$\forall\rho\in P_{k}\>\forall\pi\in A_{a}\>:\>\pi\|\rho\to\pi\geq\rho$.

By Corollary 4.7 the number of leaves of $P_{k}$ is bounded from below by
$\frac{(n-|\sigma|)!}{(n-|\sigma|-2k^{2})!}$.

Note that each $\rho\in P_{k}$ is compatible with $\sigma$ and does not
intersect it. Furthermore, by Proposition 4.8 any two different $\rho$ and
$\rho^{\prime}$ from $P_{k}$ are incompatible, and for any $\pi\leq\sigma$
there is a $\rho\in P_{k}$ compatible with it. This implies, assuming the
contents of each row of $A^{\prime}$ are created by the process described
above, the resulting $A^{\prime}$ satisfies all of the properties of uniform
$A^{2k^{2}}_{m,\sigma}$-array , assuming the content of each row is correctly
distributed among the columns to satisfy property 3 of (4.1).

The distribution proceeds as follows: for any $\rho\in P_{k}$ pick $\tau\in
A_{a}$ so that $\rho\leq\tau$. Note that such $\tau$ is unique and is uniquely
placed into one of the columns of $A$. Let $b\in[m]$ so that $\tau\in A(a,b)$.
Put $\rho$ into $A^{\prime}(a,b)$.

The above gives us a well-defined array $A^{\prime}$ which, as we have already
seen, satisfies all of the properties of the (4.1) up to the third one.

Let $b,b^{\prime}\in[m]$ be different and let $\tau\in
A^{\prime}(a,b),\tau^{\prime}\in A^{\prime}(a,b^{\prime})$. Let $\pi$ and
$\pi^{\prime}$ be conditions from $A(a,b)$ and $A(a,b^{\prime})$,
respectively, so that $\tau\leq\pi$ and $\tau^{\prime}\leq\pi^{\prime}$. Since
$\pi\perp\pi^{\prime}$ it follows that $\tau\perp\tau^{\prime}$. This shows
that the third property is satisfied, as well.

Finally, by Proposition 4.2 the size of the array $A^{\prime}$ is bounded from
below by

$\displaystyle 2m\cdot\min_{a}|\bigcup_{b}A^{\prime}(a,b)|\geq
2m\cdot\frac{(n-|\sigma|)!}{(n-|\sigma|-2k^{2})}!$

with the inequality following from the fact that all the rows of $A^{\prime}$
are $2k^{2}$-uniform $PHP^{\sigma}$-trees. ∎

By a slightly more careful construction, one can get $k^{\prime}$ from the
above proof to be equal to $k^{2}+k$ instead of $2k^{2}$. This, however, does
not make a major difference.

######  Theorem 4.12.

Let $A$ be a $k$-uniform $A^{k}_{m,\sigma}$-array for $\sigma\in\mathbb{P}$.
Then, the size of $A$ is bounded from above by
$m\cdot\frac{(n+1-|\sigma|)!}{(n+1-|\sigma|-k)!}$.

###### Proof.

The proof is reminiscent of the famous Erdős–Ko–Rado theorem as in [6]. By
Proposition 4.2 we know that the size of $A$ is bounded from above by
$m\cdot\max_{b}|\bigcup_{a}A(a,b)|$.

Let $A^{b}$ denote $\bigcup_{a}A(a,b)$. In particular, each $\tau\in A^{b}$ is
of size $k$ and different $\tau,\tau^{\prime}\in A^{b}$ are incompatible.

We view each $\tau$ as a $k$-large matching of the
$K_{n+1-|\sigma|,n-|\sigma|}$ (a complete bipartite graph with partitions of
sizes $n+1-|\sigma|$ and $n-|\sigma|$). We will now prove that for any
$k,c,d\in\mathbb{M}$ enjoying $k\leq c\leq d$ it holds that the size of any
family $\mathfrak{M}$ of pairwise-incompatible $k$-large matchings (i.e. union
of any two matchings of $\mathfrak{M}$ is not a matching) of $K_{d,c}$ is
bounded from above by $\frac{d!}{(d-k)!}$.

Note that any two different submatchings of some fixed $c$-large matching $M$
of $K_{d,c}$ are compatible and so $\mathfrak{M}$ can contain at most one
submatching of such $M$. There are $k!\binom{d}{k}\binom{c}{k}$ different
$k$-large matchings of $K_{d,c}$ and each such matching can be extended to
$(c-k)!\binom{d-k}{c-k}$ different $c$-large matchings of $K_{d,c}$. Any two
$c$-large matchings extending different $k$-large matchings from
$\mathfrak{M}$ must necessarily be incompatible and, in particular, different.

It follows that:

$\displaystyle|\mathfrak{M}|\leq
c!\binom{d}{c}\cdot\frac{1}{(c-k)!\binom{d-k}{c-k}}=\frac{d!}{(d-k)!}.$

∎

######  Corollary 4.13.

For any $\sigma\in\mathbb{P},m\in\mathbb{M}$ and $k\leq|n|^{c}$ for standard
$c$ there does not exist a $A^{k}_{m,\sigma}$-array .

###### Proof.

Assume $A$ is a $A^{k}_{m,\sigma}$-array . By Theorem 4.11 we can assume it is
$k$-uniform and has size $N\geq 2m\cdot\frac{(n-|\sigma|)!}{(n-|\sigma|-k)!}$.

By Theorem 4.12 it follows that $N\leq
m\cdot\frac{(n+1-|\sigma|)!}{(n+1-|\sigma|-k)!}$.

Combining both lower and upper bounds we derive:

$\displaystyle 2\leq\frac{n+1-|\sigma|}{n+1-|\sigma|-k},$

which is a contradiction, since both $|\sigma|$ and $k$ are bounded by
$|n|^{c^{\prime}}$ for a suitable standard $c$. ∎

To get the desired contradiction assuming that $(\mathbb{I},R_{G})\nvDash
WPHP^{2m}_{m}(\Delta^{b}_{1}(R))$ we prove the following and key theorem.

######  Theorem 4.14.

Assume $\emptyset\nVdash WPHP^{2m}_{m}(\Delta^{b}_{1}(R))$ for
$m\in\mathbb{I}$. Then, there exists an $A^{k}_{m,\sigma}$-array for some
$\sigma\in\mathbb{P}$ and $k\leq|n|^{c}$ for a suitable standard $c$.

###### Proof.

Let $\phi(x,y)$ be $\Delta^{b}_{1}(R)$-formula with parameters from
$\mathbb{I}$ so that $\emptyset$ does not force $WPHP_{m}^{2m}(\phi(x,y))$.

Let $D\subseteq\mathbb{P}$ contain such $\rho\in\mathbb{P}$ that one of the
below holds:

  * •

$\exists a\neq a^{\prime}\in[2m]\>\exists
b\in[m]\>:\>\rho\Vdash\phi(a,b)\land\phi(a^{\prime},b)$;

  * •

$\exists a\in[2m]\>\exists b\neq
b^{\prime}\in[m]\>:\>\rho\Vdash\phi(a,b)\land\phi(a,b^{\prime})$;

  * •

$\exists a\in[2m]\>\forall b\in[m]\>:\>\rho\Vdash\neg\phi(a,b)$.

We want to show that $D$ is $\mathbb{P}$-definable. Since $\phi(x,y)$ is a
$\Delta^{b}_{1}(R)$-formula and $\Delta^{b}_{1}(R)\subseteq\Sigma^{b}_{1}(R)$
we can assume $\phi(x,y)$ is of the form:

$\displaystyle\exists\overline{u}\leq t(x,y)\>\psi(x,y,\overline{u}),$

where $t$ is an $L$-term with parameters from $\mathbb{I}$ and
$\psi(x,y,\overline{u})$ is sharply bounded. It is now enough to use Theorem
3.7 to show $\mathbb{P}$-definability of $D$ by writing it as a union of three
sets, one for each condition defining $D$, and then applying different parts
of (3.7) depending on the structure of $\phi(x,y)$.

As an example, we show that the set of all conditions forcing $\phi(a,b)$ for
particular $a,b\in\mathbb{I}$ is $\mathbb{P}$-definable. By (3.7, 7) we get:

$\displaystyle\rho\Vdash\exists\overline{u}\leq
t(a,b)\>\psi(a,b,\overline{u})$

iff

$\displaystyle\forall\tau\leq\rho\>\exists\pi\leq\tau\>\exists\overline{u}\leq
t(a,b)\>:\>\pi\Vdash\psi(a,b,\overline{u}).$

So it is enough to show $\mathbb{P}$-definability of the set of all conditions
$\pi$ forcing $\psi(a,b,\overline{u})$. This follows immediately from
Proposition 3.13.

It is clear that any condition in $D$ forces $WPHP^{2m}_{m}(\phi(x,y))$. Thus,
according to the assumptions, $D$ is not dense. Let $\sigma\in\mathbb{P}$ be a
condition not extendable to any condition from $D$.

As a next step, we define an array $A\in\mathbb{M}$ which should satisfy the
properties of the $A^{|n|^{c}}_{m,\sigma}$-array for a standard $c$. We start
by writing the formula $\phi(x,y)$ as $\phi^{\prime}(x,y,\overline{c})$ so
that $\overline{c}\in\mathbb{I}$ and $\phi^{\prime}(x,y,\overline{z})$ is a
$\Delta^{b}_{1}(R)$-formula without parameters.

We shall use the following statement that follows readily from well-known
facts.

######  Fact.

There is standard $c\geq 1$ depending just on $\phi^{\prime}$ and parameters
$\overline{c}$ and $m$ from $\mathbb{I}$ such that for any $a\in[2m],b\in[m]$
there is a depth $|n|^{c}$ $PHP^{\sigma}\text{-tree}$ $T_{a,b}\in\mathbb{M}$
that decides the truth value of $\phi(a,b)$ in $(\mathbb{I},R_{G})$.

The quickest (although not the most elementary) way to see this is to use the
already mentioned fact that $\phi^{\prime}(x,y,\overline{z})$ defines a
relation computable by a standard polynomial-time Turing machine $U$ definable
in $S^{1}_{2}(R)$ and querying oracle about relation $R$ (see [7, Sections 6
and 7]). When $\overline{c}$ and $m$ from $\mathbb{I}$ (i.e. of bit-size
polynomial in $|n|$) are fixed and inputs $a,b$ are bounded by fixed $m$, the
running time of $U$ is bounded by $|n|^{c}$ for some standard $c$ and this
number bounds also the number of queries $U$ makes on any input. We already
know that for generic $G$ the structure $(\mathbb{I},R_{G})$ is a model of
$T^{1}_{2}(R)\vdash S^{1}_{2}(R)$ and so $U$ works there as well.

Given $a,b$, the computation develops according to oracle answers and all
possible computations can be represented by a decision tree $T^{\prime}_{a,b}$
of depth $\leq|n|^{c}$ that asks about truth values of atomic sentences
$R(u,v)$, for some $u\in[n+1]$ and $v\in[n]$.

To represent this by a $PHP\text{-tree}$ $T_{a,b}$ we simply replace query
“$R(u,v)?$” in $T^{\prime}_{a,b}$ by a $PHP$-query “$u\mapsto?$” (i.e. query
asking for a $w$ satisfying $R(u,w)$); if the answer is $v$, then the original
query in $T^{\prime}_{a,b}$ is answered “yes”, in all other cases it is
answered “no”. Because we know that the generic $R_{G}$ violates
$ontoPHP^{n+1}_{n}(R)$, we can delete from $T_{a,b}$ all paths that are not
partial one-to-one maps, getting the desired tree $T_{a,b}$.

As before, we identify $T_{a,b}$ with its maximal paths which, in turn, are
represented by partial one-to-one maps between $[n+1]$ and $[n]$ of size
$\leq|n|^{c}$, i.e. as elements of $\mathbb{P}$. Let $T^{+}_{a,b}$ be all such
maps for which the corresponding maximal paths in $T_{a,b}$ lead to acceptance
of $\phi(a,b)$.

We define $A$ as $A(a,b)=T^{+}_{a,b}$. Since $T_{a,b}$ is a
$PHP^{\sigma}\text{-tree}$ two different conditions from $A(a,b)$ are
incompatible and all such conditions are compatible with $\sigma$ while their
intersections with $\sigma$ are empty.

It is now enough to show that $A$ satisfies all four properties of (4.1). The
first three properties follow immediately from the fact that $\sigma$ is not
extendable to a condition which either forces
$\phi(a,b)\land\phi(a^{\prime},b)$ or $\phi(a,b)\land\phi(a,b^{\prime})$ for
$a\neq a^{\prime}$ and $b\neq b^{\prime}$.

Assume the fourth property is not satisfied, i.e.:

$\displaystyle\exists\rho\leq\sigma\>\exists a\in[2m]\>\forall
b\in[m]\>\forall\tau\in A(a,b)\>:\>\tau\perp\rho.$

It is enough to show $\rho\Vdash\neg\phi(a,b)$ for $a$ as above and all
$b\in[m]$ to derive a contradiction. Since $\phi(a,b)$ is
$\exists\overline{u}\leq t(a,b)\>\psi(a,b,\overline{u})$ for a sharply bounded
$\psi(a,b,\overline{u})$, we get:

$\displaystyle\rho\Vdash\neg\phi(a,b)\>\text{ iff
}\>\rho\Vdash\forall\overline{u}\leq t(a,b)\>\neg\psi(a,b,\overline{u}),$

where by (3.7, 4) the latter is equivalent to:

$\displaystyle\forall\overline{u}\leq
t(a,b)\>\rho\Vdash\neg\psi(a,b,\overline{u}).$

Since $\psi$ is sharply bounded we use (3.7, 7) to derive:

$\displaystyle\rho\Vdash\neg\psi(a,b,\overline{u})\>\text{ iff
}\>\forall\pi\leq\rho\>\pi\nVdash\psi(a,b,\overline{u}).$

Pick any $\pi$ extending $\rho$ and assume it forces $\psi(a,b,\overline{u})$.
Thus, $\pi\Vdash\phi(a,b)$ which implies $\pi$ is compatible with some
$\tau\in A(a,b)$. However, this implies $\rho\|\tau$ since $\pi\leq\rho$
contradicting our initial assumption that $\rho$ is incompatible with every
$\tau$ from $A(a,b)$ for every $b\in[m]$.

∎

######  Corollary 4.15.

$\displaystyle\emptyset\Vdash WPHP^{2m}_{m}(\Delta^{b}_{1}(R)),$

implying that for any generic filter $G$ it holds that:

$\displaystyle(\mathbb{I},R_{G})\vDash T^{1}_{2}(R)+\forall
mWPHP^{2m}_{m}(\Delta^{b}_{1}(R))+\exists n\neg ontoPHP^{n+1}_{n}(R).$

As an application of our proof methods, we derive the following result already
advertised in the abstract.

######  Theorem 4.16.

There exists a model of:

$\displaystyle T_{2}^{1}(R)+\exists n(\forall m\leq
n^{1-\epsilon}(PHP_{m}^{m+1}(\Delta^{b}_{1}(R)))+\neg PHP_{n}^{n+1}(R)),$

where $\epsilon$ is an arbitrarily small standard rational.

###### Proof.

The model is actually the same $(\mathbb{I},R_{G})$ as in 4.15.

Assuming:

$\displaystyle\emptyset\nVdash\forall m\leq
n^{1-\epsilon}(PHP_{m}^{m+1}(\Delta^{b}_{1}(R)))$

it follows that one can construct
$(n^{1-\epsilon},|n|^{c},\sigma)$-$PHP$-$array$ defined analogously as in 4.1
with the only difference being that the indexing set is
$[n^{1-\epsilon}+1]\times[n^{1-\epsilon}]$.

Theorems 4.11 and 4.12 still apply implying:

$\displaystyle(n^{1-\epsilon}+1)\cdot\frac{(n-|\sigma|)!}{(n-|\sigma|-|n|^{c})!}\leq
n^{1-\epsilon}\cdot\frac{(n+1-|\sigma|)!}{(n+1-|\sigma|-|n|^{c})!},$

The above results in:

$\displaystyle\frac{n^{1-\epsilon}+1}{n^{1-\epsilon}}\leq\frac{n+1-|\sigma|}{n+1-|\sigma|-|n|^{c}},$

which is a contradiction, since $|\sigma|\leq|n|^{c^{\prime}}$ and
$c^{\prime},c,\epsilon$ are standard. ∎

## Acknowledgements

The work first appeared in [11] supervised by Jan Krajíček. I am indebted to
my supervisor for detailed comments and suggestions.

## 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] M. Ajtai.  Parity and the Pigeonhole Principle.  In S. R. Buss and P. Scott, editors, Feasible mathematics, Progress in Computer Science and Applied Logic, pages 1 – 24. Birkhäuser, 1990.
  * [3] A. Atserias and M. Müller.  Partially definable forcing and bounded arithmetic.  Archive for Mathematical Logic, 54:1–33, 2015.
  * [4] S. R. Buss.  Bounded Arithmetic.  PhD thesis, Princeton University, 1985.
  * [5] R. Impagliazzo and J Krajíček.  A Note on Conservativity Relations Among Bounded Arithmetic Theories.  Mathematical Logic Quarterly, 48(3):375–377, 2002.
  * [6] 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.
  * [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] 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.
  * [11] M. Narusevych.  Models of bounded arithmetic.  Master’s thesis, Charles University, Prague, 2022.
  * [12] J. Paris and A. J. Wilkie.  Counting problems in bounded arithmetic.  pages 332 – 334, 1985.
  * [13] J. Paris, A. J. Wilkie, and A. R. Woods.  Provability of the pigeonhole principle and the existence of infinitely many primes.  J. Symbolic Logic, 53:1235 – 1244, 1988.
  * [14] T. Pitassi, P. Beame, and R. Impagliazzo.  Exponential lower bounds for the pigeonhole principle.  Random Structures and Algorithms, 7:15 – 39, 1995.
  * [15] Søren Riis.  Making infinite structures finite in models of second order bounded arithmetic.  Arithmetic, proof theory and computational complexity, pages 289–319, 1993.


11institutetext: University of Lincoln, UK 22institutetext: University of Hong
Kong, Hong Kong
22email: xq141839, kuangww, baogela, zeyu2022<EMAIL_ADDRESS>22email<EMAIL_ADDRESS>
# SPPNet: A Single-Point Prompt Network for Nuclei Image Segmentation

Qing Xu 1122 Wenwei Kuang 22 Zeyu Zhang 22 Xueyao Bao 22 Haoran Chen 22
Wenting Duan 11

###### Abstract

Image segmentation plays an essential role in nuclei image analysis. Recently,
the segment anything model has made a significant breakthrough in such tasks.
However, the current model exists two major issues for cell segmentation: (1)
the image encoder of the segment anything model involves a large number of
parameters. Retraining or even fine-tuning the model still requires expensive
computational resources. (2) in point prompt mode, points are sampled from the
center of the ground truth and more than one set of points is expected to
achieve reliable performance, which is not efficient for practical
applications. In this paper, a single-point prompt network is proposed for
nuclei image segmentation, called SPPNet. We replace the original image
encoder with a lightweight vision transformer. Also, an effective
convolutional block is added in parallel to extract the low-level semantic
information from the image and compensate for the performance degradation due
to the small image encoder. We propose a new point-sampling method based on
the Gaussian kernel. The proposed model is evaluated on the MoNuSeg-2018
dataset. The result demonstrated that SPPNet outperforms existing U-shape
architectures and shows faster convergence in training. Compared to the
segment anything model, SPPNet shows roughly 20 times faster inference, with
1/70 parameters and computational cost. Particularly, only one set of points
is required in both the training and inference phases, which is more
reasonable for clinical applications. The code for our work and more technical
details can be found at https://github.com/xq141839/SPPNet.

###### Keywords:

Single-point prompt, Feature combination, Nuclei segmentation

##  1 Introduction

Automatic nuclei segmentation has received significant attention from
pathologists and become an indispensable part of computer-aid diagnosis in the
future [15]. In the last few years, deep neural networks displayed outstanding
performance in various computer vision tasks. Specifically. U-Net, proposed by
Ronneberger et al. [12], has achieved great success in biomedical image
segmentation. It adopts a convolutional encoder and decoder to extract image
features and recover the original image shape respectively. A skip connection
strategy is used to incorporate low-level semantic information with high-level
semantic information in each layer. Zhou et al. [19] designed a nested U-Net
(Unet++). It adds a series of nested and dense skip pathways between the
encoder and decoder so that each layer can receive multi-scale semantic
information. Schlemper et al. [14] developed an attention U-Net that uses a
bottom-up attention gate to weight the concatenated feature map of the encoder
and decoder. It highlights target regions and improves the sensitivity of the
model. Instead of using a solely convolutional neural network (CNN) to encode
image features, Chen et al. [2] proposed TransUNet that combines CNN with
vision transformer (ViT) [4] for image patch extraction and global context
collection. With the increasing influence of transformer, a growing number of
modern medical segmentation models embed ViT or even adopt fully-transformer
architecture [17, 1]. Recently, segment anything model (SAM) [10] was proposed
as a foundation model for natural image segmentation. It consists of three
modules: a large masked autoencoders (MAE) [5] pre-trained ViT as image
encoder. A prompt encoder is used to fetch tokens from box, point, or text
inputs. A two-layer mask decoder leverages cross-attention for updating both
the image embedding and prompt tokens. However, it can be difficult to retrain
or fine-tune SAM when limited training sources are available. For nuclei image
segmentation, although SAM can present remarkable performance when provided
sufficient cell box or point prompts [6], it is not efficient for clinical
applications.

In this paper, we propose a single-point prompt network (SPPNet) for nuclei
segmentation in microscopic images. In order to improve the model robustness
in practical scenarios, a center neighbour selection algorithm is established
using the combination of distance transform and Gaussian kernel. To reduce the
parameters of image encoder, the MAE ViT of SAM is replaced with a Tiny-ViT
[16]. This small network may be not able to provide feature representations as
complex as the large one. Therefore, we introduce a helpful shadow network,
named low-level semantic information extractor (LLSIE). We evaluate the
proposed on the small dataset: MoNuSeg-2018 [11], and train the model with
only one RTX2080Ti graphic card. The experimental result shows that SPPNet
performs better than other state-of-the-art (SOTA) models and takes more than
20% less training time. Compared to SAM, our proposed model requires much
lower parameters, computational cost, and faster inference speed. Overall,
SPPNet shows promising potential as a new cell segmentation method for
pathological images in clinical settings.

##  2 Method

###  2.1 Center Neighborhood Point Sampling

The SAM model supports box and point prompts as inputs to direct the network
focus on target regions and provide precise segmentation masks. The former
requires gathering all potential cell bounding boxes in images. The latter
expects to acquire the center point of cells. Both methods are difficult to be
implemented in practice as one whole-slide microscopic image may include
thousands of nuclei and medical experts cannot guarantee to always label the
center of cells. To address this issue, we design a center neighborhood point
sampling algorithm, which is presented in Fig. 1.

Figure 1: Algorithm of center neighborhood point selection.

Firstly, we randomly select one cell from the ground truth as the target
region $\boldsymbol{x}$. Secondly, to find the center point $M$ of the nuclei,
the L1 distance transform method is applied to this area, which can be
represented as:

$M(\boldsymbol{x})=\arg\max\left[\min_{\boldsymbol{y}\in\Omega}|\boldsymbol{x}-\boldsymbol{y}|\right]$
(1)

The transform calculates the minimum L1 distance between each point in
$\boldsymbol{x}$ and the cell border $\Omega$. Then, we select the point with
the maximum value in this set as the center of the cell. If more than one
point satisfies the condition, we choose the first point in order. Thridly, a
Gaussian filter is operated on this center to capture its neighborhood points.
They can be defined as:

$G_{\sigma}\left(m_{x},m_{y}\right)=C\cdot
e^{-\frac{m_{x}^{2}+m_{y}^{2}}{2\sigma^{2}}},m_{x},m_{y}\in\left\\{-K,\ldots,0,\ldots,K\right\\}$
(2)

Where
$G_{\sigma}\left(m_{x},m_{y}\right)\in\mathbb{R}^{\left(2K+1\right)\times\left(2K+1\right)}$
stands for a 2D Gaussian kernel and
$\sum_{m_{x}=-K}^{K}\sum_{m_{y}=-K}^{K}G_{\sigma}\left(m_{x},m_{y}\right)=1$.
$\sigma^{2}$ is the isotropic covariance, the kernel size can be defined as
$(2K+1)\times(2K+1)$ and $C$ is a constant. Finally, we randomly pick one from
these neighbors as the positive input, which mimics the human behaviour of
point selection. The parameter $K$ is set to 2. For the negative point, we
randomly choose one from the background.

###  2.2 Patch up Low-Level Semantic Information

For the image encoder, SAM adopts a large-sized MAE [5] pre-trained ViT to
extract features from input images. Although point prompt-based SAM has
performed amazing zero-shot ability in natural image segmentation, medical
image segmentation still can be a challenging task due to its complexity of
interpretation. To retrain or fine-tune SAM on Nuclei datasets, 256 A100 GPUS
are required in the training phase [10]. It can be a non-trivial burden for
many researchers. Therefore, we replace SAM image encoder with a Tiny-ViT
[16], which drops the number of parameters by about 99.1%. However, such an
operation somehow diminishes the feature extraction ability of the image
encoder. Inspired by previous U-shape segmentation networks, we construct a
low-level semantic information extractor (LLSIE) to patch up shallow features.
The U-Net module [12] in Fig. 2 (a) has been widely used in various
architectures [9, 8]. The stem block [3] in Fig. 2 (b) is usually developed to
obtain the larger receptive field. The structure of LLSIE is shown in Fig. 2
(c). In order to decrease the

Figure 2: Comparison of our design and other common structures for low-level
feature extraction from input images.

computational cost and parameters of the network, our proposed module uses
depthwise separable convolution [7], composed of $3\times 3$ depthwise
convolution followed by $1\times 1$ pointwise convolution. The former is used
to merge spatial information. The latter integrates channel information. A
$3\times 3$ general convolution is inserted into the head of LLSIE to preserve
the receptive field and increase the feature dimension as depthwise separable
convolution cannot perform well on low-channel feature maps [13]. In the end,
we involve a residual connection to mitigate the potential effect of the
gradient vanish.

###  2.3 SPPNet Architecture

For nuclei image segmentation, we establish the SPPNet based on the proposed
point sampling strategy and LLSIE block. Fig. 3 displays an overview of our
SSPNet.

Figure 3: Overview of our single-point prompt network with efficient vison
transformer.

The input RGB microscopic images are first fed to the Tiny-ViT for feature
extraction. A single set of point prompts, including one cell point and one
background point, will be generated using center neighborhood point sampling,
and then used to collect tokens by prompt encoder. The mask decoder leverages
multilayer perceptrons and a cross-attention mechanism to upgrade the image
embedding as well as prompt, and raise the width and height of feature maps to
$256\times 256$. In addition, the LLSIE block is in parallel with the image
encoder for capturing low-level semantic information from inputs. This block
is followed by a $2\times 2$ max pooling with stride 2 for aligning with the
shape of the feature map produced by the mask decoder. A connection operation
fuses both two features and one $1\times 1$ convolution declines the channel
to the same number of classes as prediction. Finally, we reuse the post-
processing method of SAM to recover the image size and generate masks.

##  3 Experiments and Results

###  3.1 Implementation Details

All experiments are conducted with PyTorch 1.10.0 framework on a single
NVIDI-A RTX2080Ti Tensor Core GPU, 4-core CPU, and 28GB RAM. A standard dice
loss function and an Adam optimizer with a learning rate of 5e-4 are used to
train all models. We set batch sizes and epochs to 4 and 200 respectively. The
early stopping strategy is implemented to avoid overfitting. During training
our SSPNet, we input original microscopic images to the image encoder and
resized images ($256\times 256$) to the LLSIE block. These resized images are
also used to train other SOTA methods for comparison. Meanwhile, Tiny-ViT
loads a pre-trained checkpoint based on knowledge distillation [18]. The
prompt encoder and mask decoder of SPPNet reuse the pre-trained weight of SAM
[10]. We randomly select 80% samples as a training set, 10% as a validation
set, and 10% as a test set. Moreover, data augmentation methods have been
widely used to extend image diversity and improve model robustness. In the
experiment, horizontal flip, rotation, and cutout with a probability of 0.25
are randomly applied to the training set.

###  3.2 Evaluation metrics.

In order to evaluate and quantify mode performance. Mean intersection over
union (mIoU) and dice coefficient (DSC), the standard medical image
segmentation metrics, are computed on the test set. Both show the similarity
between prediction and ground truth using different calculation methods, where
mIoU tends to penalise single instances of bad classification. Additionally,
we report parameters (Params), floating point operations (FLOPs), and frames
per second (FPS) of models to reveal their sizes, computational complexity,
and inference speed.

###  3.3 Comparison on MoNuSeg-2018 dataset.

Microscopic images usually include a large number of cells. Manual labeling is
expensive and time-consuming. Therefore, we select a small dataset to evaluate
all models, which is more feasible in clinical applications. MoNuSeg-2018 is
an open-access dataset for MICCAI 2018 multi-organ nuclei segmentation
challenge. It only contains 51 fully-labeled pathological images. We trained
SPPNet and four SOTA models. The quantitative result of the test set is
provided in Table 1.

Table 1: Performance comparison between our method (SSPNet) and other SOTA
models on MoNuSeg-2018 dataset.

Method | mIoU(%) | DSC(%) | Params(M) | FLOPs | FPS
---|---|---|---|---|---
U-Net [12] | 61.64±8.28 | 75.92±6.79 | 13.40 | 23.83 | 93.22
Unet++ [19] | 62.28±6.54 | 76.05±5.06 | 9.16 | 26.73 | 69.88
Attention U-Net [14] | 63.85±7.23 | 77.68±5.82 | 34.88 | 51.02 | 55.19
TransUNet [2] | 57.87±6.41 | 73.09±5.51 | 61.82 | 32.63 | 66.67
Swin-UNet [1] | 58.21±6.50 | 73.36±5.50 | 27.15 | 5.91 | 43.12
SPPNet | 66.43±4.32 | 79.77±3.11 | 9.79 | 39.90 | 22.61

We can observe that SPPNet achieves a DSC of 79.77% and a mIoU of 66.43%,
which outperforms Attention U-Net by 2.09% in terms of DSC and 2.58% in mIoU.
Particularly, our proposed model demonstrates a significant enhancement over
the two previous transformer-based architectures, where the mIoU of SPPNet is
8.56% and 8.22% higher than TransUNet and Swin-UNet, and the DSC of SPPNet is
6.68% and 6.41% higher than these two models respectively. Also, SPPNet costs
considerably fewer parameters. Consequently, our proposed model reveals the
highest score in standard evaluation metrics of medical image segmentation.

###  3.4 Ablation Study

In this section, a detailed ablation study is conducted on SPPNet. LLSIE block
is an essential module to capture low-level semantic information from input
images. We first compare LLSIE with other prevalent blocks, which is shown in
Table 2.

Table 2: Performance comparison between our LLSIE block and other general
methods for low-level semantic information extraction on MoNuSeg-2018 dataset.

Block | mIoU(%) | DSC(%) | Params(M) | FLOPs | FPS
---|---|---|---|---|---
U-Net [12] | 64.95±7.94 | 77.70±6.37 | 9.80 | 40.41 | 22.12
Stem | 65.13±6.69 | 78.93±5.19 | 9.81 | 41.02 | 21.55
LLSIE | 66.43±4.32 | 79.77±3.11 | 9.79 | 39.90 | 22.61

Figure 4: Training time cost to achieve SOTA performance with the U-Net
baseline (left side) and presentation of model stability with violin plot
(right side).

It can be demonstrated that the LLSIE block not only performs better than
U-Net and Stem blocks in metrics of mIoU and DSC, but also has faster
inference speed and costs a lower number of parameters as well as
computational resources. Furthermore, we evaluate the efficiency of Tiny-ViT,
center neighborhood point sampling strategy, and LLSIE block, which is
presented in Table 3. We make a comparison to SAM with fine-tuned prompt
encoder and mask decoder.

Table 3: Detailed ablation study of our single-point prompt network
architecture on dataset. IE: image encoder, PE: prompt encoder, MD: mask
decoder, CNPS: center neighborhood point sampling

SAM | SPPNet |  |  |  |  |
---|---|---|---|---|---|---
IE | PE | MD | IE | CNPS | LLSIE | mIoU(%) | DSC(%) | Params(M) | FLOPs | FPS
✓ | ✓ | ✓ |  |  |  | 60.18±8.15 | 74.76±7.00 | 635.93 | 2736.63 | 1.39
| ✓ | ✓ | ✓ |  |  | 62.33±4.05 | 76.22±2.98 | 9.78 | 39.73 | 23.78
| ✓ | ✓ | ✓ | ✓ |  | 63.77±5.77 | 77.73±4.26 | 9.78 | 39.73 | 23.64
| ✓ | ✓ | ✓ | ✓ | ✓ | 66.43±4.32 | 79.77±3.11 | 9.79 | 39.90 | 22.61

From Table 3, we can first conclude that it is necessary to retrain the image
encoder when applied to the nuclei segmentation task as retrained Tiny-ViT
outperforms pre-trained MAE ViT. Secondly, our center neighborhood point
sampling strategy can improve model performance without any extra parameters
and computational costs. Thirdly, incorporating low-level semantic information
can help the model predict a more precise segmentation mask. Overall, compared
to SAM, SPPNet shows better performance, considerably fewer parameters, lower
computational costs, and faster inference.

Figure 5: Qualitative comparison results between SPPNet and other SOTA models
on the test set of MoNuSeg-2018.

###  3.5 Model Stability

When applying the center neighborhood point sampling strategy to determine a
positive point, the target cell and neighbors are randomly selected by our
program. To evaluate our model stability, we use the same trained model to
implement the test set with 500 iterations. The result is provided in Fig. 4
(right side) with a violin plot. It can be demonstrated that the dice score of
the proposed SPPNet is clustered at 79.776% to 79.778%. The maximum
performance gap is only about 0.01%. As a result, we can argue that the random
point selection based on our sampling strategy does not have a significant
impact on the model performance.

###  3.6 Dicussion

Nuclei image segmentation is an important step for pathological analysis for
patients. From the above experimental results, our approach shows an
outstanding improvement compared to SAM in training resource costs and better
performance than existing SOTA models of medical image segmentation. Also,
SPPNet can take about 50% less time than others in the training phase, which
is shown in Fig. 4 (left side). To further demonstrate the efficiency of
SPPNet in clinical applications, some segmentation masks using all models on
the test set are visualised in Fig. 5. Compared to other architectures, SPPNet
is able to provide more accurate masks and fewer false positive cases. In
addition, SAM displays a great zero-shot ability in natural image segmentation
as it is trained on an extremely sufficient dataset. Therefore, we will also
explore the zero-shot performance of SPPNet for nuclei image segmentation in
the future. Achieving a such foundation model can considerably alleviate the
paucity of pathologists.

##  4 Conclusion

In this paper, we propose a single-point prompt network for nuclei image
segmentation. The LLSIE block is used to patch up lower-level semantic
information in the mask decoder. A center neighborhood point sampling strategy
makes inference more feasible in clinical applications. The experimental
results demonstrate that our SPPNet can be considered a new benchmark for cell
segmentation.

## References

  * [1] Cao, H., Wang, Y., Chen, J., Jiang, D., Zhang, X., Tian, Q., Wang, M.: Swin-unet: Unet-like pure transformer for medical image segmentation. In: European conference on computer vision. pp. 205–218. Springer (2022)
  * [2] Chen, J., Lu, Y., Yu, Q., Luo, X., Adeli, E., Wang, Y., Lu, L., Yuille, A.L., Zhou, Y.: Transunet: Transformers make strong encoders for medical image segmentation. arXiv preprint arXiv:2102.04306 (2021)
  * [3] Chen, K., Wang, J., Pang, J., Cao, Y., Xiong, Y., Li, X., Sun, S., Feng, W., Liu, Z., Xu, J., et al.: Mmdetection: Open mmlab detection toolbox and benchmark. arXiv preprint arXiv:1906.07155 (2019)
  * [4] Dosovitskiy, A., Beyer, L., Kolesnikov, A., Weissenborn, D., Zhai, X., Unterthiner, T., Dehghani, M., Minderer, M., Heigold, G., Gelly, S., et al.: An image is worth 16x16 words: Transformers for image recognition at scale. arXiv preprint arXiv:2010.11929 (2020)
  * [5] He, K., Chen, X., Xie, S., Li, Y., Dollár, P., Girshick, R.: Masked autoencoders are scalable vision learners. In: Proceedings of the IEEE/CVF conference on computer vision and pattern recognition. pp. 16000–16009 (2022)
  * [6] He, S., Bao, R., Li, J., Grant, P.E., Ou, Y.: Accuracy of segment-anything model (sam) in medical image segmentation tasks. arXiv preprint arXiv:2304.09324 (2023)
  * [7] Howard, A.G., Zhu, M., Chen, B., Kalenichenko, D., Wang, W., Weyand, T., Andreetto, M., Adam, H.: Mobilenets: Efficient convolutional neural networks for mobile vision applications. arXiv preprint arXiv:1704.04861 (2017)
  * [8] Huang, H., Lin, L., Tong, R., Hu, H., Zhang, Q., Iwamoto, Y., Han, X., Chen, Y.W., Wu, J.: Unet 3+: A full-scale connected unet for medical image segmentation. In: ICASSP 2020-2020 IEEE international conference on acoustics, speech and signal processing (ICASSP). pp. 1055–1059. IEEE (2020)
  * [9] Jha, D., Riegler, M.A., Johansen, D., Halvorsen, P., Johansen, H.D.: Doubleu-net: A deep convolutional neural network for medical image segmentation. In: 2020 IEEE 33rd International symposium on computer-based medical systems (CBMS). pp. 558–564. IEEE (2020)
  * [10] Kirillov, A., Mintun, E., Ravi, N., Mao, H., Rolland, C., Gustafson, L., Xiao, T., Whitehead, S., Berg, A.C., Lo, W.Y., et al.: Segment anything. arXiv preprint arXiv:2304.02643 (2023)
  * [11] Kumar, N., Verma, R., Sharma, S., Bhargava, S., Vahadane, A., Sethi, A.: A dataset and a technique for generalized nuclear segmentation for computational pathology. IEEE transactions on medical imaging 36(7), 1550–1560 (2017)
  * [12] Ronneberger, O., Fischer, P., Brox, T.: U-net: Convolutional networks for biomedical image segmentation. In: International Conference on Medical image computing and computer-assisted intervention. pp. 234–241. Springer (2015)
  * [13] Sandler, M., Howard, A., Zhu, M., Zhmoginov, A., Chen, L.C.: Mobilenetv2: Inverted residuals and linear bottlenecks. In: Proceedings of the IEEE conference on computer vision and pattern recognition. pp. 4510–4520 (2018)
  * [14] Schlemper, J., Oktay, O., Schaap, M., Heinrich, M., Kainz, B., Glocker, B., Rueckert, D.: Attention gated networks: Learning to leverage salient regions in medical images. Medical image analysis 53, 197–207 (2019)
  * [15] Wang, R., Lei, T., Cui, R., Zhang, B., Meng, H., Nandi, A.K.: Medical image segmentation using deep learning: A survey. IET Image Processing 16(5), 1243–1267 (2022)
  * [16] Wu, K., Zhang, J., Peng, H., Liu, M., Xiao, B., Fu, J., Yuan, L.: Tinyvit: Fast pretraining distillation for small vision transformers. In: European Conference on Computer Vision. pp. 68–85. Springer (2022)
  * [17] Yan, X., Tang, H., Sun, S., Ma, H., Kong, D., Xie, X.: After-unet: Axial fusion transformer unet for medical image segmentation. In: Proceedings of the IEEE/CVF winter conference on applications of computer vision. pp. 3971–3981 (2022)
  * [18] Zhang, C., Han, D., Qiao, Y., Kim, J.U., Bae, S.H., Lee, S., Hong, C.S.: Faster segment anything: Towards lightweight sam for mobile applications. arXiv preprint arXiv:2306.14289 (2023)
  * [19] Zhou, Z., Siddiquee, M.M.R., Tajbakhsh, N., Liang, J.: Unet++: Redesigning skip connections to exploit multiscale features in image segmentation. IEEE transactions on medical imaging 39(6), 1856–1867 (2019)