# On the Unprovability of Circuit Size Bounds in Intuitionistic
$\mathsf{S}^{1}_{2}$

Lijie Chen111Miller Institute for Basic Research in Science. University of
California at Berkeley. Email<EMAIL_ADDRESS>
Jiatu Li222Computer Science & Artificial Intelligence Laboratory.
Massachusetts Institute of Technology. Email<EMAIL_ADDRESS>
Igor C. Oliveira333Department of Computer Science. University of Warwick.
Email<EMAIL_ADDRESS>

###### Abstract

We show that there is a constant $k$ such that Buss’s intuitionistic theory
$\mathsf{IS}^{1}_{2}$ does not prove that SAT requires co-nondeterministic
circuits of size at least $n^{k}$. To our knowledge, this is the first
unconditional unprovability result in bounded arithmetic in the context of
worst-case fixed-polynomial size circuit lower bounds. We complement this
result by showing that the upper bound
$\mathsf{NP}\subseteq\mathsf{coNSIZE}[n^{k}]$ is unprovable in
$\mathsf{IS}^{1}_{2}$.

###### Contents

  1. 1 Introduction
    1. 1.1 Context and motivation
    2. 1.2 Results
    3. 1.3 Related work
  2. 2 Preliminaries
    1. 2.1 Intuitionistic bounded arithmetic
    2. 2.2 Complexity theory
  3. 3 Unprovability of Lower Bounds in $\mathsf{IS}^{1}_{2}$
    1. 3.1 Unconditional lower bounds for refuters
    2. 3.2 Unprovability of lower bounds via refuter lower bounds
  4. 4 Unprovability of Upper Bounds in $\mathsf{IS}^{1}_{2}$
    1. 4.1 Unconditional uniform lower bound against co-nondeterministic circuits
    2. 4.2 Unprovability of upper bounds via uniform lower bounds
  5. 5 Interpretation and Generalization of Our Results
  6. A On the Unprovability of Lower Bounds Against Deterministic Circuits

##  1 Introduction

###  1.1 Context and motivation

Pich and Santhanam [31] and subsequently Li and Oliveira [27] have shown that
certain strong complexity lower bounds are unprovable in bounded arithmetic
theory $\mathsf{PV}_{1}$ and its extensions, such as $\mathsf{APC}_{1}$ and
$\mathsf{S}^{1}_{2}$. For instance, [31] established that $\mathsf{PV}_{1}$
does not prove that there is a language $L\in\mathsf{NP}$ that is average-case
hard against co-nondeterministic circuits of size $2^{n^{o(1)}}$. Note that,
while the unprovability results of [31] and [27] are unconditional, they only
apply to significantly strong complexity lower bounds.

It would be more interesting to understand the (un)provability of circuit
lower bounds that are closer to major open problems from complexity theory,
such as showing that $\mathsf{NP}$ is not contained in $\P/\poly$. To achieve
this, it is necessary to develop techniques to address the following three
aspects for which these lower bound statements are stronger than
$\NP\not\subset\P/\poly$:

  1. (A)

The statements consider average-case instead of worst-case lower bounds.

  2. (B)

They refer to sub-exponential size instead of super-polynomial size lower
bounds.

  3. (C)

The lower bound is against co-nondeterministic circuits instead of
deterministic circuits.

Aiming for unconditional results, we propose the consideration of these three
challenges in the more restricted (but formally necessary) setting of
_intuitionistic_ theories of bounded arithmetic. Intuitionistic theories
distinguish themselves from classical logic systems by aligning more closely
with the concept of constructive proofs. Notably, intuitionistic logic systems
do not presuppose the principles of the excluded middle and double negation
elimination, which give rise to key inference rules in classical logic (see,
e.g., [23] for some background and applications).444For instance, win-win
arguments from complexity theory, such as the non-constructive proof of the
existence of a pseudodeterministic algorithm for generating primes from [29]
by considering if $\mathsf{PSPACE}\subseteq\mathsf{BPP}$ or not, are not
available in intuitionistic theories. We note that connections between
complexity theory and intuitionistic logic have been widely investigated (see,
e.g., [7, 16, 8, 20, 17, 9, 3, 28, 18, 21] and references therein).

###  1.2 Results

We show that _worst-case_ _fixed-polynomial size_ lower bounds against _co-
nondeterministic_ circuits for a language in $\mathsf{NP}$ cannot be
established in $\mathrm{IS}^{1}_{2}$ [7], the intuitionistic analogue of
Buss’s theory $\mathsf{S}^{1}_{2}$ [6]. This unconditional result addresses
aspects (A) and (B) highlighted above, in the setting of intuitionistic
bounded arithmetic.555Note that showing the unprovability of fixed-polynomial
size lower bounds is stronger than showing the unprovability of super-
polynomial size lower bounds. We also remark that the lower bound we consider,
which is weaker than $\NP\not\subset\coNP/\poly$, is implied by the widely
believed conjecture that $\PH$ does not collapse. On the other hand, we are
not aware of any standard assumption that implies the strong two-sided error
average-case lower bounds for $\NP$ against subexponential-size co-
nondeterministic circuits considered in previous unprovability results [31,
27].

A natural question is whether one can also unconditionally show that lower
bounds against deterministic circuits (instead of co-nondeterministic
circuits) are unprovable in $\mathsf{IS}^{1}_{2}$, which corresponds to Item
(C) in the discussion above. As we explain in Appendix A, for some
formalizations of this lower bound statement, unprovability in
$\mathsf{IS}^{1}_{2}$ yields unprovability in the stronger theory
$\mathsf{S}^{1}_{2}$, an observation that first appeared in Ghasemloo and Pich
[18]. We believe that this connection further motivates the investigation of
the unprovability of complexity lower bounds in intuitionistic theories.

Next, we provide more details about our results and formalizations.

#### Formalizations.

Fix a polynomial-time nondeterministic machine $M$. Given $n_{0}\in\mathbb{N}$
and a size-bound $s\colon\mathbb{N}\to\mathbb{N}$ that is sufficiently time-
constructive and satisfies $n\leq s(n)\leq 2^{n}$, we consider a sentence
$\mathsf{LB}^{\mathsf{exp}}(M,s,n_{0})$ stating that:666Note that
$n\in\mathsf{Log}\mathsf{Log}$ essentially means that bounded quantifiers
refer to objects of length $2^{O(n)}$; similarly, $n\in\mathsf{Log}$ means
that bounded quantifiers refer to objects of length $\poly(n)$. For a formal
definition, see Section 2.1.

$\forall n\in\mathsf{LogLog}~{}\text{with}~{}n\geq n_{0}~{}\forall
D\in\mathsf{coNSIZE}[s(n)]~{}\exists
x\in\\{0,1\\}^{n}~{}\mathsf{Error}_{M}(D,n,x)\;,$

where $\mathsf{Error}_{M}(D,n,x)$ denotes the formula

$(\exists y,z\in\\{0,1\\}^{s(n)}\,M(x,y)=1\wedge D(x,z)=0)\vee(\forall
y,z\in\\{0,1\\}^{s(n)}~{}M(x,y)=0\wedge D(x,z)=1)\;.$

This sentence expresses that, for every $n\geq n_{0}$, no co-nondeterministic
circuit of size at most $s(n)$ decides $L(M)$ on inputs of length $n$. The
notation $\mathsf{LB}^{\mathsf{exp}}$ emphasizes that a candidate proof of
this sentence is able to manipulate concepts of exponential size $2^{O(n)}$,
since $n\in\mathsf{LogLog}$. We refer to Section 2.1 for more details on how
to formalize this sentence in the setting of $\mathsf{IS}^{1}_{2}$.

If $s(n)=n^{k}$ for some rational number $k\geq 1$, we can consider a sentence
$\mathsf{LB}^{\mathsf{poly}}(M,s,n_{0})$ stating that:

$\forall n\in\mathsf{Log}~{}\text{with}~{}n\geq n_{0}~{}\forall
D\in\mathsf{coNSIZE}[s(n)]~{}\exists
x\in\\{0,1\\}^{n}~{}\mathsf{Error}_{M}(D,n,x)\;.$

The key difference here is that when $s(n)=n^{k}$ it is sufficient to assume
$n\in\mathsf{Log}$ to obtain a natural formalization of complexity lower
bounds. Correspondingly, the notation $\mathsf{LB}^{\mathsf{poly}}$ emphasizes
that a candidate proof of this sentence can manipulate concepts of size
polynomial in $n$.

######  Theorem 1.1.

The following results hold:

  * _(_ i _)_

_[Exponential Regime]_ Let $\delta>0$ be a rational number,
$n_{0}\in\mathbb{N}$, and $M$ be a polynomial-time nondetermistic machine.
Then
$\mathsf{IS}^{1}_{2}\nvdash\mathsf{LB}^{\mathsf{exp}}(M,2^{n^{\delta}},n_{0})\;.$

  * _(_ ii _)_

_[Polynomial Regime]_ Let $n_{0}\in\mathbb{N}$ and $M$ be a polynomial-time
nondetermistic machine. Then there is an integer $k\geq 1$ such that
$\mathsf{IS}^{1}_{2}\nvdash\mathsf{LB}^{\mathsf{poly}}(M,n^{k},n_{0})\;.$

The proof of Theorem 1.1 combines two main steps. First, we employ a strong
witnessing result [7, 16] for the intuitionistic theory $\mathsf{IS}^{1}_{2}$
to show that the provability of a circuit lower bound yields a computationally
bounded _refuter_. A refuter for a lower bound of the form
$L\notin\mathcal{C}$, where $\mathcal{C}$ is a complexity class, is an
algorithm $R(1^{n},E)$ that, given an input length $n$ and a device $E$ from
$\mathcal{C}$, outputs an $n$-bit string $x$ such that $E(x)\neq L(x)$. We
then establish unconditionally that such a refuter does not exist.
Consequently, the lower bound sentence cannot be proved in the theory
$\mathsf{IS}^{1}_{2}$.

Elaborating on our approach, we now present some new consequences for refuters
that might be of independent interest. We use $\mathsf{SAT}_{n}$ to denote the
decision version of the satisfiability problem for De Morgan Boolean formulas
represented by $n$-bit strings (our results are robust to encoding details).
As in the discussion above, we say that a refuter $R$ for a language $L$
succeeds against a class $\mathcal{C}$ of devices on input length $n$ if, for
every $E\in\mathcal{C}$, $R(1^{n},E)$ outputs $x\in\\{0,1\\}^{n}$ such that
$E(x)\neq L(x)$. Observe that the existence of such a refuter implies that
$L\notin\mathcal{C}$.

######  Theorem 1.2.

The following results hold:

  * _(_ i _)_

Let $k$ and $c$ be rational numbers such that $1<k<c<k^{2}$. Then there is no
refuter $R(1^{n},E_{n})$ for $\mathsf{SAT}_{n}$ against
$E_{n}\in\mathsf{coNSIZE}[n^{k}]$ that has nonuniform circuit size $\leq
n^{c}$ and succeeds on every large enough input length $n$.

  * _(_ ii _)_

There is an integer $k\geq 1$ such that there is no refuter $R(1^{n},E_{n})$
for $\mathsf{SAT}_{n}$ against $E_{n}\in\mathsf{coNSIZE}[n^{k}]$ of nonuniform
polynomial size which succeeds on every large enough input length.

These two items are incomparable. The first item of Theorem 1.2 is an
impossibility result for refuting even very weak lower bounds ($n^{k}$ gates
for any fixed $k>1$), but only addresses refuters of size smaller than
$n^{k^{2}}$. On the other hand, the second item holds against any polynomial
size refuter, but does not provide an explicit constant $k$ for the size
bound.

At a high level, the proof of Theorem 1.2 proceeds by contradiction. From the
existence of such a refuter, we obtain a worst-case _upper bound_ on the
complexity of $\mathsf{SAT}_{n}$. This step requires an extension of a
technique from previous papers [26, 30] to the setting of _worst-case
complexity_ and to the _polynomial circuit size_ regime. To achieve this, we
employ a new _bootstrapping argument_ (see Section 3.1) that invokes the
refuter over different input lengths and aggregates the information obtained
from it. Finally, the circuit size upper bound extracted from the refuter
contradicts the original assumption that a refuter exists, since it implicitly
assumes a corresponding circuit lower bound. We note that the second item of
Theorem 1.2 requires an extra non-constructive ingredient, and as a result,
the proof does not produce an explicit constant $k$.

Finally, we complement Theorem 1.1 by establishing the unprovability in
$\mathsf{IS}^{1}_{2}$ of the upper bound
$\NP\subseteq\mathsf{coNSIZE}[n^{k}]$, for any fixed $k\in\mathbb{N}$. The
formalization of this upper bound statement is presented in Section 4.

######  Theorem 1.3 (Informal, see Theorem 4.5).

For any constant $k\in\mathbb{N}$,
$\mathsf{IS}^{1}_{2}\nvdash``\NP\subseteq\mathsf{coNSIZE}[n^{k}]"$.

The proof of Theorem 1.3 relies on an adaptation of an approach from [22],
which reduces the _unprovability of non-uniform circuit upper bounds_ to
establishing certain _uniform circuit lower bounds_ (in the standard sense of
complexity theory). In our result, the required uniform circuit lower bound is
achieved by a modification of an argument from [34].

Theorem 1.3 contributes to an active line of research on the unprovability of
circuit upper bounds [14, 22, 5, 4, 15, 2]. In contrast to other unconditional
results from these papers, which hold even for stronger theories, Theorem 1.3
establishes the unprovability of _co-nondeterministic_ circuit upper bounds
for $\mathsf{NP}$.777Note that establishing the unprovability of co-
nondeterministic circuit size upper bounds is stronger than establishing the
unprovability of deterministic circuit size upper bounds.

Altogether, Theorem 1.1 Item (_ii_) and Theorem 1.3 bring us closer to an
unconditional _independence_ result for $\mathsf{IS}^{1}_{2}$ with respect to
worst-case fixed-polynomial bounds in co-nondeterministic circuit
complexity.888Formally, our results show that for each $L\in\mathsf{NP}$ there
is $k$ such that the lower bound $L\notin\mathsf{coNSIZE}[n^{k}]$ is
unprovable, and that for each $k$ there is $L\in\mathsf{NP}$ such that the
upper bound $L\in\mathsf{coNSIZE}[n^{k}]$ is unprovable. While our
unprovability results are robust to the use of different machines of the same
time complexity to represent $L$ in a sentence, we note that they do not give
a fixed pair $(L^{\prime},k^{\prime})$ for which both lower bounds and upper
bounds are unprovable.

