1 Introduction↩︎

Unprovability of combinatorial statements in weak fragments of bounded arithmetic is a topic with a long history [1]. While the weak theory \(\textsf{T}^1_2(\alpha)\) and some of its extensions come with known unprovability results [2]–[4], there are no general methods able to tackle theories above \(\textsf{T}^2_2(\alpha)\), except the switching lemma [5] and lifting theorems [6] (which also use the switching lemma). However, mentioned methods seem difficult to adapt to fine-grained separations between successive theories \(\textsf{T}^i_2(\alpha)\) and \(\textsf{T}^{i+1}_2(\alpha)\): while those theories are known to be distinct [1], no formulas of fixed complexity are known to separate all of them.

In this paper, we follow on an earlier work of analyzing extensions of \(\textsf{T}^1_2(\alpha)\) and identify a computational condition on polynomial-time definable linear orderings, the Factorization Hypothesis. Our main result is that, over the base theory \(\textsf{T}^1_2(\alpha)\), the tournament principle is not implied by the minimization principle [6] restricted to those polynomial-time linear orders which satisfy this hypothesis. In fact, we conjecture that the Factorization Hypothesis is satisfied by all polynomial-time linear orders.

2 Preliminaries↩︎

2.1 Bounded Arithmetic↩︎

We start with a brief overview of bounded arithmetic. For further details, refer to [7] and [1].