Finally, we note that both Theorem 1.1 and Theorem 1.3 can be extended to
“semi-classical” formalizations of the statements, where the sub-formula
inside the outermost existential quantifier can be replaced by any classically
equivalent formula. Details of this extension are discussed in Section 5.

###  1.3 Related work

Ghasemloo and Pich [18] studied connections between natural proofs [33] and
intuitionistic logic. In a bit more detail, the theory of natural proofs can
be used to establish the _conditional_ unprovability of circuit lower bounds
in classical theories admitting certain interpolation theorems (see [32, 25]),
and [18] investigates what (conditional) consequences this can have for the
provability of lower bounds in intuitionistic theories.

Theorem 1.1 should be contrasted with a result from Cook and Urquhart [16,
Theorem 10.16] establishing the unprovability of super-polynomial lower bounds
for the extended Frege propositional proof system in the related
intuitionistic theory $\mathsf{IPV}^{\omega}$ (see also [24, Corollary 4] and
[9, Section 6.2]). We note that the two results consider different lower bound
questions, formalizations, and choice of parameters. Moreover, their proofs
rely on completely different approaches. For instance, in terms of the
formalization, the sentences $\mathsf{LB}^{\mathsf{exp}}$ and
$\mathsf{LB}^{\mathsf{poly}}$ do not state that the input $x$ under
$\mathsf{Error}_{M}(x)$ is a tautology, which appears to be crucial in the
results from [16, 24]. Furthermore, to our knowledge, it is not known how to
extend their results to the fixed-polynomial size regime, as in Theorem 1.1
Item (_ii_).

It is perhaps interesting to compare Theorem 1.2 Item (_ii_) with the positive
results of Gutfreund, Shaltiel, and Ta-Shma [19] about the existence of
refuters (see also [13] and references therein). For instance, [19, Lemma 4.1]
roughly states that, if $\mathsf{NP}\neq\mathsf{RP}$, then it is possible to
produce counter-examples to the correctness of a randomized input machine of
complexity $n^{k}$ in time of order $n^{k^{2}}$. While the parameters of our
lower bound and of their upper bound nearly match, we note that their results
and Theorem 1.2 Item (_ii_) refer to different complexity lower bounds and
consider slightly different refuter guarantees.

#### Acknowledgements.

We would like to thank Erfan Khaniki and Dimitrios Tsintsilidas for
discussions on proof complexity lower bounds in intuitionistic bounded
arithmetic. Igor C. Oliveira received support from the Royal Society
University Research Fellowship URF$\setminus$R1$\setminus$191059; the UKRI
Frontier Research Guarantee Grant EP/Y007999/1; and the Centre for Discrete
Mathematics and its Applications (DIMAP) at the University of Warwick. Lijie
Chen is supported by a Miller Research Fellowship. Jiatu Li is supported by an
Akamai Presidential Fellowship.

##  2 Preliminaries

###  2.1 Intuitionistic bounded arithmetic

We consider the intuitionistic theory of bounded arithmetic
$\mathsf{IS}^{1}_{2}$ introduced in [7] (see also [16, 8] for equivalent
definitions). Our unprovability results are quite robust, as they rely on the
consequences of a witnessing theorem for $\mathsf{IS}^{1}_{2}$ and do not
crucially depend on details of the formalization. Nevertheless, for
concreteness and in order to complement the discussion in Appendix A, below we
provide more details about the theory. The exposition assumes basic
familiarity with bounded arithmetic (see, e.g., [10] for the necessary
background).

Informally, $\mathsf{IS}^{1}_{2}$ can be defined as theory
$\mathsf{S}^{1}_{2}$ but with intuitionistic predicate logic and polynomial
induction restricted to $\Sigma^{b+}_{1}$-formulas, i.e.,
$\Sigma^{b}_{1}$-formulas that do not contain implications and negations.
Next, we review some details for a reader that might not be familiar with this
terminology. Since we will not make use of sequent calculus, we follow the
Hilbert-style equivalent presentation from [16].

As in the case of $\mathsf{S}^{1}_{2}$, we take the language of
$\mathsf{IS}^{1}_{2}$ to consist of non-logical symbols $0$, $S$, $+$,
$\times$, $\\#$, $\lfloor\frac{1}{2}x\rfloor$, $|x|$, and $\leq$ with their
usual interpretations over the intended standard model $\mathbb{N}$. The
logical symbols are $\wedge$, $\vee$, $\rightarrow$, $\forall$, $\exists$, and
$=$. The connectives $\neg$ and $\leftrightarrow$ can be introduced with
appropriate abbreviations using $\rightarrow$ [16, Page 109]. In terms of non-
logical axioms, $\mathsf{IS}^{1}_{2}$ consists of 21 basic axioms (see [16,
Page 111]) and the axiom scheme $\Sigma^{b+}_{1}$-PIND (discussed below). The
standard logical axiom schemes and rules of inference governing intuitionistic
predicate logic are listed in [16, Page 110].

For a term $t$ not containing a variable $x$, we can define _bounded
quantifiers_ $(\exists x\leq t)\,\varphi$ and $(\forall x\leq t)\,\varphi$ via
the abbreviations $\exists x\,(x\leq t\wedge\varphi)$ and $\forall x\,(St\leq
x\vee\varphi)$, respectively. _Sharply bounded quantifiers_ are bounded
quantifiers of the form $(\exists x\leq|t|)$ and $(\forall x\leq|t|)$. We
recall that $\Pi^{b}_{0}=\Sigma^{b}_{0}$ is the set of formulas whose
quantifiers are all sharply bounded. Similarly, formulas containing only
bounded quantifiers can be classified into hierarchies $\Sigma^{b}_{i}$ and
$\Pi^{b}_{i}$ by counting alternations of bounded quantifiers while ignoring
sharply bounded quantifiers (cf. [16, Page 111]). A formula is _positive_ if
it contains no occurrence of the symbol $\rightarrow$ (recall that negations
are introduced via abbreviation and do not need to be explicitly discussed). A
formula is $\Sigma^{b+}_{1}$ if it is both $\Sigma^{b}_{1}$ and positive.

We define $\forall n\in\mathsf{Log}$ (resp. $\exists n\in\mathsf{Log}$) as the
abbreviation of $\forall N~{}\forall n=|N|$ (resp. $\exists N~{}\exists
n=|N|$), namely bounded quantifiers refer to objects of length up to
$\poly(n)$. Similarly, we define $\forall n\in\mathsf{Log}\mathsf{Log}$ (resp.
$\exists n\in\mathsf{Log}\mathsf{Log}$) as the abbreviation of $\forall
N~{}\forall n=||N||$ (resp. $\exists N~{}\exists n=||N||$).

Finally, $\mathsf{IS}^{1}_{2}$ admits the aforementioned
$\Sigma^{b+}_{1}$-PIND axiom scheme, consisting of formulas (possibly with
additional parameters) of the form $\varphi(0)\wedge\forall
x\,(\varphi(\lfloor\frac{1}{2}x\rfloor)\rightarrow\varphi(x))\rightarrow\forall
y\,\varphi(y)\;,$ where $\varphi$ is a $\Sigma^{b+}_{1}$-formula.

#### Formalization of complexity lower bounds.

We now discuss the formalization of the sentences
$\mathsf{LB}^{\mathsf{exp}}(M,s,n_{0})$ and
$\mathsf{LB}^{\mathsf{poly}}(M,s,n_{0})$ informally introduced in Section 1.2.
Recall that $M$ is a non-deterministic polynomial-time machine,
$s\colon\mathbb{N}\to\mathbb{N}$, and $n_{0}\in\mathbb{N}$. The fixed machine
$M$ and the constant $n_{0}$ can be explicitly encoded using a term of
$\mathsf{IS}^{1}_{2}$ built from the constant symbol $0$ and from the other
function symbols. Note that, in order to formalize the lower bound statements,
it is sufficient to be able to define any polynomial-time function in the
language of $\mathsf{IS}^{1}_{2}$. Indeed, this allows us to employ
appropriate formulas to specify the output of $M$ on a given input, check if
an object $D$ encodes a circuit of a given size, evaluate a given circuit on
an input pair $(x,y)$, decode an $n$-bit string from an object $x$, etc.

It turns out that, as established in [16, Corollary 2.7], every function $f$
computable in polynomial time is $\Sigma^{b+}_{1}$-definable in
$\mathsf{IS}^{1}_{2}$. This means that there is a $\Sigma^{b+}_{1}$-formula
$\phi(x,y)$ such that $\mathbb{N}\models\forall x\,\phi(x,f(x))$ and
$\mathsf{IS}^{1}_{2}$ proves that $\forall x\,\exists!\,y\,\phi(x,y)$ (see
[16, Pages 114-115]). Given this result, it is not hard to fully specify the
sentences $\mathsf{LB}^{\mathsf{exp}}(M,s,n_{0})$ and
$\mathsf{LB}^{\mathsf{poly}}(M,s,n_{0})$ using a formula for each relevant
polynomial-time function. Since the details of how this can be done appear on
previous works on the provability of lower bounds in bounded arithmetic (see,
e.g., [30]), below we comment only on the part of the formalization that
affects the running time of computations obtained from proofs in
$\mathsf{IS}^{1}_{2}$.

For instance, the sentence $\mathsf{LB}^{\mathsf{exp}}(M,s,n_{0})$ can be
expressed as

$\forall N\,\forall n\,\forall D\,\exists x\,\Big{(}n=||N||\wedge n\geq
n_{0}\wedge|x|=n\wedge\mathsf{Circuit}_{s}(D,n)\rightarrow\mathsf{Error}_{M}(D,n,x)\Big{)}\;,$

where $\mathsf{Circuit}_{s}$ is a $\Sigma^{b+}_{1}$-formula that checks if $D$
is the description of a co-nondeterministic circuit of size at most $s(n)$,
and $\mathsf{Error}_{M}$ is built as a formula that checks if $M(x)\neq D(x)$.
Note that if $x$ is an $n$-bit number and $D$ encodes a circuit of size at
most $2^{n}$, a polynomial-time function $f$ over inputs $N$, $n$, and $D$
computes in time $\mathsf{poly}(|N|,|D|,|n|)=2^{O(n)}$. On the other hand,
when $s(n)\leq n^{k}$ for some $k$, we can take $n=|N|$ in the formalization
of $\mathsf{LB}^{\mathsf{poly}}(M,s,n_{0})$, which yields an algorithm from a
proof in $\mathsf{IS}^{1}_{2}$ whose running time is $\mathsf{poly}(n)$
instead of $\mathsf{poly}(2^{n})$.

We stress that our unprovability results do not depend on the specific
formulas employed to formalize the lower bound sentence. For more detailed
discussion, see Section 5.

###  2.2 Complexity theory

We assume basic familiarity with complexity theory, e.g., the definition of
complexity classes $\P,\NP$ and $\coNP$ (see [1]). We use
$\mathsf{NSIZE}[s(n)]$ (resp. $\mathsf{coNSIZE}[s(n)]$) to denote the set of
languages decidable by families of nondeterministic (resp. co-
nondeterministic) circuits of size $s(n)$.

#### Uniform circuits.

Let $\mathcal{C}$ be a non-uniform complexity class, e.g.,
$\mathcal{C}=\SIZE[\poly(n)]$ or $\mathcal{C}=\mathsf{NSIZE}[\poly(n)]$. We
say that $L\in\P\text{-}\mathsf{uniform}~{}\mathcal{C}$ if $L$ is decidable by
a family of $\mathcal{C}$-circuits
$\\{C_{n}:\\{0,1\\}^{n}\to\\{0,1\\}\\}_{n\in\mathbb{N}}$ such that there is a
polynomial-time Turing machine $M$ such that $M(1^{n})$ outputs the
description of $C_{n}$.

#### Refuters.

Let $L$ be a language, $R$ be a uniform algorithm, and $\mathcal{C}$ be a
complexity class. We often abuse notation and also view $\mathcal{C}$ as a
class of computational devices. We say that $R$ is a refuter for
$L\in\mathcal{C}$ (or a refuter for $L$ against $\mathcal{C}$) on input length
$n$ if, for every $E\in\mathcal{C}$, $R(1^{n},E)$ outputs $x\in\\{0,1\\}^{n}$
such that $E(x)\neq L(x)$. We extend this definition in the natural way when
$R$ represents a non-uniform family of circuits. In this case, we might omit
the input $1^{n}$ and simply write $R_{n}$.

##  3 Unprovability of Lower Bounds in $\mathsf{IS}^{1}_{2}$

In this section, we prove new results about refuters and employ them to
establish the unprovability of lower bounds against co-nondeterministic
circuits in theory $\mathsf{IS}^{1}_{2}$.

###  3.1 Unconditional lower bounds for refuters

In this section, we prove each item of Theorem 1.2 and establish some related
results needed in the proof of Theorem 1.1. First, we prove the following
lemma, which shows that _worst-case_ upper bounds can be extracted from
refuters, even in situations where the refuter runs in exponential time. This
result will be useful in the proof of Theorem 1.1 Item (_i_).

######  Lemma 3.1.

Let $L\in\mathsf{NP}$, and let $\delta>0$. Suppose that there is a uniform
algorithm $R(1^{n},D)$ such that, for every co-nondeterministic circuit $D$ on
$n$ input variables and of size at most $2^{n^{\delta}}$, $R(1^{n},D)$ runs in
time $2^{O(n)}$ and outputs a string $w\in\\{0,1\\}^{n}$ such that $D(w)\neq
L(w)$. Then, for every language $L^{\prime}\in\mathsf{NP}$ and for every
constant $\varepsilon>0$, we have
$L^{\prime}\in\mathsf{DTIME}[2^{n^{\varepsilon}}]$.

###### Proof.

Suppose that $L\in\mathsf{NTIME}[n^{d}]$ for some $d\in\mathbb{N}$. Let
$M^{\prime}$ be a nondeterministic machine that decides $L^{\prime}$ and runs
in time at most $n^{c^{\prime}}$, where $c^{\prime}\in\mathbb{N}$. Let
$\varepsilon>0$ be an arbitrary constant. Finally, let
$\gamma=\gamma(d,\varepsilon)>0$ be a small enough constant to be defined
later. We argue that the following deterministic algorithm $B^{\gamma}(x)$
decides $L^{\prime}$ in time $O(2^{n^{\varepsilon}})$:

  1. 1.

Let $x\in\\{0,1\\}^{n}$ be the input string.

  2. 2.

$B^{\gamma}$ computes the description of a co-nondeterministic circuit
$E^{\prime}$ of size at most $n^{2c^{\prime}}$ that decides the complement of
$L^{\prime}$. In other words, $E^{\prime}(u)=1-L^{\prime}(u)$ for every string
$u\in\\{0,1\\}^{n}$.

  3. 3.

$B^{\gamma}$ produces the code of a co-nondeterministic circuit $D_{x}(y)$,
where $y\in\\{0,1\\}^{n^{\gamma}}$, such that $D_{x}(y)$ ignores its input $y$
and computes according to $E^{\prime}(x)$.

(In other words, while the length of the main input string $y$ of $D_{x}(y)$
is smaller than the length of the main input string $u$ of $E^{\prime}(u)$,
they share the same non-deterministic input string, and $E^{\prime}$ sets $u$
to be the fixed string $x$.)

  4. 4.

$B^{\gamma}$ computes $w=R(1^{n^{\gamma}},D_{x})\in\\{0,1\\}^{n^{\gamma}}$.

  5. 5.

Finally, $B^{\gamma}$ determines the bit $b=L(w)$ by a brute force
computation, then sets $b$ as its output bit.

First, we argue that $B^{\gamma}$ decides $L^{\prime}$. Since $D_{x}$ is a co-
nondeterministic circuit over $m=n^{\gamma}$ input strings and of size at most
$n^{2c^{\prime}}=m^{2c^{\prime}/\gamma}\leq 2^{m^{\delta}}$ (for a large
enough $m$ and assuming that $\gamma$ is constant), $R(1^{n^{\gamma}},D_{x})$
outputs a string $w\in\\{0,1\\}^{n^{\gamma}}$ such that $L(w)=1-D_{x}(w)$.
Consequently,

$b=L(w)=1-D_{x}(w)=1-E^{\prime}(x)=1-(1-L^{\prime}(x))=L^{\prime}(x)\;,$

i.e., the output bit of $B(x)$ is correct.

Next, we argue that $B$ runs in time at most $O(2^{n^{\varepsilon}})$.
Clearly, Steps 1–3 all run in $\mathsf{poly}(n)$ time. Moreover, Step 4 runs
in time $2^{O(n^{\gamma})}$ under the assumption on the running time of
$R(1^{n^{\gamma}},D_{x})$. This is at most $2^{n^{\varepsilon}}$ if we set
$\gamma\leq\varepsilon/2$. Finally, since $L\in\mathsf{NTIME}[n^{d}]$, the
brute force computation in Step 5 can be performed in deterministic time
$2^{O(\ell^{d})}$ over an input of length $\ell$. Since $\ell=n^{\gamma}=|w|$
in our case, if $\gamma\leq\varepsilon/2d$ we get that Step $5$ runs in time
at most $2^{n^{\varepsilon}}$. Overall, if we set
$\gamma\triangleq\varepsilon/2d$, it follows that $B^{\gamma}$ runs in time at
most $O(2^{n^{\varepsilon}})$. This completes the proof that
$L^{\prime}\in\mathsf{DTIME}[2^{n^{\varepsilon}}]$.999We observe that, in the
proof of Lemma 3.1, it is enough for the refuter $R$ to work on co-
nondeterministic circuits of size $n^{\alpha(n)}$, where $\alpha(n)\to\infty$.
However, the formulation above will be sufficient for our purposes. ∎

In the proof of the next result, we employ a more sophisticated _bootstrapping
argument_ consisting of iterated applications of the refuter over different
input lengths. Recall that we use $\mathsf{SAT}_{n}$ to denote the
satisfiability problem for De Morgan Boolean formulas represented by $n$-bit
strings.

######  Theorem 3.2 (Restatement of Theorem 1.2 Item (_i_)).

Let $k$ and $c$ be rational numbers such that $1<k<c<k^{2}$. Then there is no
refuter $R(1^{n},E_{n})$ for $\mathsf{SAT}_{n}$ against
$E_{n}\in\mathsf{coNSIZE}[n^{k}]$ that has nonuniform circuit size $\leq
n^{c}$ and succeeds on every large enough input length $n$.

###### Proof.

In order to simplify some calculations, we prove the result for a fixed but
arbitrary language $L\in\mathsf{NTIME}[n]$. Since $\mathsf{poly}(\log n)$
overheads in our estimates do not affect the result, it is easy to check that
the same proof works for a language in
$\mathsf{NTIME}[n\cdot\mathsf{poly}(\log n)]$, such as
$\mathsf{SAT}=\\{\mathsf{SAT}_{n}\\}$. Similarly, we will tacitly assume that
machines of complexity $t$ can be simulated by circuit of size $t$ (instead of
$O(t\cdot\log t)$). Our construction and upper bounds can be easily adjusted
to account for these small overheads, since for constants $a<b$,
$n^{a}\cdot\mathsf{poly}(\log n)<n^{b}$ for every large enough $n$.

Let $1<k<c<k^{2}$, and let $M$ be a linear time nondeterministic machine that
decides $L$. Now consider an arbitrary $n_{0}\in\mathbb{N}$, and suppose
towards a contradiction that $R=\\{R_{\ell}\\}_{\ell\geq n_{0}}$ is a sequence
of nonuniform circuits $R_{\ell}$ of size $\leq\ell^{c}$ such that, given a
circuit $E_{\ell}\in\mathsf{coNSIZE}[\ell^{k}]$ over $\ell$ input bits,
$R_{\ell}(E_{\ell})$ outputs a string $x_{\ell}$ such that $M(x_{\ell})\neq
E_{\ell}(x_{\ell})$. We will prove the following claim.

######  Claim 3.3.

There is an input length $\ell_{0}\geq n_{0}$ and a deterministic circuit
$B_{\ell_{0}}$ of size at most $\ell_{0}^{k}$ that agrees with the language
$L$ over $\\{0,1\\}^{\ell_{0}}$, i.e., $B_{\ell_{0}}(x)=M(x)$ for all
$x\in\\{0,1\\}^{\ell_{0}}$.

Note that the existence of $B_{\ell_{0}}$ is in contradiction with the
existence of the refuter $R_{\ell_{0}}$, since there is no string
$x_{\ell_{0}}$ such that $B_{\ell_{0}}(x_{\ell_{0}})\neq M(x_{\ell_{0}})$.
Consequently, in order to complete the proof of Theorem 3.2, it is sufficient
to establish 3.3.

###### Proof of 3.3.

We will consider a large enough input length $\ell_{0}\geq n_{0}$ specified
later in the proof. Consider a deterministic circuit $B_{\ell_{0}}(x)$ that
computes as follows:101010We often write $M_{u}$ to emphasize that we run the
machine $M$ on inputs of length $u$.

  1. 1.

$B_{\ell_{0}}$ is given a string $x_{\ell_{0}}\in\\{0,1\\}^{\ell_{0}}$ as
input.

  2. 2.

It computes the description of a co-nondeterministic circuit $E_{\ell_{1}}(z)$
operating on inputs of length $\ell_{1}$ that ignores its input string $z$ and
satisfies $E_{\ell_{1}}(z)\triangleq\overline{M}_{\ell_{0}}(x_{\ell_{0}})$.

(The value $\ell_{1}<\ell_{0}$ will be defined below.)

  3. 3.

$B_{\ell_{0}}$ obtains $x_{\ell_{1}}\triangleq R_{\ell_{1}}(E_{\ell_{1}})$.

(Note that if $\mathsf{size}(E_{\ell_{1}})\leq\ell_{1}^{k}$ then
$M_{\ell_{1}}(x_{\ell_{1}})=1-E_{\ell_{1}}(x_{\ell_{1}})=1-\overline{M}_{\ell_{0}}(x_{\ell_{0}})=M_{\ell_{0}}(x_{\ell_{0}})$.)

  4. 4.

Finally, it computes $b_{\ell_{1}}\triangleq M_{\ell_{1}}(x_{\ell_{1}})$, and
uses this bit to decide $M_{\ell_{0}}(x_{\ell_{0}})$.

Let $t(\ell_{1})$ denote the circuit complexity of computing the bit
$b_{\ell_{1}}\triangleq M_{\ell_{1}}(x_{\ell_{1}})$ on an arbitrary input
$x_{\ell_{1}}$, i.e., the complexity of deciding if $x_{\ell_{1}}\in L$ over
strings of length $\ell_{1}$. As explained below, in order for $B_{\ell_{0}}$
to be correct and of the desired size, it is sufficient that:

  * •

$\mathsf{size}(E_{\ell_{1}})\approx\ell_{0}\leq\ell_{1}^{k}$ (i.e., the
refuter receives a circuit of bounded size in Step 3), where we have used that
$M$ runs in nondeterministic linear time and omitted polylog factors.

(In our analysis below, we can assume that the description of $E_{\ell_{1}}$
can be computed in size at most $\ell_{0}^{k}/4$, since $k>1$ and $M$ runs in
linear time.)

  * •

We need that $\ell_{1}\geq n_{0}$, so the output of
$R_{\ell_{1}}(E_{\ell_{1}})$ is defined in Step $3$.

  * •

The circuit size of the refuter in Step $3$, which is upper bounded by
$\ell_{1}^{c}$, satisfies $\ell_{1}^{c}\leq\ell_{0}^{k}/4$.

  * •

The circuit size $t(\ell_{1})$ needed to compute $b_{\ell_{1}}$ satisfies
$t(\ell_{1})\leq\ell_{0}^{k}/4$.

If these conditions are met, $B_{\ell_{0}}(x)=M(x)$ for all
$x\in\\{0,1\\}^{\ell_{0}}$, and its overall size $t(\ell_{0})$ is strictly
less than $\ell_{0}^{k}$ (with some room to spare that will be handy later in
the proof), since

$t(\ell_{0})\leq\ell_{0}^{k}/4+\ell_{0}^{k}/4+t(\ell_{1})\leq\ell_{0}^{k}/4+\ell_{0}^{k}/4+\ell_{0}^{k}/4<\ell_{0}^{k}.$

Constraints. The conditions described above yield the following inequalities
(omitting some small order factors):

$\ell_{0}^{1/k}\leq\ell_{1}\leq\ell_{0}^{k/c}\;\;(\text{thus}~{}c<k^{2})\quad\text{and}\quad
t(\ell_{1})\leq\ell_{0}^{k}/4.$

Recall that the condition $c<k^{2}$ is one of our assumptions. Jumping ahead,
we will define $\ell_{1}$ as a function of $\ell_{0}$, $k$, and $c$, and
employ a recursive approach to compute $b_{\ell_{1}}$ so that the conditions
are satisfied.

Key insight. Note that in order to compute
$b_{\ell_{1}}=M_{\ell_{1}}(x_{\ell_{1}})$ we must solve the _same problem_ on
a _smaller input length_ , i.e., we would like to design a circuit
$B_{\ell_{1}}$ that computes $L$ on input length $\ell_{1}\ll\ell_{0}$.
Consequently, using that we have refuter circuits for all input lengths $\geq
n_{0}$, it is enough to iterate the same construction!

Recursion. The circuit $B_{\ell_{1}}$ computes analogously to $B_{\ell_{0}}$,
by considering a smaller input length $\ell_{2}\ll\ell_{1}$ and a
corresponding co-nondeterministic circuit $B_{\ell_{2}}$. Similarly to the
analysis from above, we obtain the following constraints to guarantee its
correctness and the desired circuit size bound (again omitting small order
factors to focus on the relevant asymptotics):

$\mathsf{size}(E_{\ell_{2}})\approx\ell_{1}\leq\ell_{2}^{k}\quad\text{and}\quad\ell_{2}^{c}\leq\ell_{1}^{k}/4\quad\text{and}\quad
t(\ell_{2})\leq\ell_{1}^{k}/4.$

This forces that

$\ell_{1}^{1/k}\leq\ell_{2}\leq\ell_{1}^{k/c}\quad\text{and}\quad
t(\ell_{1})\leq\ell_{1}^{k}/4+\ell_{1}^{k}/4+t(\ell_{2})<3\cdot\ell_{1}^{k}/4\leq\ell_{0}^{k}/4,$

where we assumed that $t(\ell_{2})\leq\ell_{1}^{k}/4$ and used that
$\ell_{1}\ll\ell_{0}$. In other words, we need

$\ell_{1}^{1/k}\leq\ell_{2}\leq\ell_{1}^{k/c}\;\;(\text{thus}~{}c<k^{2})\quad\text{and}\quad
t(\ell_{2})\leq\ell_{1}^{k}/4.$

Parameters and base case. Consider the input lengths
$\ell_{0}>\ell_{1}>\ldots>\ell_{d}$ explored in this way, together with the
corresponding circuits $B_{\ell_{0}},\ldots,B_{\ell_{d}}$, where each
$B_{\ell_{i}}$ contains $B_{\ell_{i+1}}$ as a subroutine. In other words,
$B_{\ell_{0}}$ appears close to the input string, followed by $B_{\ell_{1}}$,
and so on. (The string $x_{\ell_{i+1}}$ computed by $B_{\ell_{i}}$ serves as
the input string to $B_{\ell_{i}}$.) We start with an input length $\ell_{0}$
sufficiently larger than $n_{0}$ so that all calls to the non-uniform refuter
$R$ consider input lengths not smaller than $n_{0}$. In order to satisfy the
inequalities from above, our parameters are defined as follows:

_– Sequence of input lengths._ We let $\ell_{i+1}\triangleq\ell_{i}^{1/k}$.
Therefore, $\ell_{d}=\ell_{0}^{1/k^{d}}$.

_– Number of stages._ We take $d$ large enough, so that
$\ell_{d}=\ell_{0}^{1/k^{d}}=\log\ell_{0}$, i.e.,
$d\triangleq(\log\log\ell_{0}-\log\log\ell_{d})/\log k=O(\log\log\ell_{0})$.