Our primary focus is the relativized bounded arithmetic theory \(\textsf{T}^1_2(\alpha)\), with \(\alpha\) being a unary predicate symbol. The language of this theory, in addition to \(\alpha\), includes the usual arithmetical symbols \(0, 1, +, \cdot, \leq\), together with unary operations \(\lfloor\frac{\cdot}{2}\rfloor\) and \(|\cdot|\), and the binary function symbol \(\#\). The symbol \(|\cdot|\) denotes bit length, i.e., \(|0| = 0\) and, for \(x>0\), \(|x| = \lfloor \log_{2} x \rfloor + 1\). The symbol \(\#\) denotes the binary smash function, standardly defined as \(2^{|x|\cdot |y|}\). We denote this language by \(L_{\textsf{S}_2}(\alpha)\), with \(L_{\textsf{S}_2}\) denoting \(L_{\textsf{S}_2}(\alpha) \setminus \{\alpha\}\).

A formula is called sharply bounded if it is bounded and the bounding terms are of the form \(|t|\). The class of sharply bounded formulas is denoted by \(\Delta^b_0(\alpha)\).

The class \(\Sigma^b_1(\alpha)\) is defined as the smallest set of bounded formulas extending \(\Delta^b_0(\alpha)\) and closed under \(\land\), \(\lor\), sharply bounded quantification, and bounded existential quantification. The class \(\Pi^b_1(\alpha)\) is defined as the set of formulas \(\varphi\) such that \(\neg \varphi \in \Sigma^b_1(\alpha)\), equivalently, as the closure of \(\Delta^b_0(\alpha)\) under \(\land\), \(\lor\), sharply bounded quantification, and bounded universal quantification.

The theory \(\textsf{T}^1_2(\alpha)\) is axiomatized by a finite number of true statements expressing the most basic properties of the symbols, such as commutativity of \(+\) and \(\cdot\), or that \(|2x+1| = |x|+1\), forming the so-called BASIC theory; see [1]. This is augmented by the induction axiom scheme for all \(\Sigma^b_1(\alpha)\)-formulas. Formulas are allowed to contain free variables.

For a formula \(\varphi(x, \overline{y})\), denote by \(\textsf{PIND}(\varphi)\) the following sentence: \[\begin{align} \forall \overline{y} \: [(\varphi(0, \overline{y}) \land \forall x (\varphi(\lfloor \frac{x}{2} \rfloor, \overline{y}) \to \varphi(x, \overline{y}))) \to \forall x \varphi(x, \overline{y})]. \end{align}\]

The corresponding axiom scheme is called polynomial induction. The theory \(\textsf{S}^1_2(\alpha)\) is defined as the already mentioned BASIC theory, not treated in the current paper, augmented by the polynomial induction scheme for \(\Sigma^b_1(\alpha)\)-formulas.

A \(\Sigma^b_1(\alpha)\)-formula \(\varphi(\overline{x})\) belongs to the class \(\Delta^b_1(\alpha)\) if there is a \(\Pi^b_1(\alpha)\)-formula \(\psi(\overline{x})\) so that \(\textsf{S}^1_2(\alpha)\vdash \forall \overline{x} \: \varphi(\overline{x}) \equiv \psi(\overline{x})\). We note that it is more common to denote the previously defined formula class as \(\Delta^b_1(\alpha)\) in \(\textsf{S}^1_2(\alpha)\) to emphasize the theory over which the equivalence is established.

2.2 Forcing↩︎

Our treatment of forcing follows [8]. The reader may consult the mentioned paper for a more general treatment of the subject; here, we focus only on features relevant to the current work.

We fix a countable nonstandard model of true arithmetic in \(L_{\textsf{S}_2}\), denoted by \(\mathbb{M}\). Throughout this subsection, formulas, terms, and so on are allowed to contain parameters from \(\mathbb{M}\), unless stated explicitly. In the next section, we restrict the parameter space.

A forcing frame is a partially ordered set \((P, \preceq)\) (in general, this poset need not be related to \(\mathbb{M}\) in any way). Its elements are called conditions. When \(p \preceq q\), we say that \(p\) extends \(q\). Two conditions \(p, q\) are said to be compatible, denoted \(p \| q\), if they have a common extension; that is, if there exists \(r \preceq p,q\). Otherwise, such conditions are said to be incompatible, denoted \(p \perp q\).

A binary relation \(\Vdash\) between conditions and \(L_{\textsf{S}_2}(\alpha)(\mathbb{M})\)-sentences is called a forcing if it satisfies the following properties for all sentences \(\varphi, \psi\), all formulas \(\chi(x)\), and all conditions \(p, q\).

• \(p \Vdash \neg \varphi \:\) if and only if \(\: \forall q \preceq p: \: q \nVdash \varphi\);

• \(p \Vdash \varphi \land \psi \:\) if and only if \(p \Vdash \varphi\) and \(p \Vdash \psi\);

• \(p \Vdash \varphi \lor \psi \:\) if and only if \(\: p \Vdash \neg(\neg \varphi \land \neg \psi)\);

• \(p \Vdash \forall x \chi(x) \:\) if and only if, for all \(a \in \mathbb{M}\), \(\: p \Vdash \chi(a)\);

• \(p \Vdash \exists x \chi(x) \:\) if and only if \(\: p \Vdash \neg \forall x \neg \chi(x)\);

• if \(p \Vdash \varphi\) and \(q \preceq p\), then \(q \Vdash \varphi\);

• if \(\forall q \preceq p \: \exists r \preceq q \: r \Vdash \varphi\), then \(p \Vdash \varphi\).

A forcing \(\Vdash\) is called conservative if, for any sentence \(\varphi\) not involving the symbol \(\alpha\), and any condition \(p\), \(p \Vdash \varphi\) if and only if \(\varphi\) is true in \(\mathbb{M}\).

To consider only reasonable \(\Vdash\), we impose the following additional requirement on every conservative forcing relation considered below. This is essentially a stronger and simpler version of [8]: given a condition \(p\), and closed terms \(s,t\), if \(\mathbb{M}\vDash t=s\) and \(p \Vdash \alpha(t)\), then \(p \Vdash \alpha(s)\).

A subset \(G \subseteq P\) is called a filter if it satisfies

• for any \(p, q \in G\), there exists \(r \in G\) so that \(r \preceq p, q\);

• for any \(p \preceq q\), if \(p \in G\), then \(q \in G\).

A subset \(D \subseteq P\) is called dense if any \(p \in P\) can be extended by some \(q \in D\), and a filter \(G\) is called generic if it intersects all sets from a selected countable collection of dense subsets of \(P\). The full definition of genericity [8] is not relevant for the current discussion. What matters is that such filters exist [8], and that they satisfy Theorem 2 below.

3 \(\textsf{TOUR}\), \(\textsf{MIN}\), and the Transfer Lemma↩︎

Let \(n\) be a nonstandard number in \(\mathbb{M}\), and let \(\mathbb{I}\) be the small canonical cut over \(n\), i.e., the set of numbers in \(\mathbb{M}\) bounded above by parameter-free terms in \(n\). As usual, the initial interval \([0, \dots, n-1]\) is denoted by \([n]\).

Recall the pairing function \(\langle \cdot, \cdot \rangle\), defined as \[\langle x, y \rangle := \frac{(x + y) (x + y + 1)}{2} + y.\] This is a bijective mapping between \(\mathbb{N}\times \mathbb{N}\) and \(\mathbb{N}\), and the same term defines, internally in \(\mathbb{M}\), a bijection between \(\mathbb{M}\times \mathbb{M}\) and \(\mathbb{M}\). With such a function, we can turn the unary \(\alpha(\cdot)\) into a binary relation \(\alpha(\langle \cdot, \cdot \rangle)\), which we denote by \(\alpha\) for simplicity as well.

It is a well-known fact that any tournament with \(m\) vertices contains a dominating set of size \(\leq |m| + 1\); see, e.g., [9].

The following formula \(\textsf{TOUR}(\alpha, u)\) expresses the above fact formally for graphs with edge-relation defined by \(\alpha\), with \(u\) being a free variable: \[\begin{gather} \exists x, y < u \: (x \neq y) \land (\neg \alpha(x, y) \land \neg \alpha(y, x)) \\ \lor \\ \exists x, y < u \: (x \neq y) \land (\alpha(x, y) \land \alpha(y, x)) \\ \lor \\ \exists X \subseteq [u] (|X| \leq |u| + 1) \: \forall x < u \: \bigl(x \in X \lor \exists y < u \: (y \in X \land \alpha(y, x))\bigr). \end{gather}\]

The sets \(X\) quantified in the above expression are represented as sequences of length at most \(|u| + 1\), or equivalently by padded sequences of length \(|u|+1\) together with a length parameter. Thus they can be encoded as numbers from \(\mathbb{M}\) of size \(O(u^{|u|+1})\).

Let \((P, \preceq)\) denote the forcing frame of definable in \(\mathbb{M}\) partial orientations of \(K_n\), the complete graph on \(n\) vertices, of size polynomial in \(|n|\). Conditions of such a frame can be identified with sets of ordered pairs of distinct elements of \([n]\), containing at most one of \((a,b)\) and \((b,a)\) for each unordered pair \(\{a,b\}\). We then define a conservative forcing relation \(\Vdash\) in the natural way: \(p \Vdash \alpha(a, b)\) if and only if \((a, b) \in p\), for numbers \(a, b \in \mathbb{M}\).

The following can be proved in the exact same way as similar statements in [8].

The main goal of the current work is to present a condition on \(\Delta^b_1(\alpha)\)-definable linear orders, stated formally in Hypothesis 15, that implies that \(\mathbb{I}[G]\) satisfies the full minimization scheme for such orders. Moreover, we conjecture that all \(\Delta^b_1(\alpha)\)-definable linear orders obey this condition. As a corollary, our conjecture implies that the tournament principle is not provable from the minimization principle, a statement which currently seems to lie outside the scope of known separation techniques.

To formulate the main conjecture, Hypothesis 15, we begin by directly analyzing the following question. Recall that \((P, \preceq)\) refers to the forcing frame of definable partial orientations on \(K_n\) with sizes polynomial in \(|n|\).

Following the standard forcing argumentation, we pick an arbitrary condition \(p\), a number \(m \in \mathbb{I}\), and a \(\Delta^b_1(\alpha)\)-formula \(\varphi(x, y)\) with parameters from \(\mathbb{I}\), with the goal of showing that \(p\) can be extended to a condition \(q\) forcing \(\textsf{MIN}(\varphi, m)\).

First, recall a fundamental property of \(\Vdash\) [8], stating that \(q \nVdash \psi\) if and only if there exists \(r \preceq q\) such that \(r \Vdash \neg \psi\), for all conditions \(q\) and any sentence \(\psi\). Thus, we may assume \[p \Vdash \bigwedge_{i=0}^3 \neg \textsf{MIN}_i(\varphi, m),\] i.e., \(p\) forces that \(\varphi(x, y)\) defines a strict linear ordering on \([m]\). Otherwise, there is an extension \(q \preceq p\) forcing the negation of this conjunction, hence forcing one of the first four disjuncts of \(\textsf{MIN}(\varphi,m)\), and we are done.

It is then enough to show that \(p \nVdash \neg \textsf{MIN}_4(\varphi, m)\). Equivalently, by the forcing clauses from Section 2.2, it is enough to find a number \(m_0 \in [m]\) and a condition \(q \preceq p\) such that \[q \Vdash \forall x < m \: \bigl((x = m_0) \lor \varphi(m_0, x)\bigr).\] A priori, this is not a simple task. Forcing the universal sentence \[\forall x < m \: \bigl((x = m_0) \lor \varphi(m_0, x)\bigr)\] is equivalent to forcing all \(\Delta^b_1(\alpha)\)-sentences \(\varphi(m_0, m_1)\) for all \(m_1 \neq m_0 < m\) simultaneously. By itself, this might not be possible to accomplish via conditions of small size.

The only way to overcome the above problem is to use, in a non-trivial way, the fact that \(\varphi\) is forced to define a strict linear ordering.

Below, we treat the cut \(\mathbb{I}\) as an \(L_{\textsf{S}_2}\)-substructure of \(\mathbb{M}\).

From this perspective, the forcing completeness theorem, Theorem 2, equates the standard forcing relation \(\Vdash\) with the relative forcing relation \(\Vdash^*_\mathcal{O}\) for \(\mathcal{O}\) being the class of all orientations induced by generic filters. The other \(\mathcal{O}\) of obvious interest is the class of all internally coded total orientations of \(K_n\). Equivalently, these are the orientations definable in \(\mathbb{M}\) with parameters from \(\mathbb{M}\). We denote this class by \(\mathcal{D}\).

Now, given some \(q\) and a bounded sentence \(\psi\), we want to express \(q \Vdash^*_\mathcal{D} \psi\) as an \(L_{\textsf{S}_2}\)-sentence “\(q \Vdash^*_\mathcal{D} \psi\)” with parameters from \(\mathbb{M}\), so that \(q \Vdash^*_\mathcal{D} \psi\) if and only if \(\mathbb{M}\vDash\) “\(q \Vdash^*_\mathcal{D} \psi\)”. In more detail, we first apply a Paris–Wilkie style propositional translation to \(\psi\); see [10]. This gives a propositional formula \(\langle \psi \rangle\) on \(\binom{n}{2}\) variables (while \(\alpha\) is binary on \([n]\), since we restrict ourselves only to orientations of \(K_n\), it is enough to consider only unordered pairs of distinct elements of \([n]\), hence the size \(\binom{n}{2}\)). Note that such a formula can be encoded as a number in \(\mathbb{M}\). The condition \(q\) is then identified with the corresponding partial assignment to those variables denoted as \(\tilde{q}\). Since every internally coded total assignment is definable in \(\mathbb{M}\) from its code, the fact that \(q \Vdash^*_{\mathcal{D}} \psi\) is equivalent to the statement that \(\langle \psi \rangle \vert_{\tilde{q}}\) is a tautology. The latter can be expressed in \(\mathbb{M}\), which we denote as “\(q \Vdash^*_\mathcal{D} \psi\)”. Notice that the sentence “\(q \Vdash^*_\mathcal{D} \psi\)” contains parameters outside of \(\mathbb{I}\), as we are quantifying over the set of all total assignments to \(\binom{n}{2}\)-many variables.

The main utility of the Transfer Lemma, Lemma 8, is to equate a statement \(q \Vdash \psi\) to “\(q \Vdash^*_\mathcal{D} \psi\)”, for \(\Pi^b_1(\alpha)\)-sentences \(\psi\), which can then be analyzed inside the ground model \(\mathbb{M}\). This is in line with how the least number principle for \(\Sigma^b_1(\alpha)\) is forced in [8]; see the notion of partial definability of \(\Vdash\) in the mentioned paper. The main difference here is that we identify a class of globally definable structures, i.e., totally defined interpretations of \(\alpha\), for which the transfer holds, instead of relying on small partial substructures, as is usually the case.

4 Factorization Hypothesis↩︎

By Theorem 1, the relation \(\varphi(x, y)\) can be decided by a Turing machine \(T[\alpha](x, y)\) which queries an oracle \(\alpha\), and which runs in time polynomial in the bit lengths of the input numbers. We choose this notation to emphasize that \(\alpha\) is not a regular input, but an oracle queried by \(T\) during the computation.

Since parameters of \(\varphi\) are from \(\mathbb{I}\), and \(x, y\) are restricted to the interval \([m]\) with \(m \in \mathbb{I}\), the runtime of \(T[\alpha](x, y)\) is bounded above by a polynomial in \(|n|\). Oracles are identified with total assignments to a fixed set of \(\binom{n}{2}\) variables. Given such a total assignment \(s\), we denote by \(T[\alpha_s](x, y)\) the result of substituting \(s\) for \(\alpha\). Then the condition \(p\) is identified with a partial assignment to the same variables, and the class \(\mathcal{D}\) is identified with all internally coded total assignments.

The statement \[``p \Vdash^*_\mathcal{D} \bigwedge_{i=0}^3 \neg \textsf{MIN}_i(\varphi, m)''\] now means that the Turing machine \(T[\alpha_s](x, y)\), for all total assignments \(s\) agreeing with \(p\), defines a strict linear order on \([m]\). Finding \(q \preceq p\) satisfying \[``q \Vdash^*_\mathcal{D} \forall y < m \: (m_0 = y) \lor \varphi(m_0, y)''\] amounts to assigning polynomially many additional variables so as to fix the smallest element of the ordering defined by \(T[\alpha](x, y)\) on \([m]\).

This leads to the following problem, with \(p\) fixed to \(\emptyset\) without loss of generality.

Suppose otherwise that the three variables \(v_{a,b}\), \(v_{a,c}\), and \(v_{b,c}\) were distinct. Since none of the pairwise comparisons is decided by \(p\), and since each comparison depends on its corresponding variable, we could assign these three variables independently so as to force \[a\triangleleft b,\quad b\triangleleft c,\quad c\triangleleft a.\] This contradicts the fact that every total assignment extending \(p\) defines a strict linear order. This proves the Triangle Lemma.

Step 4. Fix an arbitrary \(a\in X\), and denote \(v_{a,b}\) simply by \(v_b\) for \(b\in X\setminus\{a\}\). We define the following binary relation \(\sim\) on \(X\setminus\{a\}\): \[b\sim c \quad \text{if and only if} \quad v_b=v_c.\] Since \(\sim\) is an equivalence relation, it induces a partition \[X\setminus\{a\}=\bigsqcup_i X_i.\]

Step 5. Assume that some component \(X_i\) has cardinality at least \(\frac{1}{3}|X|\). Let \(v\) denote \(v_b\) for an arbitrary \(b\in X_i\). By averaging, there is \(s\in\{0,1\}\) so that, for at least half of the elements \(c\in X_i\), \[p\cup\{v=s\}\Vdash a\triangleleft c.\] Denote the set of such elements \(c\) by \(X'\). It follows that \[|X'|\geq \frac{1}{6}|X|.\] By induction, we can extend \(p\cup\{v=s\}\) to a condition \(q\) of size \[|q| \leq |p|+1+C\log_2\left(\frac{5}{6}|X|\right) \leq |p|+C\log_2|X|\] which forces the \(\triangleleft\)-minimality of some \(d\in X\setminus X'\). It follows that \(q\Vdash d\triangleleft a\), or \(d=a\), and hence such \(d\) is \(\triangleleft\)-minimal on the whole set \(X\) as well.

For the remainder of the proof, we assume that all of the components \(X_i\) have cardinality less than \(\frac{1}{3}|X|\).

Step 6. Given distinct \(X_i,X_j\), and arbitrary \(b\in X_i\), \(c\in X_j\), the Triangle Lemma implies \[v_{b,c}\in \{v_b,v_c\}.\] We then define the following grid \(G\), indexed by ordered pairs of elements of \(X\setminus\{a\}\): \[G_{b,c} = \begin{cases} *, & b \sim c; \\ 0, & v_{b,c} = v_b (= v_{a,b}); \\ 1, & v_{b,c} = v_c (= v_{a,c}). \end{cases}\] Denote by \(G_b\) and \(G^c\) the row and column of \(G\) corresponding to \(b\) and \(c\), respectively.

Step 7. Assume that some row \(G_b\) contains at least \(\frac{1}{3}|X|\) many \(0\)s. Let \(X'\) denote the set of all \(c\) such that \(G_{b,c}=0\). For any \(c\in X'\), it holds that \(v_{b,c}=v_b\). We can then proceed similarly to Step 5: find an \(s\in\{0,1\}\) such that \(p\cup\{v_b=s\}\) forces \(b\triangleleft c\) for at least half of the elements of \(X'\), and apply induction to \(X\setminus X'\), whose size is at most \(\frac{5}{6}|X|\).

For the remainder of the proof, we assume that every row of \(G\) contains fewer than \(\frac{1}{3}|X|\) many \(0\)s.

Step 8. Note that each row and each column of \(G\) contains fewer than \(\frac{1}{3}|X|\) many \(*\)s. Let \(o\) denote the maximum number of \(1\)s contained in a single column of \(G\). By double-counting the number of \(1\)s in \(G\), and using the assumptions that every row contains fewer than \(\frac{1}{3}|X|\) many \(0\)s and fewer than \(\frac{1}{3}|X|\) many \(*\)s, it follows that \[|X \setminus \{a\}| \cdot o > |X \setminus \{a\}| \cdot (|X \setminus \{a\}| - \frac{2}{3}|X|),\] which implies \(o > \frac{1}{3}|X| - 1\).

The column version of Step 7 now applies: if a column \(G^c\) contains at least \(\frac{1}{3}|X| - 1\)-many \(1\)s, then we can fix \(v_c\) appropriately to \(s\) to force \(c\triangleleft b\) for at least \(\frac{1}{6}|X| - \frac{1}{2}\)-many \(b\)s. By induction, we can extend \(p\cup\{v_c=s\}\) to a condition \(q\) of size \[|q| \leq |p|+1+C\log_2\left(\frac{5}{6}|X| + \frac{1}{2}\right) \leq |p|+C\log_2|X|,\] finishing the proof. ◻ ::::

Unfortunately, we are unable to extend the above proof method to the general case needed for resolving Question 10. We believe that the crucial missing detail is a more general analogue of the Triangle Lemma.

Below, we formulate a stronger, but arguably more natural, condition on orderings defined by polynomial-time oracle Turing machines that is enough to resolve Question 10. This condition may be of independent interest.

We choose the name because the computation of \(T[\alpha](\overline{a},a,b)\) factorizes into two independent computations \(f[\alpha](\overline{a},a)\) and \(f[\alpha](\overline{a},b)\).

It is important to keep in mind that \(f\) does not need to calculate the exact index of the corresponding number in the given ordering. In other words, \(f\) need not be surjective on \([m]\).

Below, we give an example of \(T\) that factorizes, but for which no polynomial-time indexing function can be constructed.

References↩︎