_– Initial input length $\ell_{0}$._ We want $\ell_{d}=\log\ell_{0}\geq
n_{0}$, so we set $\ell_{0}\triangleq 2^{n_{0}}$.

In the base case (input length $\ell_{d}$ and circuit $B_{\ell_{d}}$), we
simply consult the hardcoded truthtable of the language $L$ computed by
machine $M$ on inputs of length $\ell_{d}=\log\ell_{0}$. The truthtable of $L$
on input length $\log\ell_{0}$ can be nonuniformly stored using $\ell_{0}$
bits. This can be seen as an overhead in the final size of $B_{\ell_{0}}$ that
is of order $\ell_{0}\leq\ell_{0}^{k}/4$, where this inequality uses that
$k>1$ and assumes that $\ell_{0}\geq n_{0}$ is large enough. Since the overall
size bound for $B_{\ell_{0}}$ is given by a simple additive function obtained
from the concatenation of a sequence of circuits, it is not hard to see that
its total size is at most $\ell_{0}^{k}$, as desired. ∎

As explained above, this completes the proof of Theorem 3.2. ∎

The next lemma will be used in the proof of Theorem 1.1 Item (_ii_).

######  Lemma 3.4.

Let $L\in\NTIME[n^{c}]$ for some constant $c\geq 1$. If there is a polynomial-
time refuter $R$ for the lower bound
$L\notin\mathsf{i.o.}\text{-}\mathsf{coNSIZE}[s(n)]$ for some monotone time-
constructible function $s\colon\mathbb{N}\to\mathbb{N}$ such that
$\omega(n^{c}\cdot\log n)\leq s(n)\leq\poly(n)$, then $L\in\P$.

###### Proof.

The proof is similar to the construction described above. Consider the
following polynomial-time algorithm that aims to solve $L$. On a given input
instance $x\in\\{0,1\\}^{n}$ for $L$, we construct a
$\mathsf{coNSIZE}[O(n^{c}\cdot\log n)]$-circuit
$D_{x}:\\{0,1\\}^{n/2}\times\\{0,1\\}^{n^{c}}\to\\{0,1\\}$ of the form
$D_{x}(u,v)$ (where $v$ is the nondeterministic input string) that ignores its
primary input $u\in\\{0,1\\}^{n/2}$ and computes according to
$\overline{L}(x)$. Since $L\in\mathsf{NTIME}[n^{c}]$, the transformation from
machines to circuits guarantees that $D_{x}(u,\cdot)$ is a co-nondeterministic
circuit of size at most $O(n^{c}\cdot\log n)\leq s(n/2)$, assuming that $n$ is
sufficiently large. Moreover, a description of $D_{x}$ can be computed from
$x$ and from the nondeterministic machine for $L$ in time polynomial in $n$.

Using the polynomial-time refuter $R$ on input $(1^{n/2},D_{x})$ and the size
upper bound for $D_{x}$, we can find a string $z_{1}\in\\{0,1\\}^{n/2}$ such
that $D_{x}(z_{1})\neq L(z_{1})$. Using the definition of the circuit $D_{x}$,
which as a co-nondeterministic circuit satisfies $D_{x}(u)=1-L(x)$ for every
input $u\in\\{0,1\\}^{n/2}$, this implies that

$L(z_{1})=1-D_{x}(z_{1})=1-(1-L(x))=L(x)\;.$

To sum up, in time polynomial in $n$, we have reduced the problem of deciding
$L$ on $x\in\\{0,1\\}^{n}$ to that of deciding $L$ on
$z_{1}\in\\{0,1\\}^{n/2}$. We now recursively evaluate $L(z_{1})$ in a similar
fashion until the input length is smaller than a large enough constant $C$. In
other words, we produce a sequence $z_{1},\ldots,z_{k}$ of inputs, where each
$|z_{i}|=n/2^{i}$, $k\leq\log n$, $|z_{k}|\leq C$, and

$L(x)=L(z_{1})=\ldots=L(z_{k})\;.$

Since $L(z_{k})$ can be computed in constant time by brute force and there are
at most $\log n$ stages of the recursion, it follows that we can decide $L(x)$
in time polynomial in $n=|x|$, i.e., $L\in\mathsf{P}$. ∎

We can also obtain the following consequence.

######  Theorem 3.5 (Restatement of Theorem 1.2 Item (_ii_)).

There is an integer $k\geq 1$ such that there is no refuter $R(1^{n},E_{n})$
for $\mathsf{SAT}_{n}$ against $E_{n}\in\mathsf{coNSIZE}[n^{k}]$ of nonuniform
polynomial size which succeeds on every large enough input length.

###### Proof.

Assume such a polynomial size refuter exists for $k=2$, since we are done
otherwise. Using that $\mathsf{SAT}\in\mathsf{NTIME}[n\cdot\mathsf{poly}(\log
n)]$ and arguing as in the proof of Lemma 3.4, it follows that there is a
constant $c\in\mathbb{N}$ and a sequence of non-uniform circuits of size
$n^{c}$ that compute $\mathsf{SAT}_{n}$ on every large enough input length
$n$. But then there is no refuter witnessing that
$\mathsf{SAT}_{n}\notin\mathsf{coNSIZE}[n^{k}]$ when $k=c+1$, since this lower
bound is simply false when the input length is large enough. ∎

###  3.2 Unprovability of lower bounds via refuter lower bounds

In this section, we prove each item of Theorem 1.1. We will need the following
witnessing result for the intuitionistic theory $\mathsf{IS}^{1}_{2}$.

######  Theorem 3.6 (Witnessing Theorem for $\mathsf{IS}^{1}_{2}$ [7, 16]).

Let $\varphi$ be an arbitrary formula, and suppose that

$\mathsf{IS}^{1}_{2}\vdash\forall x\;\exists y~{}\varphi(x,y)\,.$

Then there is a polynomial-time computable function $f$ such that

$\mathbb{N}\models\forall a~{}\varphi(a,f(a))\,.$

Furthermore, there is a $\Sigma^{b+}_{1}$-formula $\psi(x,y)$ such that:

  * _(_i_)_

$\mathsf{IS}^{1}_{2}\vdash\forall x\,\forall
y\,(\psi(x,y)\rightarrow\varphi(x,y))\,$.

  * _(_ii_)_

$\mathsf{IS}^{1}_{2}\vdash\forall x\,\forall y\,\forall
z\,(\psi(x,y)\wedge\psi(x,z)\rightarrow y=z)\,$.

  * _(_iii_)_

$\mathsf{IS}^{1}_{2}\vdash\forall x\,\exists y\,\psi(x,y)\,$.

In particular, Theorem 3.6 shows that the outermost existential quantifier of
a sentence of arbitrary quantifier complexity provable in
$\mathsf{IS}^{1}_{2}$ can be efficiently witnessed by a polynomial-time
function.

######  Theorem 3.7 (Restatement of Theorem 1.1 Part (_i_)).

Let $\delta>0$ be a rational number, $n_{0}\in\mathbb{N}$, and $M$ be a
polynomial-time nondetermistic machine. Then
$\mathsf{IS}^{1}_{2}\nvdash\mathsf{LB}^{\mathsf{exp}}(M,2^{n^{\delta}},n_{0})\;.$

###### Proof.

We argue by contradiction. Under the assumption that

$\mathsf{IS}^{1}_{2}\vdash\mathsf{LB}^{\mathsf{exp}}(M,2^{n^{\delta}},n_{0})$

for a choice of $M$, $\delta>0$, and $n_{0}$, it follows from Theorem 3.6 that
there is a refuter $R(1^{n},D)$ that runs in time $2^{O(n)}$ and outputs an
input $x\in\\{0,1\\}^{n}$ such that $\mathsf{Error}_{M}(D,n,x)$, whenever $D$
is a co-nondeterministic circuit of size at most $2^{n^{\delta}}$ and $n\geq
n_{0}$. By Lemma 3.1, for any choice of $\varepsilon>0$, we get that
$L(M)\in\mathsf{DTIME}[2^{n^{\varepsilon}}]$. Taking $\varepsilon<\delta$,
this upper bound and the provability of
$\mathsf{LB}^{\mathsf{exp}}(M,2^{n^{\delta}},n_{0})$ contradict the soundness
of $\mathrm{IS}^{1}_{2}$. ∎

######  Theorem 3.8 (Restatement of Theorem 1.1 Part (_ii_)).

Let $n_{0}\in\mathbb{N}$ and $M$ be a polynomial-time nondetermistic machine.
Then there is an integer $k\geq 1$ such that
$\mathsf{IS}^{1}_{2}\nvdash\mathsf{LB}^{\mathsf{poly}}(M,n^{k},n_{0})\;.$

###### Proof.

Let $n^{c}$ be an upper bound on the nondeterministic time complexity of $M$.
Towards a contradiction, assume that
$\mathsf{IS}^{1}_{2}\vdash\mathsf{LB}^{\mathsf{poly}}(M,n^{k},n_{0})$ for
every $k\geq 1$. In particular, this holds for $k=2c$. It follows from Theorem
3.6 that there is a refuter $R(1^{n},D)$ that runs in time $\mathsf{poly}(n)$
and outputs an input $x\in\\{0,1\\}^{n}$ such that
$\mathsf{Error}_{M}(D,n,x)$, whenever $D$ is a co-nondeterministic circuit of
size at most $n^{k}$ and $n\geq n_{0}$. Consequently, by Lemma 3.4, we get
that $L(M)\in\P$. In particular, the sentence
$\mathsf{LB}^{\mathsf{poly}}(M,n^{k},n_{0})$ is _false_ for some large enough
constant $k$. This and the assumption that
$\mathsf{IS}^{1}_{2}\vdash\mathsf{LB}^{\mathsf{poly}}(M,n^{k},n_{0})$ for
every $k\geq 1$ contradict the soundness of $\mathsf{IS}^{1}_{2}$. ∎

##  4 Unprovability of Upper Bounds in $\mathsf{IS}^{1}_{2}$

In this section, we prove unconditionally that a natural formalization of the
circuit _upper bound_ $\NP\subseteq\mathsf{coNSIZE}[n^{k}]$ is unprovable in
$\mathsf{IS}^{1}_{2}$, for every fixed constant $k$.

###  4.1 Unconditional uniform lower bound against co-nondeterministic
circuits

We first prove that
$\NP\nsubseteq\mathsf{P}\text{-}\mathsf{uniform}~{}\mathsf{coNSIZE}[n^{k}]$,
for every constant $k$. That is, for each $k$, there is a language $L\in\NP$
that cannot be decided by any polynomial-time uniform family of co-
nodeterministic circuits of size $n^{k}$. This uniform lower bound is obtained
though an adaptation of a technique of Santhanam and Williams [34] showing
that $\P\nsubseteq\mathsf{P}\text{-}\mathsf{uniform}~{}\SIZE[n^{k}]$.

coNTIME

First, we will need the following standard “no complementary speedup theorem”.

######  Theorem 4.1 (Folklore).

For every constant $b\geq 1$,
$\coNTIME[n^{b+1}]\nsubseteq\NTIME[n^{b}]_{/o(n)}$.

###### Proof Sketch.

Fix any constant $b\geq 1$. Consider the following co-nondeterministic Turing
machine $M$ that runs in time $O(n^{b+1})$: On any input of the form
$x=(\hat{M},\alpha,\pi)\in\\{0,1\\}^{n}$, where $\hat{M}$ is interpreted as
the encoding of a (clocked) nondeterministic Turing machine running in time
$O(n^{b})$, $\alpha_{n}$ is interpreted as the advice to $\hat{M}$ on input
length $n$, and $\pi\in\\{0\\}^{*}$ is a padding string, $M$ simulates
$\hat{M}(x)_{\alpha_{n}}$ (i.e., $\hat{M}$ on input $x$ with advice string
$\alpha_{n}$) and accepts if and only if $\hat{M}(x)_{\alpha_{n}}$ rejects. It
is not hard to show that the language $L(M)\notin\NTIME[n^{b}]_{/o(n)}$. ∎

Next, we introduce an auxiliary definition and establish a proposition that
will be useful.

pDCL nDCL

######  Definition 4.2.

Let $C=\\{C_{n}\\}_{n\geq 1}$ be a family of polynomial-size nondeterministic
circuits, and $m=m(n)$ be a constructive function. The positive and negative
$m$-padded _direct connect language_ for $C$, short for $m\text{-}\pDCL(C)$
and $m\text{-}\nDCL(C)$, are defined as follows:

$\displaystyle m\text{-}\pDCL(C)\triangleq\\{(n,1^{m},i)\mid\langle
C_{n}\rangle_{i}=1\\},$ $\displaystyle
m\text{-}\nDCL(C)\triangleq\\{(n,1^{m},i)\mid\langle C_{n}\rangle_{i}=0\\},$

where $\langle C_{n}\rangle$ is the string that encodes the circuit $C_{n}$.

######  Proposition 4.3.

If $C=\\{C_{n}\\}_{n\geq 1}$ is a $\mathsf{P}\text{-}\mathsf{uniform}$ family
of _(_ nondeterministic _)_ circuits, the padded direct connect languages
$n^{\varepsilon}\text{-}\pDCL(C),n^{\varepsilon}\text{-}\nDCL(C)\in\P$ for any
fixed constant $\varepsilon\in(0,1)$.

###### Proof.

Given $(n,1^{n^{\varepsilon}},i)$, one can first print the description
$y=\langle C_{n}\rangle$ of $C_{n}$ in $\poly(n)$ time, then check whether the
$i$-th bit is $0$ or $1$. Since the input length is at least
$n^{\varepsilon}$, this algorithm runs in polynomial time. ∎

######  Theorem 4.4.

For every positive integer $k$,
$\NP\nsubseteq\mathsf{P}\text{-}\mathsf{uniform}~{}\mathsf{coNSIZE}[n^{k}]$.

###### Proof.

We argue that
$\coNP\nsubseteq\mathsf{P}\text{-}\mathsf{uniform}~{}\mathsf{NSIZE}[n^{k}]$.
The theorem follows from this separation by a simple complementation argument.
Let $k$ be any constant, and $H_{b}$ be the hard language in Theorem 4.1 for
some $b>k$ to be determined later. Towards a contradiction, we assume that for
every language $L\in\coNP$, there is a family of
$\mathsf{P}\text{-}\mathsf{uniform}$ nondeterministic circuits
$C=\\{C_{n}\\}_{n\geq 1}$ of size $cn^{k}$ that decides $L$, where $c$ is an
arbitrary constant that can depend on $L$. In particular, this uniform fixed
polynomial upper bound holds for $H_{b}$. We will use the fixed polynomial
upper bound for $\coNP$ to optimize $H_{b}$ to the extent that it violates
Theorem 4.1.

  1. 1.

(_Pad Down_). Let $\varepsilon\triangleq 1/2k$ and $C=\\{C_{n}\\}_{n\geq 1}$
be the $\mathsf{P}\text{-}\mathsf{uniform}$ family of nondeterministic
circuits of size $cn^{k}$ that decides $H_{b}$. By Proposition 4.3, we know
that $n^{\varepsilon}\text{-}\pDCL(C)$ and $n^{\varepsilon}\text{-}\nDCL(C)$
are in $\P$, and therefore also in $\coNP$.

  2. 2.

(_Compress_ $C_{n}$). Let $m=m(n)\leq O(\log n)+n^{\varepsilon}$ be the length
of the input $(n,1^{n^{\varepsilon}},i)$ for $n^{\varepsilon}\text{-}\pDCL(C)$
and $n^{\varepsilon}\text{-}\nDCL(C)$. Since
$n^{\varepsilon}\text{-}\pDCL(C)\in\coNP$, by the upper bound for $\coNP$, we
get that there is a family of nondeterministic circuits
$D^{p}=\\{D^{p}_{m}\\}_{m\geq 1}$ of size $c^{\prime}m^{k}$ that decides
$n^{\varepsilon}\text{-}\pDCL(C)$. Similarly, there is a family of
nondeterministic circuits $D^{n}=\\{D^{n}_{m}\\}_{m\geq 1}$ of size
$c^{\prime\prime}m^{k}$ that decides $n^{\varepsilon}\text{-}\nDCL(C)$. Note
that the sizes of both circuits $D^{p}_{m}$ and $D^{n}_{m}$ are $O(m^{k})\leq
O(n^{\varepsilon k})=O(\sqrt{n})$, which gives a succinct representation of
$C_{n}$.

  3. 3.

(_Speedup with Advice_). Now we speedup the computation of $H_{b}$ with
$C_{n}$, $D^{p}_{m}$, and $D^{n}_{m}$. Let $M^{\prime}_{/\alpha_{n}}$ be the
following nondeterministic algorithm with advice $\\{\alpha_{n}\\}_{n\geq 1}$
of length $o(n)$:

     * •

The advice is defined as $\alpha_{n}\triangleq(D_{m}^{p},D_{m}^{n})$.

     * •

Let $\alpha_{n}=(D_{m}^{p},D^{m}_{n})$ be the advice and $x\in\\{0,1\\}^{n}$
be the input. Let $\ell\triangleq|\langle C_{n}\rangle|$. Note that since
$C_{n}$ is of size $O(n^{k})$, $\ell\leq\tilde{O}(n^{k})$. The algorithm
nondeterministically guesses a string $y\in\\{0,1\\}^{\ell}$ for every
$i\in[\ell]$, then verifies that for every $i\in[\ell]$, $y_{i}=\langle
C_{n}\rangle_{i}$. Concretely, for every $i\in[\ell]$, the algorithm works as
follows: if $y_{i}=1$, it simulates $D_{m}^{p}(n,1^{n^{\varepsilon}},i)$ and
immediately rejects if $D_{m}^{p}$ rejects; otherwise, the algorithm simulates
$D_{m}^{n}(n,1^{n^{\varepsilon}},i)$ and immediately rejects if $D_{m}^{n}$
rejects. Note that since both $D_{m}^{p}$ and $D_{m}^{n}$ are nondeterministic
circuits of size $O(\sqrt{n})$, the running time for this step is
$O(\ell)+\tilde{O}(\sqrt{n})=\tilde{O}(n^{k})$. After this step, we know that
$y=\langle C_{n}\rangle$.

     * •

Finally, the algorithm simulates $C_{n}(x)$, which takes $\tilde{O}(n^{k})$
time.

In summary, this algorithm takes an advice of length $o(n)$ and simulates
$C_{n}(x)$ in time $\tilde{O}(n^{k})$. Since $C_{n}$ decides $H_{b}$, this
algorithm also decides $H_{b}$. Therefore, $H_{b}\in\NTIME[n^{k+1}]_{/o(n)}$.

This leads to a contradiction by choosing $b=k+2$. ∎

###  4.2 Unprovability of upper bounds via uniform lower bounds

We now combine the uniform lower bound (Theorem 4.4) and the witnessing
theorem for $\mathsf{IS}^{1}_{2}$ (Theorem 3.6) to establish the unprovability
of $\NP\subseteq\mathsf{coNSIZE}[n^{k}]$ in $\mathsf{IS}^{1}_{2}$. First, we
explain how to formalize this upper bound statement. This is similar to a
formalization in [22].

#### Formalization.

The fixed polynomial circuit upper bound $\NP\subseteq\mathsf{coNSIZE}[n^{k}]$
states that for every polynomial-time nondeterministic Turing machine $M$ and
every input length $n$, there is a co-nondeterministic circuit $C$ of size
$O(n^{k})$ such that $C(x)=M(x)$. For each $k$, we capture the upper bound
statement using a collection of sentences

$``\NP\subseteq\mathsf{coNSIZE}[n^{k}]"\triangleq\\{\mathsf{UB}_{M}(k,c)\mid
M\text{ is an }\NP\text{ machine and}~{}c\in\mathbb{N}\\},$

where $\mathsf{UB}_{M}(k,c)$ is the sentence:

$\displaystyle\mathsf{UB}_{M}(k,c)\triangleq\forall n\in\mathsf{Log}~{}\exists
C\in\mathsf{coNSIZE}[cn^{k}]~{}\forall
x\in\\{0,1\\}^{n}~{}\lnot\mathsf{Error}_{M}(C,n,x).$

The sentence $\mathsf{UB}_{M}(k,c)$ can be expressed in a natural way,
similarly to the lower bound sentence $\mathsf{LB}^{\mathsf{poly}}$ described
in Section 2.1.

For a fixed $k$, we say that a theory $T$ proves
$``\NP\subseteq\mathsf{coNSIZE}[n^{k}]"$ if for every polynomial-time
nondeterministic Turing machine $M$ there is a constant $c$ such that
$T\vdash\mathsf{UB}_{M}(k,c)$.

We are now ready to prove the main result of this section.

######  Theorem 4.5.

For every $k\in\mathbb{N}$,
$\mathsf{IS}^{1}_{2}\nvdash``\NP\subseteq\mathsf{coNSIZE}[n^{k}]"$.

###### Proof.

Towards a contradiction, we assume that
$\mathsf{IS}^{1}_{2}\vdash``\NP\subseteq\mathsf{coNSIZE}[n^{k}]"$ for some
$k\in\mathbb{N}$, that is, for every $\NP$ machine $M$ there is a constant
$c_{M}$ such that $\mathsf{IS}^{1}_{2}\vdash\mathsf{UB}_{M}(k,c_{M})$. For
convenience, we write

$\mathsf{UB}_{M}(k,c)=\forall n\in\mathsf{Log}~{}\exists
C\in\mathsf{coNSIZE}[c_{M}n^{k}]~{}\varphi(n,C),$

where $\varphi(n,C)\triangleq\forall
x\in\\{0,1\\}^{n}~{}\lnot\mathsf{Error}_{M}(C,n,x)$. By the witnessing theorem
for $\mathsf{IS}^{1}_{2}$ (Theorem 3.6), for each $\NP$ machine $M$, there is
a polynomial-time algorithm $A_{M}$ that takes $1^{n}$ as input and outputs a
co-nondeterministic circuit $C_{n}$ of size at most $c_{M}n^{k}$ such that
$\varphi(n,C_{n})$ holds in the standard model $\mathbb{N}$. In other words,
$C=\\{C_{n}\\}_{n\geq 1}$ is a $\mathsf{P}$-uniform co-nondeterministic
circuit family that decides $L(M)$. (Note that the algorithm takes $1^{n}$
instead of $n$ as input as $\forall n\in\mathsf{Log}$ is a shorthand for
$\forall v~{}\forall n=|v|$.) This immediately implies that every language in
$\NP$ can be computable by a $\P$-uniform family of co-nondeterministic
circuits of size $O(n^{k})$, which is impossible by Theorem 4.4. ∎

##  5 Interpretation and Generalization of Our Results

We make two remarks about the interpretation and generalization of our
results.

#### Interpretation of the unprovability results.

In this paper, we established the unprovability of both co-nondeterministic
circuit size upper bounds and lower bounds in the intuitionistic theory
$\mathsf{IS}^{1}_{2}$. Roughly speaking, the standard interpretation of the
results is that the question of whether $\NP$ requires large co-
nondeterministic circuits cannot be constructively resolved, either because of
the _lack of relevant non-logical axioms_ or because of _the absence of the
law of excluded middle_.

Due to the nature of intuitionistic logic, it could still be the case that
while $\NP\subseteq\mathsf{coNSIZE}[n^{k}]$ is unprovable in
$\mathsf{IS}^{1}_{2}$, $\lnot\lnot``\NP\subseteq\mathsf{coNSIZE}[n^{k}]"$ is
indeed provable in $\mathsf{IS}^{1}_{2}$, as $\lnot\lnot\varphi\vdash\varphi$
is not an admissible inference rule in intuitionistic logic. As explained in
more detail next, our results can be considered necessary steps towards the
classical independence of worst-case lower bounds. (See also [9, Section 6.2]
for related considerations in a different context.)

#### Robustness of our unprovability results.

Recall that the proofs of our unprovability results in Theorem 3.7, Theorem
3.8, and Theorem 4.5 only rely on the soundness of $\mathsf{IS}^{1}_{2}$ over
the standard model and on the witnessing theorem to extract a polynomial-time
algorithm for the _outermost existential quantifier_. Therefore, the
unprovability result holds even if one substitutes a subformula of the lower
bound or upper bound sentences inside the outermost existential quantifier by
any formula that coincides with the intended meaning over the standard model
$\mathbb{N}$.

In particular, the unprovability result holds even if any subformula inside
the outermost existential quantifier is replaced by any classically equivalent
formula. This suggests that our unprovability result holds in “semi-classical”
setting, i.e., classical reasoning is allowed inside the outermost existential
quantifier.

A more formal way to phrase the observation is via the well-known _double-
negation translation_ (i.e. Gödel–Gentzen translation). The double-negation
translation of a first-order sentence $\varphi$, denoted by
$\varphi^{\mathsf{N}}$, is defined inductively by the following rules:

  * •

$A^{\mathsf{N}}\triangleq\lnot\lnot A$ for atomic $A$ (i.e. $A$ is a
predicate);

  * •

$(\varphi\land\psi)^{\mathsf{N}}\triangleq\varphi^{\mathsf{N}}\land\psi^{\mathsf{N}}$;
$(\lnot\varphi)^{\mathsf{N}}\triangleq\lnot\varphi^{\mathsf{N}}$;
$(\varphi\to\psi)^{\mathsf{N}}\triangleq\varphi^{\mathsf{N}}\to\psi^{\mathsf{N}}$;

  * •

$(\varphi\lor\psi)^{\mathsf{N}}\triangleq\lnot\lnot(\varphi^{\mathsf{N}}\lor\psi^{\mathsf{N}})$;

  * •

$(\forall x~{}\varphi)^{\mathsf{N}}\triangleq\forall
x~{}\varphi^{\mathsf{N}}$;

  * •

$(\exists x~{}\varphi)^{\mathsf{N}}\triangleq\lnot\lnot\exists
x~{}\varphi^{\mathsf{N}}$.

For a set $\Pi$ of formulas, we define
$\Pi^{\mathsf{N}}\triangleq\\{\varphi^{\mathsf{N}}\mid\varphi\in\Pi\\}$.

######  Theorem 5.1 (see, e.g., [11]).

For a set $\Pi$ of formulas and a formula $\varphi$, $\Pi$ proves $\varphi$
classically if and only if $\Pi^{\mathsf{N}}$ proves $\varphi^{\mathsf{N}}$
intuitionistically. In particular, $\varphi$ and $\psi$ are classically
equivalent if and only if $\varphi^{\mathsf{N}}$ and $\psi^{\mathsf{N}}$ are
intuitionistically equivalent.

######  Corollary 5.2.

In Theorem 3.7, Theorem 3.8, and Theorem 4.5, the corresponding unprovability
result holds even if the subformula inside the outermost existential
quantifier is replaced by its double-negation translation.

## References

  * AB [09] Sanjeev Arora and Boaz Barak.  Computational Complexity - A Modern Approach.  Cambridge University Press, 2009.
  * ABM [23] Albert Atserias, Sam Buss, and Moritz Müller.  On the consistency of circuit lower bounds for non-deterministic time.  In Symposium on Theory of Computing _(STOC)_ , pages 1257–1270, 2023.
  * Avi [00] Jeremy Avigad.  Interpreting classical theories in constructive ones.  Journal of Symbolic Logic, 65(4):1785–1812, 2000.
  * BKO [20] Jan Bydzovsky, Jan Krajíček, and Igor C. Oliveira.  Consistency of circuit lower bounds with bounded theories.  Logical Methods in Computer Science, 16(2), 2020.
  * BM [20] Jan Bydzovsky and Moritz Müller.  Polynomial time ultrapowers and the consistency of circuit lower bounds.  Arch. Math. Log., 59(1-2):127–147, 2020.
  * [6] Samuel R. Buss.  Bounded Arithmetic.  Bibliopolis, 1986.
  * [7] Samuel R. Buss.  The polynomial hierarchy and intuitionistic bounded arithmetic.  In Structure in Complexity Theory _(CCC)_ , pages 77–103, 1986\.
  * [8] Samuel R. Buss.  A note on bootstrapping intuitionistic bounded arithmetic.  Proof Theory: a selection of papers from the Leeds Theory Programme, pages 142–169, 1990.
  * [9] Samuel R. Buss.  On model theory for intuitionistic bounded arithmetic with applications to independence results.  In Feasible Mathematics: A Mathematical Sciences Institute Workshop, Ithaca, New York, June 1989, pages 27–47. Springer, 1990.
  * Bus [97] Samuel R. Buss.  Bounded arithmetic and propositional proof complexity.  In Logic of Computation, pages 67–121. Springer Berlin Heidelberg, 1997.
  * Bus [98] Samuel R. Buss.  Handbook of Proof Theory.  Elsevier, 1998.
  * CH [99] Thierry Coquand and Martin Hofmann.  A new method for establishing conservativity of classical systems over their intuitionistic version.  Mathematical Structures in Computer Science, 9(4):323–333, 1999\.
  * CJSW [21] Lijie Chen, Ce Jin, Rahul Santhanam, and Ryan Williams.  Constructive separations and their consequences.  In Symposium on Foundations of Computer Science _(FOCS)_ , 2021\.
  * CK [07] Stephen A. Cook and Jan Krajíček.  Consequences of the provability of $\mathsf{NP}\subseteq\mathsf{P}/\mathsf{poly}$.  Journal of Symbolic Logic, 72(4):1353–1371, 2007.
  * CKKO [21] Marco Carmosino, Valentine Kabanets, Antonina Kolokolova, and Igor C. Oliveira.  Learn-uniform circuit lower bounds and provability in bounded arithmetic.  In Symposium on Foundations of Computer Science _(FOCS)_ , 2021\.
  * CU [93] Stephen Cook and Alasdair Urquhart.  Functional interpretations of feasibly constructive arithmetic.  Annals of Pure and Applied Logic, 63(2):103–200, 1993.
  * FM [98] Fernando Ferreira and António Marques.  Extracting algorithms from intuitionistic proofs.  Mathematical Logic Quarterly, 44:143–160, 1998.
  * GP [13] Kaveh Ghasemloo and Ján Pich.  A note on natural proofs and intuitionism.  Manuscript, 2013.
  * GST [07] Dan Gutfreund, Ronen Shaltiel, and Amnon Ta-Shma.  If NP languages are hard on the worst-case, then it is easy to find their hard instances.  Comput. Complex., 16(4):412–441, 2007.
  * Har [92] Victor Harnik.  Provably total functions of intuitionistic bounded arithmetic.  Journal of Symbolic Logic, 57(2):466–477, 1992.
  * Jeř [17] Emil Jeřábek.  Proof complexity of intuitionistic implicational formulas.  Annals of Pure and Applied Logic, 168(1):150–190, 2017.
  * KO [17] Jan Krajíček and Igor C. Oliveira.  Unprovability of circuit upper bounds in Cook’s theory PV.  Logical Methods in Computer Science, 13(1), 2017.
  * Koh [08] Ulrich Kohlenbach.  Applied Proof Theory - Proof Interpretations and their Use in Mathematics.  Springer Monographs in Mathematics. Springer, 2008.
  * KP [89] Jan Krajíček and Pavel Pudlák.  Propositional provability and models of weak arithmetic.  In CSL’89: Proceedings of the 3rd Workshop on Computer Science Logic, pages 193–210. Springer, 1989.
  * Kra [97] Jan Krajíček.  Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic.  The Journal of Symbolic Logic, 62(2):457–486, 1997.
  * Kra [11] Jan Krajícek.  On the proof complexity of the Nisan-Wigderson generator based on a hard NP $\cap$ coNP function.  Journal of Mathematical Logic, 11(1), 2011.
  * LO [23] Jiatu Li and Igor C. Oliveira.  Unprovability of strong complexity lower bounds in bounded arithmetic.  In Symposium on Theory of Computing _(STOC)_ , 2023.
  * Mon [08] Morteza Moniri.  On the hierarchy of intuitionistic bounded arithmetic.  Journal of Logic and Computation, 18(4):625–630, 2008.
  * OS [17] Igor C. Oliveira and Rahul Santhanam.  Pseudodeterministic constructions in subexponential time.  In Symposium on Theory of Computing _(STOC)_ , pages 665–677, 2017.
  * Pic [15] Ján Pich.  Circuit lower bounds in bounded arithmetics.  Annals of Pure and Applied Logic, 166(1):29–45, 2015.
  * PS [21] Ján Pich and Rahul Santhanam.  Strong co-nondeterministic lower bounds for NP cannot be proved feasibly.  In Symposium on Theory of Computing _(STOC)_ , pages 223–233, 2021.
  * Raz [95] Alexander A. Razborov.  Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic.  Izvestiya: mathematics, 59(1):205, 1995.
  * RR [97] Alexander A. Razborov and Steven Rudich.  Natural proofs.  Journal of Computer and System Sciences, 55(1):24–35, 1997.
  * SW [14] Rahul Santhanam and Ryan Williams.  On uniformity and circuit lower bounds.  Computational Complexity, 23(2):177–205, 2014.

##  Appendix A On the Unprovability of Lower Bounds Against Deterministic
Circuits

This section provides an overview of a result from [18] showing that, under an
appropriate formalization, the unprovability of worst-case lower bounds
against _deterministic_ Boolean circuits in $\mathsf{IS}^{1}_{2}$ yields the
unprovability of the same lower bound in $\mathsf{S}^{1}_{2}$. The necessary
background on bounded arithmetic can be found in Section 2. In particular, the
vocabulary of $\mathsf{S}^{1}_{2}$ and $\mathsf{IS}^{1}_{2}$ is discussed in
Section 2.1.

#### Formalization.

For concreteness, we consider a constant $\delta>0$ and focus on the size
bound $2^{n^{\delta}}$. (The actual size bound is not relevant for the result,
provided that it can be captured by a sharply bounded formula in the sense
described below.) We use $\mathsf{SAT}=\\{\mathsf{SAT}_{n}\\}$ to denote the
decision version of the satisfiability problem for de Morgan Boolean formulas
represented by $n$-bit strings. We consider a sentence
$\mathsf{SAT}\text{-}\mathsf{DLB}^{\mathsf{exp}}(2^{n^{\varepsilon}},n_{0})$
which encodes that, for every input length $n\geq n_{0}$ and for every
deterministic circuit $D$ of size at most $2^{n^{\delta}}$, there is an input
$y$ such that $\mathsf{SAT}_{n}(y)\neq D(y)$. The formalization will require
the following auxiliary formulas. (The variable $f$ appearing in some of them
but not referred to is used to guarantee bounded quantification, as discussed
later in this section.)

$\mathsf{ONE}(f,y)$. For variables $f$ (a truth-table with $|f|=2^{n}$) and
$y$ (an index/input of $f$), we use the formula $\mathsf{ONE}(f,y)$ to
determine if the $y$-th entry of $f$ is $1$.

$\mathsf{SAT}(f,y,z)$. For variables $y$ (encoding a Boolean formula) and $z$
(encoding an assignment), the formula $\mathsf{SAT}(f,y,z)$ denotes that $y$
is satisfied by $z$.

$\mathsf{DECIDES}\text{-}\mathsf{SAT}(f,y)$. For variables $f$ and $y$, the
formula $\mathsf{DECIDES}\text{-}\mathsf{SAT}(f,y)$ denotes
$\mathsf{ONE}(f,y)\leftrightarrow\exists z\leq|f|\;\mathsf{SAT}(y,z)$, i.e.,
$f$ correctly decides the satisfiability of the formula encoded by $y$. (The
intended interpretation is that $z$ is an integer of magnitude at most $2^{n}$
and consequently can be viewed as an $n$-bit string.)

$\mathsf{SIZE}(f,D,n)$. For a variable $D$ (encoding a deterministic Boolean
circuit), $\mathsf{SIZE}(f,D,n)$ denotes the formula that checks if $D$ has
$n$ inputs and at most $2^{n^{\delta}}$ gates.

$\mathsf{ERROR}(f,D,w,y)$. For variables $f$, $D$, $w$ (a transcript of $D$’s
computation), and $y$, $\mathsf{Error}(f,D,w,y)$ denotes the formula stating
that $w$ correctly encodes the computation of $D$ on $y$ and $f(y)\neq D(y)$.

$\mathsf{INDEX}(f,W,y,w)$. For variables $W$ (a sequence of transcripts), $y$,
and $w$, $\mathsf{INDEX}(f,W,y,w)$ denotes that the $y$-th element of $W$ is
$w$.

Some of these formulas might require the specification of additional sub-
formulas in order to capture their intended behavior. Most importantly, we
note that all these formulas admit _sharply bounded_ descriptions due to the
presence of the variable $f$ (we will use $n=||f||)$ and the explicitly
provided candidate transcript $w$ (whose correctness is easy to check). (This
claim can be somewhat tedious to check; for additional details, see a similar
presentation in [18].) Next, we let
$\mathsf{SAT}\text{-}\mathsf{DLB}^{\mathsf{exp}}(2^{n^{\delta}},n_{0})$ denote
the following sentence:

$\displaystyle\forall f\;\forall n\;\forall D\;\forall W\;\forall w\;\exists
y\leq|f|\;$ $\displaystyle\Big{(}n=||f||\wedge n\geq
n_{0}\wedge\mathsf{DECIDES}\text{-}\mathsf{SAT}(f,y)\wedge\mathsf{SIZE}(f,D,n)\wedge\mathsf{INDEX}(f,W,y,w)\Big{)}$
$\displaystyle\rightarrow$ $\displaystyle\mathsf{ERROR}(f,D,w,y)\;.$

Observe that
$\mathsf{SAT}\text{-}\mathsf{DLB}^{\mathsf{exp}}(2^{n^{\delta}},n_{0})$ is the
universal closure of a sharply bounded formula, which is in particular a
$\forall\Sigma^{b}_{1}$-formula. It is not hard to see that it correctly
captures (over the standard model $\mathbb{N}$) the statement that
$\mathsf{SAT}_{n}\notin\mathsf{SIZE}[2^{n^{\delta}}]$ for all $n\geq n_{0}$.

Finally, we will make use of the following conservation result.

######  Theorem A.1 (Avigad [3, Theorem 3.17]).

$\mathsf{S}^{1}_{2}$ is conservative over $\mathsf{IS}^{1}_{2}$ for
$\forall\Sigma^{b}_{1}$ sentences.

As a consequence of this result and of the quantifier complexity of the
formalization, the provability of
$\mathsf{SAT}\text{-}\mathsf{DLB}^{\mathsf{exp}}(2^{n^{\delta}},n_{0})$ in
$\mathsf{S}^{1}_{2}$ yields its provability in $\mathsf{IS}^{1}_{2}$. In other
words, if the lower bound sentence in unprovable in $\mathsf{IS}^{1}_{2}$, it
is also unprovable in $\mathsf{S}^{1}_{2}$:

######  Theorem A.2.

For every rational $\delta>0$ and $n_{0}\in\mathbb{N}$, if
$\mathsf{IS}^{1}_{2}\nvdash\mathsf{SAT}\text{-}\mathsf{DLB}^{\mathsf{exp}}(2^{n^{\delta}},n_{0})$
then
$\mathsf{S}^{1}_{2}\nvdash\mathsf{SAT}\text{-}\mathsf{DLB}^{\mathsf{exp}}(2^{n^{\delta}},n_{0})$.

This result should be contrasted with Theorem 1.1 Item (_i_), which
establishes in particular the unprovability in $\mathsf{IS}^{1}_{2}$ of a _co-
nondeterministic_ size lower bound for $\mathsf{SAT}$. Note that the
quantifier complexity of the sentences $\mathsf{LB}^{\mathsf{exp}}$ and
$\mathsf{LB}^{\mathsf{poly}}$ from Theorem 1.1 does not allow us to invoke
Theorem A.2 (nor an extension of this conservation result from [12]) to derive
an unprovability result for $\mathsf{S}^{1}_{2}$.


# Semiparametrically Efficient Score for the Survival Odds Ratio

Denise Rava<EMAIL_ADDRESS>
Department of Mathematics  University of California  San Diego  Jelena Bradic
<EMAIL_ADDRESS>
Department of Mathematics and Halicioglu Data Science Institute
University of California  San Diego  Ronghui Xu<EMAIL_ADDRESS>
Department of Mathematics and Herbert Wertheim School of Public Health and
Halicioglu Data Science Institute
University of California  San Diego

###### Abstract

We consider a general proportional odds model for survival data under binary
treatment, where the functional form of the covariates is left unspecified. We
derive the efficient score for the conditional survival odds ratio given the
covariates using modern semiparametric theory. The efficient score may be
useful in the development of doubly robust estimators, although computational
challenges remain.

##  1 Introduction

The commonly used hazard ratio recently come under scrutiny due to its
conditioning on the risk sets which became not exchangeable even under
randomized treatment assignment at time zero (Hernán, 2010; Aalen et al.,
2015; Martinussen et al., 2020). While the debate is still on-going (Prentice
and Aragaki, 2022; Ying and Xu, 2023), a useful alternative measure of
treatment effect is the survival odds ratio. The proportional odds model for
survival data, assuming the odds ratio to be constant over time given the
treatment and the covariates, has been well studied in the literature
(Bennett, 1983; Pettitt, 1984; Dinse and Lagakos, 1983; Dabrowska and Doksum,
1988; Murphy et al., 1997; Rossini and Tsiatis, 1996; Scharfstein et al.,
1998; Yang and Prentice, 1999; Xu and Harrington, 2001; Collet, 2003; Crowder
et al., 2017). It is a special case of the transformation model with error
belonging to the $G^{\rho}$ family of Harrington and Fleming (1982), where
$\rho=1$. It models attenuating hazard ratios among treatment groups and also
provides a useful alternative to the otherwise commonly used proportional
hazards assumption, the latter equivalent to the $G^{\rho}$ family of error
distribution with $\rho=0$.

In this paper we consider a more general proportional odds model for survival
data, and relax the functional forms of the covariates in the model. We derive
the efficient score for the conditional survival odds ratio using modern
semiparametric theory. Efficient scores are useful in practice, not only
because they are efficient, but also because they can be useful in the
development of doubly robust estimators (Bickel et al., 1993; Tsiatis, 2006;
Zheng et al., 2016; Dukes et al., 2019; Rava and Xu, 2023).

###  1.1 Model and notation

Denote $T$ the time to failure, $C$ the censoring random variable and
$X=\min{(T,C)}$ the observed (and possibly censored) failure time. Let
$\delta$ be the event indicator, $A=0,1$ a binary treatment, $Z$ be a vector
of baseline covariates, and $\tau<\infty$ be an upper limit to follow-up time.

Denote $S(t|A,Z)$ the conditional survival function of $T$ given $A$ and $Z$.
Consider the following model for the distribution of $T$ given $A$ and $Z$:

$\displaystyle\operatorname{logit}\left\\{S(t|A,Z)\right\\}=\beta A-G(t,Z),$
(1)

where $\operatorname{logit}(x)=\log\\{x/(1-x)\\}$ and $G(t,Z)$ is completely
unspecified. This is more general than the classical proportional odds model
for survival data that assumes $G(t,Z)$ to be a baseline function in $t$ plus
a linear function in $Z$ (Bennett, 1983; Pettitt, 1984; Chen et al., 2012).
Under model (1) the treatment effecte expressed as the log survival odds ratio
between the treated and the untreated, is captured by the estimand $\beta$:

$\displaystyle\beta=\log\left\\{\frac{S(t|A=1,Z)}{1-S(t|A=1,Z)}\left/\frac{S(t|A=0,Z)}{1-S(t|A=0,Z)}\right.\right\\}.$
(2)

We use the counting process and the at-risk process notation:
$N(t)=\mathbbm{1}\left\\{X\leq t,\;\delta=1\right\\}$ and
$Y(t)=\mathbbm{1}\left\\{X\geq t\right\\}$. Define the martingale
$M(t):=N(t)-\int_{0}^{t}Y(u)\lambda(u|A,Z)du$, where $\lambda(t|A,Z)$ is the
conditional hazard function. We make the standard assumption $C\perp T|A,Z$,
where $\perp$ indicates statistical independence.

##  2 Semiparametrically efficient score

In the following we derive the semiparametrically efficient score for the
estimand $\beta$, following the approach described in Tsiatis (2006). We
consider the reparametrization as in Chen et al. (2012):
$R(t,Z)=\exp\\{G(t,Z))\\}$. Define also $r(t,Z)=\partial_{t}R(t,Z)$, where
$\partial_{t}$ is shorthand for $\partial/\partial_{t}$. Under model (1), it
can be verified immediately that:

$\displaystyle S(t|A,Z)=\frac{\exp(\beta A)}{\exp(\beta A)+R(t,Z)},$ (3)

and

$\displaystyle\lambda(t|A,Z)=\frac{r(t,Z)}{\exp(\beta A)+R(t,Z)}.$ (4)

Under model (1), the likelihood for a single copy of the data is:

$\displaystyle L(\beta,R,\Lambda_{c},f)$ $\displaystyle=$
$\displaystyle\left\\{\frac{r(X,Z)}{\exp(\beta
A)+R(X,Z)}\right\\}^{\delta}\frac{\exp(\beta A)}{\exp(\beta A)+R(X,Z)}$
$\displaystyle\cdot\lambda_{c}(X|A,Z)^{1-\delta}\exp\\{-\Lambda_{c}(X|A,Z)\\}f(A,Z),$

where $\Lambda_{c}(t|a,z)=\int_{0}^{t}\lambda_{c}(u|a,z)du$,
$\lambda_{c}(t|a,z)$ is the conditional hazard function for $C$ given $A$ and
$Z$, and $f(a,z)$ is the joint density or probability function of $A$ and $Z$.
Here the parameter of interest is $\beta$ while the nuisance parameter is
$\eta=\left[R,\lambda_{c},f\right]^{\top}$. Following lemma 2 of Rava and Xu
(2023), the score for $\beta$ is:

$\displaystyle S_{\beta}=\frac{\partial\log
L}{\partial\beta}=-\int_{0}^{\tau}A\cdot S(t|A,Z)dM(t).$ (5)

Let $\mathbf{\Lambda}$ be the nuisance tangent space, i.e. the space spanned
by the nuisance score function, and let $\mathbf{\Lambda}^{\perp}$ be its
orthogonal complement. The efficient score is
$S_{eff}=S_{\beta}-\Pi\\{S_{\beta}|\mathbf{\Lambda}\\}=\Pi\\{S_{\beta}|\mathbf{\Lambda}^{\perp}\\}$
(Tsiatis, 2006), where $\Pi\\{S_{\beta}|\mathbf{\Lambda}\\}$ and
$\Pi\\{S_{\beta}|\mathbf{\Lambda}^{\perp}\\}$ are the projections of
$S_{\beta}$ onto $\mathbf{\Lambda}$ and $\mathbf{\Lambda}^{\perp}$,
respectively.

Let $\Lambda_{1s}$, $\Lambda_{2s}$ and $\Lambda_{3s}$ be the nuisance tangent
spaces of $R$, $\lambda_{c}$ and $f$, respectively. Denote $M_{c}(t)$ the
martingale associated with the censoring distribution. The following Lemmas
describe $\mathbf{\Lambda}$ and $\mathbf{\Lambda}^{\perp}$ under model (1).

######  Lemma 1.

Under model (1), the nuisance tangent space $\mathbf{\Lambda}$ is

$\displaystyle\mathbf{\Lambda}=\Lambda_{1s}\oplus\Lambda_{2s}\oplus\Lambda_{3s},$
(6)

where

$\displaystyle\Lambda_{1s}$ $\displaystyle=$
$\displaystyle\left\\{\int_{0}^{\tau}\left\\{\frac{\partial_{t}h(t,Z)}{\exp(\beta
A)\lambda(t|A,Z)}-\frac{h(t,Z)}{\exp(\beta A)}\right\\}S(t|A,Z)dM(t)\right.$
$\displaystyle\left.\;\;:\;for\;\;all\;\;h(t,Z)\;\;s.t.\;\;\partial_{t}h(t,Z)\;\;exists\right\\},$
$\displaystyle\Lambda_{2s}=\left\\{\int_{0}^{\tau}\alpha(t,A,Z)dM_{c}(t)\;:\;for\;all\;\alpha(t,A,Z)\right\\},$
(8)

and

$\displaystyle\Lambda_{3s}=\left\\{b(A,Z)\;:\;E\left[b(A,Z)\right]=0\right\\}.$
(9)

######  Lemma 2.

Under model (1), the orthogonal nuisance tangent space is:

$\displaystyle\mathbf{\Lambda}^{\perp}$ $\displaystyle=$
$\displaystyle\left\\{\int_{0}^{\tau}\left\\{h(t,A,Z)-\frac{\partial_{t}h_{0}(t,Z)}{\exp(\beta
A)\lambda(t|A,Z)}+\frac{h_{0}(t,Z)}{\exp(\beta
A)}\right\\}S(t|A,Z)dM(t)\right.$ (10)
$\displaystyle\left.\;:\;for\;\;all\;\;h(t,A,Z)\right\\},$

where $h_{0}(t,Z)$, for almost every $t$, is a solution of the integro-
differential equation

$\displaystyle\partial_{t}h_{0}(t,Z)-h_{0}(t,Z)m(t,A,Z)-q\\{t,A,Z,h\\}$
$\displaystyle+v(t,A,Z)\int_{0}^{t}\left\\{\partial_{u}h_{0}(u,Z)w(u,A,Z)-h_{0}(u,Z)k(u,A,Z)\right\\}du=0.$
(11)

The coefficients $m(t,A,Z),q\\{t,A,Z,h\\},v(t,A,Z),w(t,A,Z),k(t,A,Z)$ are
provided in Appendix A. Formulas.

The proofs of all results can be found in 3.1.

Since $S_{\beta}=-\int_{0}^{\tau}A\cdot S(t|A,Z)dM(t)$, its projection on
$\mathbf{\Lambda}^{\perp}$ is the element of $\mathbf{\Lambda}^{\perp}$ that
corresponds to $h(t,A,Z)=-A$; that is:

$\displaystyle
S_{eff}=\int_{0}^{\tau}\left\\{-A-\frac{\partial_{t}h_{0}(t,Z)}{\exp(\beta
A)\lambda(t|A,Z)}+\frac{h_{0}(t,Z)}{\exp(\beta A)}\right\\}S(t|A,Z)dM(t)=0,$
(12)

where $h_{0}(t,Z)$ is a solution to the differential equation (2) with
$h(t,A,Z)=-A$.

##  3 Final remarks

Given $n$ independently and identically distributed (i.i.d.) observations, one
can estimate the unknown nuisance parameters that are needed: $R(t,z)$,
$S_{c}(t|a,z)=\exp\\{-\Lambda_{c}(t|a,z)\\}$ and $\pi(z)=P(A=1|z)$, either
nonparametrically or using parametric or semiparametric working models. A
major challenge for implementation of the efficient score (12) is the solution
of the complicated integro-differential equation (2) (Lakshmikantham, 1995).

Recall that $h_{0}(t,Z)=h_{0}(t,Z;R,S_{c},\pi)$ is a solution of the integro-
differential equation (2), with $h(t,A,Z)=-A$ for the efficient score (12).
With the estimates $\hat{R}(t,Z),\hat{S}_{c}(t|A,Z)$ and $\hat{\pi}(Z)$,
denote $\hat{h}_{0}(t,Z)=h_{0}(t,Z_{i};\hat{R},\hat{S}_{c},\hat{\pi})$ an
estimator for $h_{0}(t,Z)$. The parameter of interest $\beta$ can then be
estimated by solving

$\displaystyle\sum_{i=1}^{n}\delta_{i}V_{i}\left(X_{i};\beta,\hat{R},\hat{S}_{c},\hat{\pi}\right)\frac{\exp(\beta
A_{i})}{\left\\{\exp(\beta A_{i})+\hat{R}(X_{i},Z_{i})\right\\}}$
$\displaystyle-\sum_{i=1}^{n}\int_{0}^{X_{i}}V_{i}\left(t;\beta,\hat{R},\hat{S}_{c},\hat{\pi}\right)\frac{\hat{r}(t,Z_{i})\exp(\beta
A_{i})}{\left\\{\exp(\beta A_{i})+\hat{R}(t,Z_{i})\right\\}^{2}}dt=0,$ (13)

where

$\displaystyle V_{i}\left(t;\beta,\hat{R},\hat{S}_{c},\hat{\pi}\right)$
$\displaystyle=-A_{i}-\frac{\partial_{t}\hat{h}_{0}(t,Z)\left\\{\exp(\beta
A_{i})+\hat{R}(t,Z_{i})\right\\}}{\exp(\beta A_{i})d\hat{R}(t,Z_{i})}$
$\displaystyle\>\;\;+\frac{\hat{h}_{0}(t,Z)}{\exp(\beta A_{i})}.$ (14)

One may consider numerically approximating such solution for various values of
$t$ on a grid of $[0,\max(X_{1},\ldots,X_{n})]$ and for every $Z_{i}$. If a
grid of $m$ elements is chosen this means numerically approximating the
solution of $n*m$ integro-differential equations. This can be therefore
computationally intensive and choosing the appropriate $m$ and the appropriate
grid may be non-trivial, and is beyond the scope of this work.

On the other hand, the efficient score might offer a starting point for the
development of doubly robust estimators (Rava and Xu, 2023). This is would be
of interest for future work.

## Appendix

### Appendix A. Formulas

We provide here the coefficients of the integro-differential equation
introduced in Lemma 2.

$\displaystyle m(t,A,Z)$ $\displaystyle=$
$\displaystyle\frac{r(t,Z)E\left[S_{c}(t\mid A,Z)\exp(\beta
A)\left\\{\exp(\beta A)+R(t,Z)\right\\}^{-3}\mid Z\right]}{E\left[S_{c}(t\mid
A,Z)\exp(\beta A)\left\\{\exp(\beta A)+R(t,Z)\right\\}^{-2}\mid Z\right]},$
$\displaystyle q\\{t,A,Z,h(\cdot)\\}$ $\displaystyle=$
$\displaystyle\frac{r(t,Z)E\left[h(t,A,Z)S_{c}(t\mid A,Z)\left\\{\exp(\beta
A)\right\\}^{2}\left\\{\exp(\beta A)+R(t,Z)\right\\}^{-3}\mid
Z\right]}{E\left[S_{c}(t\mid A,Z)\exp(\beta A)\left\\{\exp(\beta
A)+R(t,Z)\right\\}^{-2}\mid Z\right]}$ $\displaystyle+$
$\displaystyle\frac{r(t,Z)\int_{0}^{t}r(u,Z)E\left[h(u,A,Z)S_{c}(u\mid
A,Z)\left\\{\exp(\beta A)\right\\}^{2}\left\\{\exp(\beta
A)+R(u,Z)\right\\}^{-4}\mid Z\right]du}{E\left[S_{c}(t\mid A,Z)\exp(\beta
A)\left\\{\exp(\beta A)+R(t,Z)\right\\}^{-2}\mid Z\right]},$ $\displaystyle
v(t,A,Z)$ $\displaystyle=$ $\displaystyle\frac{r(t,Z)}{E\left[S_{c}(t\mid
A,Z)\exp(\beta A)\left\\{\exp(\beta A)+R(t,Z)\right\\}^{-2}\mid Z\right]},$
$\displaystyle w(t,A,Z)$ $\displaystyle=$ $\displaystyle E\left[S_{c}(t\mid
A,Z)\exp(\beta A)\left\\{\exp(\beta A)+R(t,Z)\right\\}^{-3}\mid Z\right],$
$\displaystyle k(t,A,Z)$ $\displaystyle=$ $\displaystyle
r(t,Z)E\left[S_{c}(t\mid A,Z)\exp(\beta A)\left\\{\exp(\beta
A)+R(t,Z)\right\\}^{-4}\mid Z\right].$

###  3.1 Appendix B. Proofs of the main results

We report here the proofs of the main results, Lemma 1 and Lemma 2.

###### Proof of Lemma 1.

The spaces $\Lambda_{1s}$, $\Lambda_{2s}$ and $\Lambda_{3s}$ are orthogonal to
each other because the corresponding nuisance parameters are variationally
independent and the likelihood factors into the likelihoods for each of them
(Tsiatis, 2006). By this and by definition of $\mathbf{\Lambda}$, (6) is
directly proven.

Lemma 5.1 and pag.117 of Tsiatis (2006) proves (8) and (9), respectively.

We now prove (1). When the nuisance parameter has finite dimension, the
nuisance tangent space is simply the space spanned by the nuisance score. For
semiparametric model, the nuisance tangent space is the mean-square closure of
the nuisance tangent spaces of all parametric submodels. Let’s consider the
following generic parametric submodel:

$\displaystyle S(t|A,Z;\gamma)=\frac{\exp{\left(\beta
A\right)}}{\exp{\left(\beta A\right)}+R(t,Z;\gamma)},$ (15)

where $\gamma_{0}$ indicates the true value of the parameter. If we focus on
this parametric submodel, by Lemma 2 of Rava and Xu (2023), we have:

$\displaystyle S_{\gamma}$ $\displaystyle=$
$\displaystyle\left.\frac{\partial\log
L}{\partial\gamma}\right|_{\gamma=\gamma_{0}}$ (16) $\displaystyle=$
$\displaystyle\int_{0}^{\tau}\left\\{\frac{\partial_{\gamma}r(t,Z;\gamma_{0})}{r(t,Z)}-\frac{\partial_{\gamma}R(t,Z;\gamma_{0})}{\exp(\beta
A)+R(t,Z)}\right\\}dM(t).$ (17)

We therefore conjecture the following:

$\displaystyle\Lambda_{1s}$ $\displaystyle=$
$\displaystyle\left\\{\int_{0}^{\tau}\left[\frac{\partial_{t}h(t,Z)}{r(t,Z)}-\frac{h(t,Z)}{\exp(\beta
A)+R(t,Z)}\right]dM(t)\right.$
$\displaystyle\left.\;\;:\;\;for\;\;all\;\;h(t,Z)\;\;s.t.\;\;\partial_{t}h(t,Z)\;\;exists\right\\}.$

The above calculations prove that the nuisance tangent space of any parametric
submodel belongs to $\Lambda_{1s}$ defined in (3.1). To complete our proof we
need to prove that, for any element of the conjectured $\Lambda_{1s}$, indexed
by $h(t,Z)$, there exists a parametric submodel such that, such element is
part of its nuisance tangent space. Given $h(t,Z)$, straightforward algebra
proves that the score of the following parametric submodel

$\displaystyle S(t|A,Z)=\frac{\exp(\beta A)}{\exp(\beta A)+\gamma
h(t,Z)+R(t,Z)}$ (19)

corresponds to the element of $\Lambda_{1s}$ indexed by the chosen $h(t,Z)$.
Our conjecture is therefore proven right and so (3.1). Simplification of (3.1)
leads to (1). ∎

###### Proof of Lemma 2.

If we don’t put any restriction on the mechanism that generates the data, it
follows from Theorem 4.4 of Tsiatis (2006) that the tangent space is
$\mathcal{H}=\\{h(X,\delta,A,Z)\;:\;E(h)=0,\;E(h^{\top}h)<\infty\\}$, i.e. the
entire Hilbert space. Since model (1) does not impose any restriction on the
censoring distribution or the distribution of the treatment and the
covariates, it is true that:

$\displaystyle\mathcal{H}=\Lambda^{*}_{1s}\oplus\Lambda_{2s}\oplus\Lambda_{3s},$
(20)

where $\Lambda^{*}_{1s}$ is the tangent space associated with the distribution
of $T$ given $A,Z$, now left arbitrary. Therefore, by (6),
$\mathbf{\Lambda}^{\perp}$ is the residual of the projection of an arbitrary
element of $\Lambda_{1s}^{*}$ onto $\Lambda_{1s}$. Similarly to the proof of
(1), it can be shown that:

$\displaystyle\Lambda_{1s}^{*}$ $\displaystyle=$
$\displaystyle\left\\{\int_{0}^{\tau}h(t,A,Z)S(t|A,Z)dM(t)\;\;for\;\;all\;\;h(t,A,Z)\right\\}.$
(21)

We hence now focus on deriving
$\prod\left[\int_{0}^{\tau}h(t,A,Z)S(t|A,Z)dM(t)|\Lambda_{1s}\right]$ for a
generic $h(t,A,Z)$.

By definition of projection and by (1), we need to find $h_{0}(t,Z)$ such
that, for any $h(t,Z)$:

$\displaystyle 0$ $\displaystyle=$ $\displaystyle
E\left(\left[\int_{0}^{\tau}\left\\{h(t,A,Z)-\frac{\partial_{t}h_{0}(t,Z)}{\exp(\beta
A)\lambda(t|A,Z)}+\frac{h_{0}(t,Z)}{\exp(\beta
A)}\right\\}S(t|A,Z)dM(t)\right]\right.$ (22)
$\displaystyle\;\;\;\;\left.\cdot\left[\int_{0}^{\tau}\left\\{\frac{\partial_{t}h(t,Z)}{\exp(\beta
A)\lambda(t|A,Z)}-\frac{h(t,Z)}{\exp(\beta
A)}\right\\}S(t|A,Z)dM(t)\right]\right).$

Given two martingales $M,M^{\prime}$, we use $<M,M^{\prime}>$ to indicate the
predictable covariation process. By (22) we have:

$\displaystyle 0$
$\displaystyle=E\left[\int_{0}^{\tau}\left\\{h(t,A,Z)-\frac{\partial_{t}h_{0}(t,Z)}{\exp(\beta
A)\lambda(t|A,Z)}+\frac{h_{0}(t,Z)}{\exp(\beta A)}\right\\}\right.$
$\displaystyle\left.\cdot\left\\{\frac{\partial_{t}h(t,Z)}{\exp(\beta
A)\lambda(t|A,Z)}-\frac{h(t,Z)}{\exp(\beta
A)}\right\\}S^{2}(t|A,Z)<dM(t)>\right].$

By (3), (4) and some tedious algebra, we therefore have:

$\displaystyle 0$
$\displaystyle=E\left[\int_{0}^{\tau}\left\\{h(t,A,Z)-\frac{\partial_{t}h_{0}(t,Z)}{\exp(\beta
A)\lambda(t|A,Z)}+\frac{h_{0}(t,Z)}{\exp(\beta A)}\right\\}\frac{\exp(\beta
A)\partial_{t}h(t,Z)Y(t)}{\left\\{\exp(\beta A)+R(t,Z)\right\\}^{2}}dt\right.$
$\displaystyle\;\;\;\;\;\;\;\left.-\int_{0}^{\tau}\left\\{h(t,A,Z)-\frac{\partial_{t}h_{0}(t,Z)}{\exp(\beta
A)\lambda(t|A,Z)}+\frac{h_{0}(t,Z)}{\exp(\beta A)}\right\\}\frac{\exp(\beta
A)r(t,Z)h(t,Z)Y(t)}{\left\\{\exp(\beta A)+R(t,Z)\right\\}^{3}}dt\right].$

Applying integration by part on the second term gives us the following:

$\displaystyle 0$
$\displaystyle=E\left\\{\int_{0}^{\tau}H(t,A,Z)\partial_{t}h(t,Z)dt\right\\},$
(23)

where

$\displaystyle H(t,A,Z)$
$\displaystyle=\left\\{h(t,A,Z)-\frac{\partial_{t}h_{0}(t,Z)}{\exp(\beta
A)\lambda(t|A,Z)}+\frac{h_{0}(t,Z)}{\exp(\beta A)}\right\\}\frac{\exp(\beta
A)Y(t)}{\left\\{\exp(\beta A)+R(t,Z)\right\\}^{2}}$
$\displaystyle\;\;\;+\int_{0}^{t}\left\\{h(u,A,Z)-\frac{\partial_{u}h_{0}(u,Z)}{\exp(\beta
A)\lambda(u|A,Z)}+\frac{h_{0}(u,Z)}{\exp(\beta A)}\right\\}\frac{\exp(\beta
A)r(u,Z)Y(u)}{\left\\{\exp(\beta A)+R(u,Z)\right\\}^{3}}du.$

By (23) we have that, for every $h(t,Z)$,

$\displaystyle\int_{0}^{\tau}E\left[E\left\\{H(t,A,Z)|Z\right\\}\partial_{t}h(t,Z)\right]dt=0.$
(24)

This implies that, for almost every $t$,

$\displaystyle E\left\\{H(t,A,Z)|Z\right\\}=0.$ (25)

The above can be easily proved by contraddiction setting
$\partial_{t}h(t,Z)=E\left\\{H(t,A,Z)|Z\right\\}$. Condition (25) together
with Lemma (3) in Appendix C. Additional lemmas completes the proof. ∎

### Appendix C. Additional lemmas

We report here an additional lemma used in the proofs of the main results.

######  Lemma 3.

For a generic functions $B(t,A,Z)$, we have:

$\displaystyle E\left\\{B(t,A,Z)Y(t)\mid Z\right\\}=E\left\\{B(t,A,Z)S(t\mid
A,Z)S_{c}(t\mid A,Z)\mid Z\right\\}$ (26)

###### Proof.

By the tower law of conditional expectation and by the fact that $T\perp C\mid
A,Z$, we have:

$\displaystyle E\left\\{B(t,A,Z)Y(t)\mid Z\right\\}$
$\displaystyle=E\left[B(t,A,Z)E\left\\{Y(t)\mid A,Z\right\\}\mid Z\right]$
(27) $\displaystyle=E\left[B(t,A,Z)S(t\mid A,Z)S_{c}(t\mid A,Z)\mid Z\right]$
(28)

∎

## References

  * Aalen et al. (2015) Aalen, O. O., Cook, R. J., and Røysland, K. (2015).  Does cox analysis of a randomized survival study yield a causal treatment effect?  Lifetime data analysis, 21(4), 579–593.
  * Bennett (1983) Bennett, S. (1983).  Analysis of survival data by the proportional odds model.  Statistics in medicine, 2(2), 273–277.
  * Bickel et al. (1993) Bickel, P. J., Klaassen, C. A., Bickel, P. J., Ritov, Y., Klaassen, J., Wellner, J. A., and Ritov, Y. (1993).  Efficient and adaptive estimation for semiparametric models, volume 4.  Johns Hopkins University Press, Baltimore.
  * Chen et al. (2012) Chen, Y. Q., Hu, N., Cheng, S.-C., Musoke, P., and Zhao, L. P. (2012).  Estimating regression parameters in an extended proportional odds model.  Journal of the American Statistical Association, 107(497), 318–330.
  * Collet (2003) Collet, D. (2003).  Modelling survival data in medical research. flórida.
  * Crowder et al. (2017) Crowder, M. J., Kimber, A., Smith, R., and Sweeting, T. (2017).  Statistical analysis of reliability data.  Routledge.
  * Dabrowska and Doksum (1988) Dabrowska, D. M. and Doksum, K. A. (1988).  Estimation and testing in a two-sample generalized odds-rate model.  Journal of the american statistical association, 83(403), 744–749.
  * Dinse and Lagakos (1983) Dinse, G. E. and Lagakos, S. (1983).  Regression analysis of tumour prevalence data.  Journal of the Royal Statistical Society: Series C (Applied Statistics), 32(3), 236–248.
  * Dukes et al. (2019) Dukes, O., Martinussen, T., Tchetgen Tchetgen, E. J., and Vansteelandt, S. (2019).  On doubly robust estimation of the hazard difference.  Biometrics, 75(1), 100–109.
  * Harrington and Fleming (1982) Harrington, D. P. and Fleming, T. R. (1982).  A class of rank test procedures for censored survival data.  Biometrika, 69, 553–566.
  * Hernán (2010) Hernán, M. A. (2010).  The hazards of hazard ratios.  Epidemiology (Cambridge, Mass.), 21(1), 13.
  * Lakshmikantham (1995) Lakshmikantham, V. (1995).  Theory of integro-differential equations, volume 1.  CRC press.
  * Martinussen et al. (2020) Martinussen, T., Vansteelandt, S., and Andersen, P. K. (2020).  Subtleties in the interpretation of hazard contrasts.  Lifetime Data Analysis, 26(4), 833–855.
  * Murphy et al. (1997) Murphy, S., Rossini, A., and van der Vaart, A. W. (1997).  Maximum likelihood estimation in the proportional odds model.  Journal of the American Statistical Association, 92(439), 968–976.
  * Pettitt (1984) Pettitt, A. (1984).  Proportional odds models for survival data and estimates using ranks.  Journal of the Royal Statistical Society: Series C (Applied Statistics), 33(2), 169–175.
  * Prentice and Aragaki (2022) Prentice, R. L. and Aragaki, A. K. (2022).  Intention-to-treat comparisons in randomized trials.  Statistical Science, 37(3), 380–393.
  * Rava and Xu (2023) Rava, D. and Xu, R. (2023).  Doubly robust estimation of the hazard difference for competing risks data.  Statistics in Medicine, 42(6), 799–814.
  * Rossini and Tsiatis (1996) Rossini, A. and Tsiatis, A. (1996).  A semiparametric proportional odds regression model for the analysis of current status data.  Journal of the American Statistical Association, 91(434), 713–721.
  * Scharfstein et al. (1998) Scharfstein, D. O., Tsiatis, A. A., and Gilbert, P. B. (1998).  Semiparametric efficient estimation in the generalized odds-rate class of regression models for right-censored time-to-event data.  Lifetime data analysis, 4(4), 355–391.
  * Tsiatis (2006) Tsiatis, A. A. (2006).  Semiparametric theory and missing data.  Springer, New York.
  * Xu and Harrington (2001) Xu, R. and Harrington, D. P. (2001).  A semiparametric estimate of treatment effects with censored data.  Biometrics, 57(3), 875–885.
  * Yang and Prentice (1999) Yang, S. and Prentice, R. L. (1999).  Semiparametric inference in the proportional odds regression model.  Journal of the American Statistical Association, 94(445), 125–136.
  * Ying and Xu (2023) Ying, A. and Xu, R. (2023).  On defense of the hazard ratio.  arXiv preprint arXiv:2307.11971.
  * Zheng et al. (2016) Zheng, W., Petersen, M., and Van Der Laan, M. J. (2016).  Doubly robust and efficient estimation of marginal structural models for the hazard function.  The International Journal of Biostatistics, 12(1), 233–252.