Anupam Das
email: anupam.das@ens-lyon.fr

From positive and intuitionistic bounded arithmetic to monotone proof complexity

We study versions of second-order bounded arithmetic where induction and comprehension formulae are positive or where the underlying logic is intuitionistic, examining their relationships to monotone and deep inference proof systems for propositional logic.

In the positive setting a restriction of a Paris-Wilkie (PW) style translation yields quasipolynomial-size monotone propositional proofs from Π 0 1 arithmetic theorems, as expected. We further show that, when only polynomial induction is used, quasipolynomialsize normal deep inference proofs may be obtained, via a graphrewriting normalisation procedure from earlier work.

For the intuitionistic setting we calibrate the PW translation with the Brouwer-Heyting-Kolmogorov interpretation of intuitionistic implication to recover a transformation to monotone proofs. By restricting type level we are able to identify an intuitionistic theory, I1U 1 2 , for which the transformation yields quasipolynomialsize monotone proofs. Conversely, we show that I1U 1 2 is powerful enough to prove the soundness of monotone proofs, thereby establishing a full correspondence.

Introduction

Bounded arithmetic has been a fruitful way to relate complexity classes with logical theories and propositional proof systems. For example Paris and Wilkie showed that proofs of Π 0 1 -sentences in the theory I∆0 1 translate to classes of polynomial-size Hilbert-Frege (HF) proofs of bounded depth [START_REF] Paris | ∆ 0 sets and induction[END_REF]; conversely, the soundness of bounded-depth HF systems can be proved in such theories. 2 In this work we identify theories of bounded arithmetic for monotone and deep inference proof systems, via positive and intuitionistic versions of well-known theories in the literature.

Deep inference proof complexity has received much attention in recent years, and the complexity of the minimal system, KS, is considered as yet unresolved [START_REF] Bruscoli | On the proof complexity of deep inference[END_REF] [START_REF] Jeřábek | Proof complexity of the cut-free calculus of structures[END_REF] [START_REF] Das | Complexity of deep inference via atomic flows[END_REF]. While an extension 1 This is the fragment of Peano Arithmetic with induction is restricted to ∆ 0 -formulae. 2 Strictly speaking, we also require the 'Ω 1 axiom', to allow simple manipulation of sequences.

[Copyright notice will appear here once 'preprint' option is removed.] of it, KS + , is known to quasipolynomially3 simulate HF systems 4[22] [START_REF] Bruscoli | A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae[END_REF], there is neither such a simulation known for KS nor some nontrivial lower bound separating the two systems.

These systems can be viewed as subclasses of tree-like monotone proofs (exemplified in e.g. [START_REF] Brünnler | Deep inference and its normal form of derivations[END_REF] and [START_REF] Jeřábek | Proof complexity of the cut-free calculus of structures[END_REF]), i.e. sequent calculus proofs free of negation steps (MLK ), studied in e.g. [START_REF] Pudlák | On the complexity of the propositional calculus[END_REF], [START_REF] Bílková | Monotone sequent calculus and resolution[END_REF] and [START_REF] Atserias | Monotone simulations of non-monotone proofs[END_REF]. 5 We exploit this correspondence in the present work and, for simplicity of exposition, work with rewriting systems MON and NOR instead of KS + and KS, respectively [START_REF] Das | On the pigeonhole and related principles in deep inference and monotone systems[END_REF].

The starting point of this work is the second-order framework due to Buss [START_REF] Samuel | Bounded arithmetic, volume 1 of Studies in Proof Theory[END_REF], as developed by Krajícek in [START_REF]Bounded arithmetic, propositional logic, and complexity theory[END_REF]. 6 In Sect. 3 we consider 'positive' versions of the theories U i j and V i j , where set variables may not occur in negative context in non-logical rules. We address some proof-theoretic issues and give a deep inference style presentation of the Paris-Wilkie (PW) translation to MON in Dfn. [START_REF] Jeřábek | Proofs with monotone cuts[END_REF]. The main result of this section is Thm. [START_REF] Paris | ∆ 0 sets and induction[END_REF], that proofs in the image of a certain theory M U 1 2 can be transformed to NORproofs in quasipolynomial time, via graph-rewriting normalisation procedures from [START_REF] Guglielmi | Normalisation control in deep inference via atomic flows[END_REF] and analysis of their complexity from [START_REF] Das | On the relative proof complexity of deep inference via atomic flows[END_REF].

In Sect. [START_REF] Bílková | Monotone sequent calculus and resolution[END_REF], in order to obtain converse statements to these translations, we turn to intuitionistic variants of these theories, allowing us to recover the ability to conduct some metalogical reasoning. The two main contributions of this section are Lemma 39, a sort of witnessing theorem that eliminates the presence of second-order existential quantifiers in a proof, and Dfn. 44, an adaptation of the PW translation by the Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic, ultimately yielding monotone proofs. For a certain theory, I1U 1 2 , we obtain in Cor. 46 that proofs in the image of the translation can be made tree-like (i.e. in MON) efficiently.

In Sect. 5 we consider reflection principles: formal statements of the soundness of a system. The main result of this section is Thm. 49, that I1U 1 2 proves the soundness of MON, thereby establishing a full correspondence between I1U 1 2 and MON. Finally, in Sect. [START_REF] Brünnler | A local system for classical logic[END_REF] we present some further discussion and results, and in Sect. 7 we give some concluding remarks.

Preliminaries

We generally follow the notations and conventions from [START_REF]Bounded arithmetic, propositional logic, and complexity theory[END_REF], and occasionally [START_REF] Cook | Logical Foundations of Proof Complexity[END_REF] as well. Throughout this paper we adopt quasipolynomial-time, i.e. 2 log O(1) n -time, as our model of feasible computation. A polylogarithm is a function log O(1) n.

Propositional and second-order logic

We formulate propositional logic (PL) with connectives ⊥, , ∨, ∧, ⊃ and countably many propositional variables, e.g. p, q etc. We may use other common connectives as abbreviations for their usual definitions in this basis. Namely, we write ¬ϕ for ϕ ⊃ ⊥ and ϕ ≡ ψ for (ϕ ⊃ ψ) ∧ (ψ ⊃ ϕ). We often omit brackets for long conjunctions and disjunctions for readability, and also for long implications when the right-most bracketing is assumed.

For arithmetic theories, we work in a two-sorted first-order logic, which we refer to as second-order logic (SOL) in line with the literature. SOL extends PL by variables x, y, z etc. for individuals, X, Y, Z etc. for sets (or strings), symbols =1, =2 for individual and set equality, respectively, and quantifiers ∃ 1 , ∀ 1 and ∃ 2 , ∀ 2 for individual and set quantification respectively. There is also a nonlogical binary infix symbol ∈ expressing membership of an individual in a set. There may be further non-logical symbols, in which case we use metavariables s, t and S, T to range over individual and set terms respectively.

We sometimes write Xx or X(x) instead of x ∈ X. In all settings, we denote formulae by Greek letters ϕ, ψ etc., possibly indicating free variables within parentheses, e.g. ϕ(x, y).

Definition 1 (Contexts and polarity). A context ϕ[•]

is a formula with a hole in place of a subformula. We say that a context ϕ[•] is positive if its hole is under the left-scope of an even number of ⊃ symbols; otherwise it is negative. E.g. the context

([•] ⊃ ϕ) ⊃ ψ is positive, while the context [•] ⊃ (ϕ ⊃ ψ) is negative.
A formula is positive or monotone if no set symbol occurs in negative context.

Convention 2 (Sequent calculus). We work with a usual sequent calculus LK 2 over our basis of connectives, with multiplicative formulations of branching logical rules and additive versions of non-branching logical rules, 7 e.g. as presented in [START_REF] Samuel | Bounded arithmetic, volume 1 of Studies in Proof Theory[END_REF]. In all cases cedents are multisets of formulae and the symbol → delimits the two sides of a sequent, e.g. a typical sequent is written Γ → ∆. We write LK for the propositional fragment of LK 2 .

A sequent is positive if it contains only positive formulae. The monotone (propositional) sequent calculus MLK is obtained from the propositional calculus LK by removing the ⊃ rules.

The intuitionistic caclulus LJ 2 is obtained from LK 2 by insisting that the RHS of each sequent in a proof consists of at most one formula. For this we must also alter the ∨-l rule slightly as follows:

Γ, ϕ → ∆ Σ, ψ → ∆ ∨-l Γ, Σ, ϕ ∨ ψ → ∆ A (dag-like)
proof is a list of sequents such that each one follows from previous ones by a rule of LK 2 . We call a proof treelike if its dependency graph is a tree, i.e. each sequent is used at most once as the premiss of an inference step.

Bounded arithmetic and the Paris-Wilkie translation

We work in the setting of [START_REF]Bounded arithmetic, propositional logic, and complexity theory[END_REF] (itself based on [START_REF] Samuel | Bounded arithmetic, volume 1 of Studies in Proof Theory[END_REF]), and refer the reader to those works for comprehensive preliminary material on bounded arithmetic.

We consider second-order theories over the vocabulary,

L2 = {0, 1, +, ×, | • |, #, • 2 , <} 7
Here, we mean 'additive' and 'multiplicative' in the sense of linear logic.

with the usual interpretation of symbols, as construed in [START_REF]Bounded arithmetic, propositional logic, and complexity theory[END_REF]. As usual, set symbols are now equipped with bounding terms and associated axioms. We will write X ≤ t for the positive atomic formula s ≤ t, where s is the bounding term of X. 8 We will write Σ B i and Π B i for the classes of formulae strict-Σ Remark 3. While we are borrowing some notation from [START_REF] Cook | Logical Foundations of Proof Complexity[END_REF] for readability, we do not formally follow their framework. They include a length term for sets, which makes it difficult to distinguish the forms of induction PIND and IND we consider later on. However we do assume that set symbols are equipped with a bounding term as in [START_REF]Bounded arithmetic, propositional logic, and complexity theory[END_REF], when necessary.

We assume that all our theories contain some appropriate set BASIC of basic axioms (including extensionality and boundedness of sets), which can be found in [START_REF]Bounded arithmetic, propositional logic, and complexity theory[END_REF].

Definition 4 (Induction and comprehension). We define the following axioms:

CA : ∃X ≤ y.∀x < y.(Xx ≡ ϕ(x)) IND : ϕ(0) ⊃ ∀x.(ϕ(x) ⊃ ϕ(x + 1)) ⊃ ∀x.ϕ(x) PIND : ϕ(0) ⊃ ∀x.(ϕ( x 2 ) ⊃ ϕ(x)) ⊃ ∀x.ϕ(x)
For any of these axioms AX and a set of formulae Φ, we denote by Φ-AX the set of axiom instances when the formula ϕ is in Φ.

Henceforth we assume the calculus LK 2 is enriched with initial sequents for (all instantiations by terms of) any axioms under consideration and also the usual designated rules for the bounded quantifiers. If we are working in theories containing IND or PIND, then we assume proofs are formulated with their associated inference rules, cf. [START_REF]Bounded arithmetic, propositional logic, and complexity theory[END_REF]. We will also have a proof-theoretic treatment of comprehension in the form of witnessing theorems, which we will present in Sects. 3.2 and 4.3.

The following result is, in fact, a corollary of what is usually called 'free-cut elimination' introduced by Takeuti in [START_REF] Takeuti | Proof Theory[END_REF], which is discussed in detail in [START_REF] Samuel | Handbook of proof theory[END_REF], although we state essentially the version from [START_REF] Cook | Logical Foundations of Proof Complexity[END_REF].

Theorem 5 (Free-cut elimination). Let S be a sequent system containing LK 2 and possibly containing non-logical initial sequents and induction rules that are closed under substitution of terms for free variables. Every S-theorem ϕ has an S-proof where each formula occurring is (a substitutional instance of) a subformula of ϕ, an induction formula, or a formula in an initial sequent.

An important point is that the above statement also holds for intuitionistic theories (e.g. as stated in [START_REF] Samuel | Handbook of proof theory[END_REF]). Definition 6. The theory U i 2 is axiomatised by BASIC , Σ B 0 -CA and Σ B i -PIND. V i 2 is the same but with IND in place of PIND. We now present a translation • of closed Σ B 0 -formulae to quasipolynomial-size propositional formulae, where set symbols are associated with propositional variables, essentially from [START_REF] Paris | ∆ 0 sets and induction[END_REF].

Let v (t) denote the numerical value of a closed term t.

Definition 7 (PW for closed formulae). We define a translation • of closed Σ B 0 -formulae as follows,

:= ⊥ := ⊥ X(t) := p X v (t) s t := ‡ ϕ ψ := ϕ ψ ∃x ≤ t.ϕ(x) := v (t) k=0 ϕ(k) ∀x ≤ t.ϕ(x) := v (t) k=0 ϕ(k)
for ∈ {≤, =} and ∈ {∨, ∧, ⊃}, where ‡ is if v (s) v (t) and ⊥ otherwise.

The following result can essentially be found in, e.g. [START_REF]Bounded arithmetic, propositional logic, and complexity theory[END_REF] or [START_REF] Cook | Logical Foundations of Proof Complexity[END_REF], but the initial idea was due to Paris and Wilkie [START_REF] Paris | ∆ 0 sets and induction[END_REF].

Theorem 8 (PW for proofs). A V 0 2 (or U 0 2 ) proof of a Π1-sentence ∀ x.ϕ( x) can be translated to quasipolynomial-size bounded-depth LK -proofs of ϕ( n) n∈N | x| .

In this paper we will be interested in adapting an extension of this result due to Krajícek, for U 1 2 .

Monotone and normal proofs in deep inference

The setting we use is due to Brünnler and McKinley [START_REF] Brünnler | Deep inference and its normal form of derivations[END_REF] [26], and independently Jeřábek [START_REF] Jeřábek | Proof complexity of the cut-free calculus of structures[END_REF]: tree-like MLK proofs can be represented as term rewriting derivations in the following system,9

w ↑ : ϕ → w ↓ : ⊥ → ϕ c↑ : ϕ → ϕ ∧ ϕ c↓ : ϕ ∨ ϕ → ϕ s : ϕ ∧ (ψ ∨ χ) → (ϕ ∧ ψ) ∨ χ (1)
modulo associativity and commutativity of ∧ and ∨ and the equa-

tions A ∧ = A = A ∨ ⊥, ∨ = and ⊥ ∧ ⊥ = ⊥.
Definition 9 (Normal proofs). A normal monotone proof is one where all ↑-steps occur before all ↓-steps.

Notation 10. We denote by MON the rewriting system in (1) above and by NOR the set of all normal monotone proofs.

For the sake of reducing prerequisites, we deal with MON and NOR in this paper rather than explicitly defining the associated deep inference proof systems, KS + and KS respectively.

In what follows we give a deep inference style presentation of rewriting derivations, first appearing in [START_REF] Guglielmi | A proof calculus which reduces syntactic bureaucracy[END_REF], in order to aid the analysis of normalisation complexity later on, e.g. in Sect. 3. Definition 11 (Derivations). We define derivations (or proofs), and premiss and conclusion functions, pr and cn resp., inductively:

• Each formula ϕ is a derivation with premiss and conclusion ϕ.

• For derivations π1, π2 and ∈ {∧, ∨}, π1 π2 is a derivation with premiss pr(π1) pr(π2) and conclusion cn(π1) cn(π2).

• If cn(π1) → pr(π2) an instance of a rule ρ then π1 ρ π2 is a derivation with premiss pr(π1) and conclusion cn(π2).

If π is a derivation where all inference steps are instances of rules in a system P with premiss ϕ, conclusion ψ, we write

ϕ π P ψ .
We now introduce a certain geometric abstraction of derivations, called atomic flows. They were first introduced in [START_REF] Guglielmi | Normalisation control in deep inference via atomic flows[END_REF], and the complexity of certain transformations were studied in [START_REF] Das | Complexity of deep inference via atomic flows[END_REF]. They can be thought of as specialised versions of Buss' flow graphs [START_REF] Samuel | The undecidability of k-provability[END_REF].

Definition 12 (Atomic flows). The (atomic) flow of a MON derivation is the (directed) graph obtained by tracing the paths of all atoms, designating nodes at w ↓, w ↑, c↓ and c↑ steps. Below we give an example of a MON-derivation and its associated flow,10 using colours to associate variable occurrences in the proof with edges in the flow:

p c↑ ----- p ∧ p ∨ ⊥ w↑ -- p c↑ ----- p ∧ p m ----------------------- p ∨ p c↓ ----- p = ---------- p ∨ ⊥ w↓ -- q ∧ p ∨ p c↓ ----- p s ----------------------- p c↑ ----- p ∧ p ∨ q ∧ p w↑ -- ⊤ = ---------- q (2)
Using flows, normalisation of monotone proofs can be conducted in an entirely 'syntax-free' way [START_REF] Guglielmi | Normalisation control in deep inference via atomic flows[END_REF]. In particular we have the following complexity bound from [START_REF] Das | Complexity of deep inference via atomic flows[END_REF]. Theorem 13. A MON proof π can be transformed into a NOR proof with the same premiss and conclusion in time polynomial in the number of maximal paths in the flow of π.

In this work it will suffice to estimate the number of paths by the following very simple upper bound: Fact 14. The number of maximal paths in a flow of length l is ≤ 2 l .

Monotone theories and translations

We first define some simple positive versions of the theories U i 2 and V i 2 , before considering certain extensions later, cf. [START_REF] Samuel | Bounded arithmetic, volume 1 of Studies in Proof Theory[END_REF]. Definition 15 (Positive classes and theories).

Σ B,+ i , Π B,+ i are the classes of positive Σ B i and Π B i formulae, resp. The theories M U i 2
and M V i 2 are defined as U i 2 and V i 2 , resp., but with induction and comprehension formulae required to be positive.

An important observation is that the usual argument proving

U 0 2 = V 0 2 , i.e. that Σ B 0 -PIND can simulate Σ B 0 -IND, cf. [9]
, cannot be carried out in the monotone setting due to the use of ⊃ symbols in that argument.

Strengthening by generalisations of comprehension

A problem with the theories defined above is that they are rather weak. Usually, the presence of induction in, say, U 1 2 allows one to 'iterate' comprehension to express more predicates. However, to prove this, we require a certain amount of negation, even if the final predicates are themselves positive. We address this problem by introducing the iterated comprehension axiom, and this will be later justified by a converse result from Sect. 4.3.

In the definition below, we assume we the presence of a pairing function allowing us to express sets of tuples [START_REF]Bounded arithmetic, propositional logic, and complexity theory[END_REF] [START_REF] Cook | Logical Foundations of Proof Complexity[END_REF]. Here, we write

(a, b) ≤ (a , b ) for a ≤ a ∧ b ≤ b . Definition 16 (Iterated comprehension). Length iterated compre- hension, denoted CA |ω| , is the following axiom schema: 11 ∃X ≤ ( a, b).∀( x, y) < ( a, b). y > 0 ⊃ X( x, y) ≡ ϕ x, y, X -, y 2 (3)
CAω is defined as CA |ω| but with (y -1) in place of y 2 . As we mentioned, this form of comprehension is already available in the presence of Σ B 1 -PIND:

Proposition 17. Σ B 1 -CA |ω| is provable in U 1 2 .
Proof. Let us denote (3) as IH (b) and proceed by induction on b.

For the inductive step, proving

IH (2b) from IH (b), we introduce a set X ≤ ( a, 2b) by Σ B 0 -CA such that: ∀( x, y) < ( a, 2b).[X ( x, y) ≡ ϕ( x, y, X(-, y 2 ))] (4)
Now, suppose y < b. We have that, X (x, 2y) ←→ ϕ( x, 2y, X( t1, y), . . . , X( tn, y)) ←→ ϕ( x, 2y, ϕ( t1, y, X(-, y

2 )), . . . , ϕ( tn, y, X(-, y 2 ))) ←→ ϕ( x, 2y, X ( t1, y), . . . , X ( tn, y))

where every occurrence of X in ϕ is indicated in the second line. The equivalences follow by (4), IH (b) and ( 4) respectively, and this finishes the proof of IH (2b). The proof of IH (2b + 1) is similar, and the base case follows from a single application of CA.

Notice that the above proof is constructive, a useful observation for when we consider intuitionistic theories in Sect. 4.3.

If ϕ is positive in (3), then we will see that the Paris-Wilkie translation can be adapted to find monotone propositional formulae witnessing this existential. Consequently, we consider theories obtained by adding

Σ B,+ 0 -CA |ω| to M U 1 2 and M V 1 2 . Notation 18. We write M U 1 2 for M U 0 2 + Σ B,+ 0 -CA |ω| , M V 0.5 2 for M V 0 2 + Σ B,+ 0 -CA |ω| and M V 1 2 for M V 0 2 + Σ B,+ 0 -CAω.
These theories are not conservative extensions, but we justify this notation by Prop. 17 above and the converse results in Sect. 4.3.

Witnessing set existentials by SO terms: part I

Second-order theories are often hasslesome for the Paris-Wilkie translation since it is not clear how to handle set quantifiers. They are often translated by extension variables, e.g. in [START_REF]Bounded arithmetic, propositional logic, and complexity theory[END_REF], although these may introduce negation in the propositional translation. 12For this reason we develop an appropriate term language for comprehension and thus eliminate occurrences of existential set quantifiers altogether. This result scales up to our intuitionistic theories later on, albeit with additional complications, which is helpful since notions of quantifier complexity beyond Σ B 0 are not well-defined in intuitionistic versions of arithmetic.

Definition 19 (Comprehension terms). We extend L2 by SO terms, a < t : ϕ and T ϕ, t parametrised by FO terms t, variables a and formulae ϕ. Φ-CT is the set of initial double-sequents,

x ∈ a < t : ϕ( a) ←→ x < t ∧ ϕ( x)
for each ϕ ∈ Φ, and Φ-CT |ω| is the set of initial double-sequents,

T ϕ, s,t ( x, y) ←→ y > 0 ∧ ( x, y) < ( s, t) ∧ ϕ(T ϕ, s,t (-, y 2
)) Intuitively, the initial sequents for CT |ω| evaluates the fixed point defined by the comprehension formula. It is not difficult to see that, over any SO theory, we have the following results: Proof. Follows from free-cut elimination, Thm. 5, and Lemma 20 above, replacing existentially quantified set variables by terms.

Finally, we can extend the Paris-Wilkie translation of closed formulae to account for comprehension terms.

Definition 22 (PW for comprehension terms). We define:

s ∈ a < t : ϕ := s < t ∧ ϕ( s) T ϕ, s,t ( r, u) := r ≤ s ∧ u < t ∧ ϕ(T ϕ, s,t (-, u 2 ))
Notice that the case of CT |ω| computes the fixed point of ϕ by a monotone propositional formula of low complexity: Fact 23. T ϕ, a,b ( s, t) has polylogarithmic depth and quasipolynomial size in v ( s), v (t), for CT |ω| .

Using CT |ω| we can, for example, express the threshold functions from [START_REF] Atserias | Monotone proofs of the pigeon hole principle[END_REF], [START_REF] Atserias | Monotone simulations of non-monotone proofs[END_REF] [8] [START_REF] Das | On the pigeonhole and related principles in deep inference and monotone systems[END_REF]:

th(x, a, 0) ←→ x = 0 ∨ (x = 1 ∧ a ∈ X) th(x, a, b) ←→ ∃y ≤ x. th(y, a, b 2 ) ∧ th(x -y, a + b 2 , b 2 )
Clearly, there are simple propositional proofs of the PW translations of the initial sequents from CT and CT |ω| .

Paris-Wilkie translation for monotone theories

We present a version of the Paris-Wilkie translation from our monotone theories to deep inference derivations, focussing on the length of the atomic flows obtained to derive complexity bounds for NOR later on. A minor contribution to the literature here is our presentation of the Paris-Wilkie translation in deep inference style, thanks in large part to insights from previous works, e.g. [START_REF] Brünnler | Deep inference and its normal form of derivations[END_REF] [22] [START_REF] Das | On the pigeonhole and related principles in deep inference and monotone systems[END_REF].

First, let us extend • to the LHS and RHS of sequents. We define Γ l as ϕ∈Γ ϕ and Γ r as ϕ∈Γ ϕ .

Definition 24 (PW for proofs). We extend the translation

• to proofs π( x) in M V 0.5 2 or M U 1 2 of a Σ B,+ 0 sequent Γ( x) → ∆( x),
mapping to derivations

Γ( n) l π( n) MON ∆( n) r
for n ∈ N | x| , by induction on the number of inference steps in π( x).

The most significant step, from the point of view of complexity is if a proof π(a) extended by an induction step:

Γ, ϕ(a) → ϕ(a + 1), ∆ IND Γ, ϕ(0) → ϕ(t), ∆
This is translated to the following derivation:

Γ l c↑ ------------ Γ l ∧ Γ l ∧ ϕ (0) = --------------------------------- Γ l c↑ ------------ Γ l ∧ Γ l ∧ Γ l ∧ ϕ (0) π(0) ϕ (1) ∨ ∆ r s --------------------------------------------- Γ l c↑ ------------ Γ l ∧ Γ l ∧    Γ l ∧ ϕ (1) π(1) ϕ (2) ∨ ∆ r ∨ ∆ r    s --------------------------------------------- . . . . . . . . . s --------------------------------------------------- Γ l ∧    Γ l ∧ ϕ (t -2) π(t-2) ϕ (t -1) ∨ ∆ r ∨ ∆ r ∨ ∆ r c↓ ------------- ∆ r    s --------------------------------------------------- Γ l ∧ ϕ (t -1) π(t-1) ϕ (t) ∨ ∆ r ∨ ∆ r ∨ ∆ r c↓ ------------- ∆ r = --------------------------------------- ϕ (t) ∨ ∆ r ∨ ∆ r c↓ ------------- ∆ r Γ l ϕ(0) π(0) π (1)
. . . . . . . . .

π(t -2) π(t -1) ϕ(t) ∆ r 4 2016/6/7
By following the path of the induction formula (in orange), notice that this multiplies the length of flow by v (t), a possibly quasipolynomial factor. The case for PIND is analogous to IND, but crucially the length of flow is only multiplied by log v (t) , a logarithmic factor.

A proof π(a) extended by a ∀-r step,

Γ, a ≤ t → ∆, ϕ(a) ∀-r Γ → ∆, ∀x ≤ t.ϕ(x)
is translated to the derivation below,

Γ l c↑ Γ l ∧ • • • ∧ Γ l ∧ = ∧ • • • ∧ = Γ l ∧ 0 ≤ t π(0) ∆ r ∨ ϕ(0) ∧ • • • ∧ Γ l ∧ v (t) ≤ t π(t) ∆ r ∨ ϕ(t) s ∆ r ∨ • • • ∨ ∆ r c↓ ∆ r ∨ v (t) k=0 ϕ(k) Γ l • • • v(t) • • • π(0) • • • π(t) • • • • • • ∆ r • • • v(t) k=0 φ(k)
where we notice that n ≤ t is for all n ≤ v(t). With regards to the length of the flow, besides that inherited from each π(i), notice that the v (t) c↑ nodes at the top (for each atom occurrence in Γ l ) can be implemented by a complete (almost) balanced tree of depth log v (t) , and similarly for the c↓ nodes corresponding to ∆ r . A proof π extended by a ∃-r step,

Γ → ∆, ϕ(s) ∃-r Γ, s ≤ t → ∆, ∃x ≤ t.ϕ(x)
is translated to the derivation below,

Γ l ∧ = Γ l π    ∆ r ∨ ϕ(s) w ↓ v (t) k=0 ϕ(k)    Γ l π ∆ r v(t) k=0 φ(k)
assuming v (s) ≤ v (t), and so s ≤ t is . Otherwise s ≤ t is ⊥ and the derivation is just composed of several w ↑ and w ↓ steps.

The composition of two proofs by cut is translated as follows:

π 1 Γ → ∆, ϕ π 2 Σ, ϕ → Π cut Γ, Σ → ∆, Π Γ l π 1 ∆ r ∨ ϕ ∧ Σ l s ∆ r ∨ ϕ ∧ Σ l π 2 Π r
This can be seen as a simpler version of the translation of an induction step, where the length of flows is increased by only a constant factor rather than a logarithmic factor. In a similar way, the translations of ∨ and ∧ steps are simpler versions of ∃ and ∀ steps, respectively, increasing flow length by at most addition of a constant rather than addition of a logarithm.

Finally, the translation of structural steps affect length of a flow by at most addition of a constant. The case for weakening, w-l and w-r, can also be seen as a simpler version of the case for ∃-r above. For instance, a proof π extended by a c-r step is translated as follows,

π Γ → ∆, ϕ, ϕ c-r Γ → ∆, ϕ Γ l π ∆ r ∨ ϕ ∨ ϕ c↓ ϕ
whence the case for c-l is dual.

A routine complexity analysis gives us the following:

Theorem 25. If M V 0.5 2 proves a Σ B,+ 0 sequent Γ( x) → ∆( x),
there are derivations

Γ( n) l MON ∆( n) r of size quasipolynomial in n ∈ N | x| .
3.4 • on M U 1 2 normalises in quasipolynomial time As we mentioned, • on PIND-steps multiplies the length of a flow by a polylogarithmic factor, due to the divide-and-conquer format of the induction.

Lemma 26. • on M U 1 2 proofs induces atomic flows of polylogarithmic length.

We can now apply the normalisation result, Thm. 13, and Fact 14 to obtain one of our main results:

Theorem 27. If M U 1 2 proves a Σ B,+ 0 sequent Γ( x) → ∆( x),
there are derivations

Γ( n) l NOR ∆( n) r of size quasipolynomial in n ∈ N | x| .

Intuitionistic theories and translations

Unfortunately, the monotone setting in arithmetic does not allow us to readily conduct metalogical reasoning, and so it does not seem possible to prove soundness results (or 'reflection' principles). Therefore we introduce an intuitionistic hierarchy of theories in which to conduct such reasoning. The idea here is to view intuitionistic implication under the Brouwer-Heyting-Kolmogorov interpretation, as a "transformation of proofs". In this way we can extend the PW-translation to deal with implication without breaking monotonicity. 13Remark 28. Previous work on intuitionistic bounded arithmetic has included only positive induction for versions of Buss' theory S 2 [START_REF] Samuel | The polynomial hierarchy and intuitionistic bounded arithmetic[END_REF] [START_REF] Cook | Functional interpretations of feasibly constructive arithmetic[END_REF], in order to conduct realizability arguments. In those settings one can, in fact, simulate the full power of non-positive induction, but it is not possible in our setting due to the presence of set symbols.

The hierarchy of type levels in intuitionistic logic

In order to simplify the definition of a higher type Paris-Wilkie translation later on, here we only work with formulae that are (∀, ∧, ⊃)-combinations of Σ B,+ 0 -formulae, as is common in realizability and Dialectica style interpretations. Disjunction and existentials, as expected, cause genuine difficulties that are cumbersome to deal with, cf. Sect. 6.4. Nonetheless, we point out that this fragment suffices to prove the various results in the converse direction that we seek, in particular Thm. 49, and so we still attain the required correspondence for this theory of arithmetic.

Definition 29 (Levels). Define L0 to be the set of positive formulae (of 'type level 0'). For j > 0 we define Lj as follows:

• If ϕ ∈ Lj-1 then ϕ ∈ Lj. • If ϕ ∈ Lj-1 and ψ ∈ Lj then ϕ ⊃ ψ ∈ Lj. • If ϕ ∈ Lj and ψ ∈ Lj then ϕ ∧ ψ ∈ Lj. • If ϕ ∈ Lj then ∀x ≤ t.ϕ ∈ Lj.
The set of bounded formulae of level j, Lj ∩Σ B 0 , is denoted Σ B,L j 0 . We write Σ B,L j 1 for the set of formulae ∃ X ≤ t.ϕ, for ϕ ∈ Σ B,L j 0 . We write LjJ and LjK to denote the fragments of LJ and LK , respectively, consisting of only (propositional) Lj formulae.

Henceforth, let us assume that theories are based over intuitionistic logic, unless otherwise mentioned.

Definition 30 (Intuitionistic theories). For i = 0, 1 define the theory IjU i 2 as U i 2 but with induction formulae in Σ B,L j i and comprehension formulae in Σ B,+ 0 .

Remark 31 (Quantifiers in intuitionistic logic). There is no canonical notion of quantifier hierarchy in intuitionistic logic, namely due to the lack of a general prenex normal form for formulae. Various hierarchies have been proposed for intuitionistic versions of bounded arithmetic, e.g. in [START_REF] Samuel | The polynomial hierarchy and intuitionistic bounded arithmetic[END_REF] [START_REF] Harnik | Provably total functions of intuitionistic bounded arithmetic[END_REF] in order to mimic associated complexity hierarchies, but this is beyond the scope of this work.

We point out that the notion of bounded formulae, Σ B 0 , remains the same in both the classical setting and the intuitionistic setting. Our notion of Σ B,L j 1 is in the 'strict' sense of [START_REF] Cook | Logical Foundations of Proof Complexity[END_REF], and we will later eliminate these existentials altogether in favour of a formulation using set terms, as in Sect. 3.2, allowing us to remain amongst Σ B 0 formulae where quantifier behaviour is more robust.

On the relative strength of theories

In this section we address the relative strength of our intuitionistic theories with the positive theories defined earlier, as well as their more well known classical versions.

From [START_REF] Samuel | The polynomial hierarchy and intuitionistic bounded arithmetic[END_REF] we have that the law of excluded middle holds for all quantifier-free formulae free of set symbols already in IS 2 , and so also I0U 0 2 , which helps prove some of the results here: Proposition 32 (Classical reasoning). If U 0 2 ϕ and ϕ is free of quantifiers and set symbols then I0U 0 2 ϕ.

By inspection of the rules, or by alluding to a multiple conclusion version of the intuitionistic calculus (e.g. from [START_REF] Dummett | Elements of intuitionism[END_REF]), notice that there are only two rules of LK 2 that cannot be simulated by LJ 2 : ⊃-r and ∀-r. In particular this yields the following, which was observed in [START_REF] Bílková | Monotone sequent calculus and resolution[END_REF]: Proposition 33. The positive propositional fragments MLJ and MLK of LJ and LK resp. polynomially simulate each other.

Both ⊃-r and ∀-r require restriction of one formula on the right to be intuitionistically valid. While the former is an inherently nonconstructive principle, the latter, which is freely available in M U i 2 and M V i 2 , can be simulated by an induction argument:

Proposition 34. I1U 1 2 ∀x ≤ t.(ϕ(x) ∨ ψ) → (∀x ≤ t.ϕ(x) ∨ ψ)
, where ϕ and ψ are Σ B,+ 0 and x does not occur free in ψ.

Proof. We reason inside the theory I1U 1 2 and prove the following L1 formula by polynomial induction on y:

∀y.∀x ≤ (t -y). ∀z ∈ [x, x + y).(ϕ(z) ∨ ψ) ⊃ ∀z ∈ [x, x + y).ϕ(z) ∨ ψ) (5)
Let χ(x, y) be such that the formula ( 5) is ∀y.∀x ≤ (ty).χ(x, y). The base case, when y = 0, is simple since the quantifiers in χ(x, y) collapse to enforcing z = x, whence χ(x, y) is equivalent to the identity formula (ϕ(x) ∨ ψ) ⊃ (ϕ(x) ∨ ψ). Now assume, for some b, we have that ∀x ≤ (t-b).χ(x, b), and let a ≤ (t -2b). We will attempt to show that χ(a, 2b). Notice that from a ≤ (t-2b) we have that a ≤ (t-b) and (a+b) ≤ (t-b), by classical reasoning and Prop. 32 above. Therefore, by the inductive hypothesis we have that χ(a, b) and χ(a + b, b). Now, let us assume the antecedent, say χ1(a, 2b), of χ(a, 2b), i.e. ∀z ∈ [a, a + 2b).(ϕ(z) ∨ ψ), and attempt to deduce the succedent, say χ2(a, 2b), i.e. ∀z ∈ [a, a+2b).ϕ(z)∨ψ. Notice that, due to the intuitionistic setting, we cannot at this point query the universal quantifier occurring in the succedent since it is underneath a disjunction. Instead, again by Prop. 32, we have:

c ∈ [a, a + 2b) ≡ c ∈ [a, a + b) ∨ c ∈ [a + b, a + 2b) (6)
Consequently, by the right-left direction of 6 above, from χ1(a, From here we can apply the left-right direction of ( 6) along with basic logical manipulations to obtain χ2(a, 2b) as required.

The inductive step for y = 2b + 1 is similar. The theorem now follows from ( 5) by setting y = t and conducting basic logical manipulations.

From here we arrive at a useful normal form for our higher-type Paris-Wilkie translation later on:

Corollary 35. Every Σ B,+ 0 -formula is equivalent in I1U 1 2 to one in prenex normal form.
The usual simulation of propositional MLK in propositional LJ , i.e. Prop. 33, is carried over by converting the succedents of MLK -sequents to disjunctions of their formulae. We just showed, in Prop. 34 above, that this approach also admits simulation of the ∀-r rule once L1-PIND is available.

The intuitionistic formulations of induction rules, with no sideformulae on the right, turn out to have equal strength to their classical formulations, by a routine argument. Furthermore, we can observe that the usual argument simulating IND from PIND, e.g. from [START_REF] Samuel | Handbook of proof theory[END_REF] or [START_REF] Samuel | Bounded arithmetic, volume 1 of Studies in Proof Theory[END_REF], is constructive and requires only an increase by 1 in the type-level of induction formulae:

Proposition 36. Σ B,L j+1 0 -PIND proves Σ B,L j 0 -IND, for j ≥ 0.
Finally, since the proof of Prop. 17 is constructive, we have:

Proposition 37. Σ B 1 -CA |ω| is provable in I1U 1 2 .
Proof. Only Σ B,L 1

1

-PIND is used in the proof of Prop. 17.

We can now conclude the following.

Theorem 38 (Inclusions).

I0U 1 2 ⊆ M U 1 2 ⊆ M V 0.5 2 ⊆ I1U 1 2 .
Proof. The first two inclusions are routine. The final inclusion follows from Props. 33, 34, 36 and 37.

Witnessing set existentials by SO terms: part II

For the same reasons as Sect. 3.2, and the difficulty of handling quantifiers in intuitionistic logic, we wish to eliminate occurrences of second-order quantification in our intuitionistic theories. The arguments are a little more involved now that we have access to induction on more complex formulae, but we are nonetheless able to work with the same comprehension terms and rules as before.

We will assume that every Σ B,L j 1 formula has just one secondorder existential quantifier. 14 Our main witnessing lemma is the following: Lemma 39. Suppose j > 0 and IjU 1 2 Γ( a, A) → ∃X.ϕ(X, a, A), where all free variables are indicated. Then there is a Σ B,+ 0 -CT |ω| term T ( a, A) such that IjU 1 2 Γ( a, A) → ϕ(T ( a, A), a, A).

Proof sketch. By induction on the number of inference steps in a free-cut free proof π. The only problematic case is when π consists of a subproof π followed by a PIND step,

Γ, ∃X ≤ s.ϕ(X, a 2 ) → ∃X ≤ s.ϕ(X, a) PIND Γ, ∃X ≤ s.ϕ(X, 0) → ∃X ≤ s.ϕ(X, t)
with free variables amongst a, A. We then have a proof of, Γ, A ≤ s, ϕ(A, a 2 ) → ∃X.ϕ(X, a) from which we have a term R(A) (with free variables from a, A), by the inductive hypothesis, and a proof π (A) of: ,s,y 2 ))(x) Finally, we can apply PIND after π (TR,s,a) to obtain a proof of the required format.

Γ, A ≤ s, ϕ(A, a 2 ) → R(A) ≤ s ∧ ϕ(R(A),
From here we can obtain our quantifier-elimination result:

Theorem 40. For j > 0, IjU 1 2 is equivalent to IjU 0 2 +Σ B,+ 0 -CT |ω| over Σ B,+ 0 -theorems.
Proof. Since the proof of Prop. 17 can be made constructive in I1U 1 2 , and so the theorem follows from Lemma 39 above.

Notation 41. Following the shorthands from Sect. 3, we will write For convenience we will switch back to the sequent calculus presentation of monotone proofs, MLK , whose tree-like variant is polynomially equivalent to MON [START_REF] Jeřábek | Proof complexity of the cut-free calculus of structures[END_REF]. It is just as simple to conduct the translation to MON, but already existing concepts and terminology for the sequent calculus makes it slightly easier to explain the translation; in particular, the existence of a sequent arrow (→) at the meta-level makes it simple to translate implications between monotone formulae to monotone sequents. This way, it will also be clearer from our translation how to obtain a correspondence for dag-like MLK , for which there is no standard definition of a corresponding system based on MON.

As expected for realizability-style translations, it is contractive behaviour that generates complexity, this time in the dependency graph of a dag-like MLK proof. However, the length of this graph is tamed just like in Sect. 3.4, by relying on PIND.

Definition 42 (Formula and sequent translation). Set ⟪•⟫ 0 = • , and for j > 0, we define a translation ⟪•⟫ j from closed bounded Lj formulae to multisets of propositional Lj-1 sequents as follows:

• If ϕ ∈ Lj-1 then, ⟪ϕ⟫ j := { → ϕ } • If ϕ ∈ Lj-1 and ψ ∈ Lj then: ⟪ϕ ⊃ ψ⟫ j := ϕ , Γ → ∆ : Γ → ∆ ∈ ⟪ψ⟫ j • If ϕ, ψ ∈ Lj then ⟪ϕ ∧ ψ⟫ j := ⟪ϕ⟫ j ∪ ⟪ψ⟫ j . • If ϕ ∈ Lj then ⟪∀x ≤ t.ϕ(x)⟫ j := v (t) k=0 ⟪ϕ(k)⟫ j . • For a cedent Γ of Lj formulae, ⟪Γ⟫ := ϕ∈Γ ⟪ϕ⟫ j .
In what follows, we will use S and its decorations to vary over sequents, and we write S π S for a (dag-like) sequent derivation called π with premisses the (multi)set or list S and conclusion S. Before proceeding to give the generalised Paris-Wilkie translation of IjU 1 2 proofs, we first give a version of the deduction theorem that will be useful, e.g. for the ⊃-r case in our translation. Proof. The right-left direction is simply obtained by cutting → ϕ against the conclusion ϕ → ψ of π . For the left-right direction, we append the cedent ϕ to the left-hand side of all sequents occurring in the derivation π:

ϕ → ϕ ϕ,π ϕ → ψ
. It is not difficult to see that the derivation remains valid in LjJ and, moreover, begins with a correct initial sequent.

Definition 44 (Translation of proofs). For j > 0, an ĪjU

1 2 or ĪjV 0.5 2 proof π of a sequent Σ → ϕ is translated by ⟪•⟫ j to a multiset of (dag-like) Lj-1J derivations of the following format:    ⟪Σ⟫ j ⟪π⟫ j S S : S ∈ ⟪ϕ⟫ j   
The translation is again by induction on the structure of an arithmetic proof π. We give some key steps in the translation below, henceforth fixing j and suppressing it in superscripts.

If π consists of subproofs π1 and π2 followed by a cut step,

Σ → ϕ Π, ϕ → ψ cut Π, Σ → ψ
then by the inductive hypothesis we have derivations

⟪Σ⟫ ⟪π 1 ⟫ S S
for each S ∈ ⟪ϕ⟫, and derivations ⟪Π⟫ ⟪ϕ⟫

⟪π 2 ⟫ S S
for each S ∈ ⟪ψ⟫. Let ⟪ϕ⟫ = {Si : i ≤ n} and, for each S ∈ ⟪ψ⟫, we define,

⟪π⟫ S := ⟪Π⟫ ⟪Σ⟫ ⟪π 1 ⟫ S 0 S0 ⟪π 1 ⟫ S 1 . . . ⟪π 1 ⟫ Sn Sn ⟪π 2 ⟫ S S
where ⟪Σ⟫ is used once for each ⟪π1⟫ S i .

If π consists of a subproof π followed by a c-l step,

Γ, ϕ, ϕ → ψ c-l Γ, ϕ → ψ
then, for S ∈ ⟪ψ⟫, ⟪π⟫ S is defined as ⟪π ⟫ S , deleting one of the occurrences of each formula χ in ⟪ϕ⟫; from the point of view of the dependency graph, any later sequents previously relying on the deleted occurrence now rely on the remaining occurrence of χ.

If a proof π consists of a subproof π followed by a ⊃-r step,

Σ, ϕ → ψ ⊃ -r Σ → ϕ ⊃ ψ
then, again, notice that ϕ must be in Lj-1, since ϕ ⊃ ψ must be in Lj. Therefore, by the inductive hypothesis, we have derivations

⟪Σ⟫ → ϕ ⟪π ⟫ S S
for each S ∈ ⟪ψ⟫. From here, we can obtain a definition of ⟪π⟫ S of the appropriate format by simply applying the deduction theorem, Lemma 43. If π consists of subproofs π1 and π2 followed by a ⊃-l step,

Σ → ϕ Π, ψ → χ ⊃ -l Π, ϕ ⊃ ψ, Σ → χ
then notice that ϕ must be Lj-1, since ϕ ⊃ ψ must be in Lj. Therefore, by the inductive hypothesis, we have a derivation

⟪Σ⟫ ⟪π 1 ⟫ ϕ → ϕ
and derivations ⟪Π⟫ ⟪ψ⟫

⟪π 2 ⟫ S S
for each S ∈ ⟪χ⟫.

Let ⟪ψ⟫ = {Γi → ∆i : i ≤ n} and, for S ∈ ⟪χ⟫, we define,

⟪π⟫ S := ⟪Π⟫ ϕ , Γ0 → ∆0 ⟪ϕ⊃ψ⟫ ϕ , Γn → ∆n ⟪Σ⟫ ⟪π 1 ⟫ ϕ → ϕ Γ0 → ∆0 cut Γn → ∆n ⟪π 2 ⟫ S S
where the sequence of formulae marked cut is obtained by cutting the sequent → ϕ against each ϕ , Γi → ∆i in ⟪ϕ ⊃ ψ⟫.

The ∀ rules are rather simple. The rule ∀-l amounts to adding further premisses to an existing derivation, while ∀-r essentially follows from expanding out the definition of ⟪•⟫ on universally quantified formulae.

For the extension of a proof by an induction step, the definition of ⟪•⟫ is obtained by first converting the induction into finitely many instances of cut (the number determined by the value of the closed term in the succedent of the lower sequent), like in the definition of • , and then applying the definition of ⟪•⟫ for the case of cut steps. This may increase the length of the dependency graph by a logarithmic factor in the case of ĪjU proofs can be made treelike in quasipolynomial time. We omit a complexity analysis here, for brevity, but remark that the argument is not dissimilar to that for • on M U 0 2 and its variations. Essentially, the length of the dependency graph of an Lj-1J proof in the image of ⟪•⟫ j is bounded by a polylogarithm in the size of the arguments in the conclusion, due to the use of only polynomial induction steps, and so 'unwinding' the proof to tree-like form takes quasipolynomialtime. The argument also bears semblance to that used in [START_REF]Bounded arithmetic, propositional logic, and complexity theory[END_REF] for the theory U 1 1 (or equivalently U 1 2 ), where it is extension variables rather than dagness that needs to be unwound in a proof. theorem, π has a dependency graph of length polylogarithmic in n.

Finally, by considering the special case when j = 1 and the aforementioned correspondence between tree-like MLK and MON, we arrive at one of our main results:

Corollary 46. If I1U 1 2 proves a Σ B,+ 0 sequent Γ → ∆ then there are quasipolynomial-size MON proofs Γ l ∆ r
, or equivalently treelike MLK proofs of Γ l → ∆ r .

Reflection principles

The reflection principle for a propositional proof system (PPS) is a formal statement of its soundness. Proofs in arithmetic theories of such principles serve as converses of propositional translations (e.g. Paris-Wilkie), since they guarantee that the theory is amongst the strongest for which such a translation could exist. Due to the criteria of positivity and level we must be careful about how to formalise sequences and data structures. Therefore we take a mixed approach, using individual variables (on which negation may occur) to code formulae and proofs, as often done in subsystems of Buss' S i 2 and T i 2 , using set variables to code the truth of the formula, as is usually done for subsystems of U i 2 and V i 2 [START_REF]Bounded arithmetic, propositional logic, and complexity theory[END_REF]. This is also the reason why we include the # symbol in all our theories, since it is required to carry out such a coding. 15We do not present the full formalisation here, but assume we have access to the following Σ B,+ 0 -formulae free of set variables:

• Fla + (x) : "x codes a positive formula".

• DerP (x, y, z) : Fla + (y) ∧ Fla + (z) ∧ "x codes a P -derivation from y to z".

We assume that their basic properties are provable in U 0 2 (and so I0U 0 2 and M U 0 2 ) cf. [START_REF]Bounded arithmetic, propositional logic, and complexity theory[END_REF]. We also need a formula, Tr + (x) : Fla + (x) ∧ "the formula coded by x is true" obtained by Σ B,+ 0 -CA |ω| and so containing set variables. In order to do this we need to use a monotone variation of Spira's theorem, stating that every formula can be polyomially transformed into an equivalent one that is balanced, i.e. has logarithmic depth.

The exposition follows that in [START_REF]Bounded arithmetic, propositional logic, and complexity theory[END_REF], taking care to preserve monotonicity. For brevity, let us suppose we have such formulae, and that Tr + (x) is logically equivalent to the propositional formula coded by x, witnessed by short proofs in NOR.

Definition 47 (Positive reflection). For a PPS P , we define:

Rfn + P := ∀x, y, z.(DerP (x, y, z) ⊃ (Tr + (y) ⊃ Tr + (z))) (7
) Recall that a (propositional) monotone implication is a propositional formula ϕ ⊃ ψ where ϕ and ψ are free of ⊃ symbols.

Proposition 48 (Quasipolynomial simulation). For a PPS P :

1. If M U Proof. Let us consider 1, whence the case for 2 is analogous. Applying Thm. 25 16 we arrive at quasipolynomial-size families of propositional derivations:

DerP (l, m, n) ∧ Tr + (m) π(l,m,n) NOR Tr + (n)
for l, m, n ∈ N. Consider a P -proof π ϕ,ψ of a monotone implication ϕ ⊃ ψ, and let us write α for the code of some (finite) object. Notice that DerP ( π ϕ,ψ , ϕ , ψ ) is true and contains no set symbols, so its image under • is simply a Boolean combination of constant symbols, which can be evaluated even in NOR. Finally, recall that Tr + ( χ ) is provably equivalent to χ by short proofs in NOR, for any positive propositional formula χ, and so we can construct from π( π ϕ,ψ , ϕ , ψ ) quasipolynomial-size derivations of the format by polynomial induction on w, whence the result follows by BASIC . In the inductive step we apply the inductive hypothesis to the first half and second half of a MON rewriting derivation, thence applying cuts to derive the inductive step. In order to construct divide-and-conquer style arguments on MON proofs, we may represent them as usual rewriting derivations that are simply lists of formulae (i.e. 'Calculus of Structures' style [START_REF] Brünnler | A local system for classical logic[END_REF]).17

Further remarks

We briefly present some further points related to this work and discuss some ongoing research.

Variants of

V 1 2
We have discussed mostly the monotone and intuitionistic versions of U 1 2 and the versions of V 1 2 with only Σ B,L 1 0 -PIND rather than Σ B,L 1 0 -IND, our so-called 'V 0.5 2 ' theories. We believe that all the expected results for M V 1 2 and I1V 1 2 go through, namely that both translate to dag-like MLK derivations with extension variables, cf. [START_REF] Jeřábek | Proofs with monotone cuts[END_REF], and the latter is able to prove its soundness.

In a recent line of work by Straßburger et al., variants of KS (or NOR) with extension have been studied [START_REF] Straßburger | Extension without cut[END_REF], so it would be interesting to see what blend of rules corresponds to those systems. The answer does not seem obvious since, as soon as we add Σ B,L 1 0 -IND we inherit Σ B,+ 0 -IND, and so cannot distinguish normal proofs from monotone proofs.

Counting arguments and further reflection principles

It is known that tree-like MLK can quasipolynomially simulate LK over monotone sequents [START_REF] Atserias | Monotone proofs of the pigeon hole principle[END_REF], and this (along with [START_REF] Atserias | Monotone proofs of the pigeon hole principle[END_REF] [16] etc.) is one of the main sources of inspiration for this work.

The proof relies crucially on monotone formulae computing the threshold function, for which we constructed SO terms at the end of Sect. 3.2. In all these works, the crucial point is to find short proofs witnessing the symmetry of threshold functions. While Atserias et al. achieved this for tree-like MLK (or MON), this is also achievable for NOR, albeit via a more complicated proof, and this was used in [START_REF] Das | On the pigeonhole and related principles in deep inference and monotone systems[END_REF] to construct quasipolynomial-size proofs of the propositional pigeonhole principle in NOR.

To show the usefulness of our monotone theories, in ongoing work we show that M U 1 2 proves the correctness of merge-sort, and so can prove the symmetry of threshold functions, subsuming the results of [START_REF] Das | On the pigeonhole and related principles in deep inference and monotone systems[END_REF]. We would be interested in taking this further, finding new upper bounds and separations via these natural theories.

Can we reproduce Atserias et al.'s result using purely logical tools, instead of complex counting arguments? A corollary of their result is that the intuitionistic calculus LJ quasipolynomially simulates LK over monotone sequents. Can we perhaps reproduce this result or something in between, say for IjU 1 2 for some large but finite j? A potentially fruitful idea is given in the next subsection; an answer to this question might have ramifications for more general questions in monotone proof complexity.

(∀, ⊃)-classical logic and Pierce's law

There are several difficulties with attempting to extend some of our results to the classical setting, but such results could provide a purely logical analogue to results in, say, [START_REF] Atserias | Monotone simulations of non-monotone proofs[END_REF], which rely on complex combinatorial arguments.

Over the (∀, ⊃)-fragment of the language we can recover classical reasoning by what is known as Pierce's law:

((ϕ ⊃ ψ) ⊃ ϕ) ⊃ ϕ or the rule Σ, ϕ ⊃ ψ → ϕ Σ → ϕ
In fact, when dealing with only L1-proofs, we can actually realize this law by (tree-like) MLK derivations, where ⟪π⟫ ϕ , ϕ is obtained by appending ϕ to the succedent of every sequent in ⟪π⟫ ϕ . Notice that, while this transformation is valid in MLK it is not, in general, valid for LjJ due to the restriction on the ⊃-r rule.

The problem with implementing this is the fact that we do not have much control on the logical complexity of ψ. Nonetheless, in ongoing work we are exploring fragments of classical U 1 2 for which a translation to MLK may still be attained.

Disjunction in the intuitionistic setting

We have not dealt with disjunction in the intuitionistic setting in favour of easing the translation. As one might expect, things become very cumbersome, with particular complications arising since our base type includes all monotone formulae. One might extend the class Lj by taking advantage of Harrop or hereditarily Harrop formulae, cf. [START_REF] Samuel | Handbook of proof theory[END_REF], which allows us to preserve the disjunction property of intuitionistic logic in the presence of contexts. This approach bears semblance with the V 1 -HORN theory presented in [START_REF] Cook | Logical Foundations of Proof Complexity[END_REF] which limits induction to a generalisation of Horn clauses.

Another approach might be to use a variant of the deep inference medial rule [START_REF] Brünnler | A local system for classical logic[END_REF] to manipulate disjunctions of implications:

(ϕ ⊃ ψ) ∨ (ϕ ⊃ ψ ) → (ϕ ∧ ϕ ) ⊃ (ψ ∨ ψ ) 9
2016/6/7

6.5 Towards a theory for NOR

We do not yet have a full correspondence for NOR, and this reflects the difficulty in deep inference proof complexity of conducting any metalogical reasoning at all in NOR, or KS. One approach might be to incorporate structural restrictions from linear logic, e.g. that induction formulae must be free of modalities, like in [START_REF] Bellantoni | A new "feasible" arithmetic[END_REF]. This could also allow us to complete the higher-types version of the PWtranslation by allowing recursive application of ⟪•⟫, using linearity to control resource usage. While this might not be desirable from the point of view of reasoning, it might allow us to conduct oneoff proofs of soundness of various systems, thereby settling certain proof complexity questions.

Conclusions

We gave uniform versions of monotone and analytic deep inference proof systems, in the setting of bounded arithmetic. This constituted an application of a characterisation of certain provable fixed points, deep inference proof normalisation and intuitionistic bounded arithmetic to propositional proof complexity. In the case of monotone proofs we were able to also prove a converse result. This work further brings research in deep inference in line with the standards of mainstream proof complexity. By studying restrictions of monotone systems we also contribute to 'bridging the gap' between weak systems and Hilbert-Frege systems (for which no nontrivial lower bounds are known), providing finer granularity of the various subproblems.

Lemma 20 . 2 and M V 1 2

 2022 Φ-CT , Φ-CT |ω| and Φ-CT ω conservatively extend Φ-CA, Φ-CA |ω| and Φ-CAω resp. Theorem 21. Σ B,+ 0 theorems of M U 1 2 , M V 0.5 have proofs containing only Σ B,+ 0 -formulae, using CT |ω| , CT |ω| and CT ω resp. instead of CA.

  2b) we can deduce ∀z ∈ [a, a+b).(ϕ(z)∨ψ) and ∀z ∈ [a+b, a+2b), i.e. χ1(a, b) and χ1(a + b, b).(ϕ(z) ∨ ψ). Finally, since we already have χ(a, b) and χ(a + b, b) from the inductive hypothesis, we can conclude χ2(a, b) and χ2(a + b, b).

  a) Now, by Σ B,+ 0 -CT |ω| , we have a term TR,s,a and initial sequents: TR,s,a(x, y) ←→ y > 0∧(x, y) < (s, a)∧R(TR

Lemma 43 (

 43 Deduction). An LjJ derivation → ϕ π → ψ can be polynomially transformed to an LjJ proof π of ϕ → ψ, and vice-versa.

Theorem 45 ( 5 2

 455 Complexity of ⟪•⟫). If ĪjV 0.proves an Lj sequent Σ( x) → ϕ( x), there are Lj-1J derivations ⟪Σ( n)⟫ π S for each S ∈ ⟪A( n)⟫ of size quasipolynomial in n and, if it is a ĪjU 1 2

  we give the following result which, in light of Prop. 48 above, provides a form of converse to Cor. 46. Theorem 49. I1U 1 2 proves Rfn + MON . Proof sketch. We prove the following Σ B,L 1 0 -formula, ∀x, y, z < w.(DerMON(x, y, z) ⊃ (Tr + (y) ⊃ Tr + (z)))

1 →

 1 ∆ 1 , ϕ w ϕ , Γn → ∆n, ϕ ⟪π⟫ ϕ , ϕ → ϕ , ϕ → ϕ

A quasipolynomial is a function 2 log O(1) n .

In fact, it is widely believed that a polynomial simulation holds, cf.[START_REF] Jeřábek | A sorting network in bounded arithmetic[END_REF].

Indeed, it was in this setting that the aforementioned quasipolynomial simulation was first proved[START_REF] Atserias | Monotone simulations of non-monotone proofs[END_REF].

We choose not to work in the framework developed by Cook and Nguyen[START_REF] Cook | Logical Foundations of Proof Complexity[END_REF] since many relevant distinctions, e.g. polynomial induction vs. regular induction, seem to collapse in that setting.

Such an X would formally have s in superscript, i.e. written X s , in[START_REF]Bounded arithmetic, propositional logic, and complexity theory[END_REF]. 2 2016/6/7

Strictly speaking, this is not a term rewriting system (TRS) due to the fact that the LHS of c↑ and w ↑ is just a variable, but the notions of reduction, derivation etc. otherwise remain the same as for a TRS.

In this derivation we also make use of the medial rule, given by m :(ϕ 1 ∧ ϕ 2 ) ∨ (ψ 1 ∧ ψ 2 ) → (ϕ 1 ∨ ψ 1 ) ∧ (ϕ 2 ∨ ψ 2 ), to show how c↑ and c↓ steps can be reduced to atomic form.

The notation ϕ(X(-)) formally corresponds to the formula ϕ(λ x.X x), where the meta-level λ binder is used for formal abstraction. 3 2016/6/7

Intuitively, one expects that this negation can be eliminated, but existing versions of free-cut elimination, e.g. from[START_REF] Cook | Logical Foundations of Proof Complexity[END_REF], do not quite yield this.

Such an approach is not generally available in classical logic due to De Morgan laws, which induce a collapse of negation to the atoms. 5 2016/6/7

This can be achieved by the usual trick of string interleaving, cf.[START_REF] Cook | Logical Foundations of Proof Complexity[END_REF].[START_REF] Brünnler | A local system for classical logic[END_REF] 2016/6/7

2016/6/7

We do not lose much, however, since quasipolynomials pop up from various locations in the propositional translations presented, not just #. 8 2016/6/7

In the case of 2 we should apply 27 or Cor. 46, as appropriate.

This representation is at most quadratically larger than the deep inference representation of Sect. 2.3.

Acknowledgements I would like to thank Arnold Beckmann for many helpful conversations on this line of research. I would also like to thank Paola Bruscoli, Alessio Guglielmi, Tom Gundersen, Lutz Straßburger and others in the deep inference community for their feedback on early versions of this work. This work has been partially supported by the ANR-14-CE25-0005 Elica project.


Vincent Lefèvre

Jean-Michel Muller

Some notes on the possible under/overflow of the most common elementary functions

The purpose of this short note is not to describe when underflow or overflow must be signalled (it is quite clear that the rules are the same as for the basic arithmetic operations). We just want to show that for some of the most common functions and floating-point formats, in many cases, we can know in advance that the results will always lie in the range of the numbers that are representable by normal FP numbers, so that in these cases there is no need to worry about underflow or overflow. Note that when it is not the case, an implementation is still possible using a run-time test.

When the input argument is not near zero

The most tricky part is with the direct trigonometric functions of large arguments. Can a floating-point number be so close to an integer multiple of π/2 that its sine or cosine is smaller than the smallest normal FP number of the format being considered, or that its tangent is larger than the largest finite FP number?

A method based on the continued-fraction theory allows to find, in a given format, the FP number that is closest to a multiple of a given irrational constant. That method was first suggested by Kahan [START_REF] Kahan | Minimizing q*m-n[END_REF] for finding the precision with which range-reduction of trigonometric functions should be carried-on (a C-program that implements that method without needing extra-precision arithmetic was written by Kahan and McDonald). A similar method was found later by Smith [START_REF] Smith | A continued-fraction analysis of trigonometric argument reduction[END_REF]. That method is presented in Muller's book [START_REF] Muller | Elementary Functions, Algorithms and Implementation[END_REF]. A good reference on continued fractions is Stark's book [START_REF] Stark | An Introduction to Number Theory[END_REF].

In the next sections, I give the results obtained for the formats defined by the new draft standard. I also include a Maple program that allows one to find the number (not near zero, of course) closest to a multiple of π/2 for any FP format. 1

Binary32 format

The FP number greater than 2 -20 in the Binary32 format that is closest to an integer multiple of π/2 is

M Bin32 = 16367173 × 2 72
we have,

ǫ = |M Bin32 -49205481242904147824922835605 × π/2| = 1.6147697982476211 • • • × 10 -9 ≈ 2 -29.206
This means that if x is a Binary32 number of absolute value greater than 2 -20 , then

Binary64 format

The FP number greater than 2 -20 in the Binary64 format that is closest to an integer multiple of π/2 is

M Bin64 = 6381956970095103 × 2 797
Its distance to the nearest integer multiple of π/2 is

ǫ = 4.6871659242546276111 • • • × 10 -19 ≈ 2 -60.8879
This means that if x is a Binary64 number of absolute value greater than 2 -20 , then

• | sin(x)| or | cos(x)| will never be less than sin(ǫ) ≈ 2 -60.8879 ,

• | tan(x)| will never be less than tan(ǫ) ≈ 2 -60.8879 (same for the cotangent function),

• | tan(x)| will never be larger than tan(π/2 -ǫ) ≈ 2 +60.8879 (same for the cotangent function).

These values are representable as normal numbers in the Binary64 format. As a consequence, the sine, cosine, tangent, cotangent, secant, cosecant of a Binary64 number not near zero cannot underflow nor overflow.

Binary128 format

The FP number greater than 2 -20 in the Binary128 format that is closest to an integer multiple of π/2 is

M Bin128 = 8794873135033829349702184924722639 × 2 1852
Its distance to the nearest integer multiple of π/2 is

ǫ = 7.88136000827235 × 10 -38 ≈ 2 -123.2548
This means that if x is a Binary128 number of absolute value greater than 2 -20 , then

• | sin(x)| or | cos(x)| will never be less than sin(ǫ) ≈ 2 -123.2548 ,
• | tan(x)| will never be less than tan(ǫ) ≈ 2 -123.2548 (same for the cotangent function),

• | tan(x)| will never be larger than tan

(π/2 -ǫ) = 1.2688 • • • × 10 37 ≈ 2 +123
.2548 (same for the cotangent function).

These values are representable as normal numbers in the Binary128 format. As a consequence, the sine, cosine, tangent, cotangent, secant, cosecant of a Binary128 number not near zero cannot underflow nor overflow.

Decimal32 format

The FP number greater than 2 -20 in the Decimal32 format that is closest to an integer multiple of π/2 is

M Dec32 = 4327189 × 10 42
we have,

ǫ = M Dec32 -2754774076171501944361681452576588198950125599968 × π/2 = 1.8908070677421251636 • • • × 10 -10
This means that if x is a Decimal32 number of absolute value greater than 2 -20 , then

• | sin(x)| or | cos(x)| will never be less than sin(ǫ) ≈ 1.89 • • • × 10 -10 ,
• | tan(x)| will never be less than tan(ǫ) ≈ 1.89 • • • × 10 -10 (same for the cotangent function),

• | tan(x)| will never be larger than tan(π/2 -ǫ) ≈ 5288746890 (same for the cotangent function).

These values are representable as normal numbers in the Decimal32 format. As a consequence, the sine, cosine, tangent, cotangent, secant, cosecant of a Decimal32 number not near zero cannot underflow nor overflow.

Decimal64 format

The FP number greater than 2 -20 in the Decimal64 format that is closest to an integer multiple of π/2 is

M Dec64 = 8919302781369317 × 10 296
Its distance to the nearest integer multiple of π/2 is

ǫ = 6.05527439099688 • • • × 10 -20
This means that if x is a Decimal64 number of absolute value greater than 2 -20 , then

• | sin(x)| or | cos(x)| will never be less than sin(ǫ) ≈ 6.05 × 10 -20 ,

• | tan(x)| will never be less than tan(ǫ) ≈ 6.05 × 10 -20 (same for the cotangent function),

• | tan(x)| will never be larger than tan(π/2 -ǫ) ≈ 1.65 × 10 19 (same for the cotangent function).

These values are representable as normal numbers in the Decimal64 format. As a consequence, the sine, cosine, tangent, cotangent, secant, cosecant of a Decimal64 number not near zero cannot underflow nor overflow.

Decimal128 format

The FP number greater than 2 -20 in the Decimal128 format that is closest to an integer multiple of π/2 is

M Dec128 = 9308532438209917461067659354862169 × 10 4639 .
Its distance to the nearest integer multiple of π/2 is

ǫ = 2.06901398954 • • • × 10 -38
This means that if x is a Decimal128 number of absolute value greater than 2 -20 , then • | sin(x)| or | cos(x)| will never be less than sin(ǫ) ≈ 2.069 × 10 -38 ,

• | tan(x)| will never be less than tan(ǫ) ≈ 2.069 × 10 -38 (same for the cotangent function),

• | tan(x)| will never be larger than tan(π/2 -ǫ) ≈ 4.83 • • • × 10 37 (same for the cotangent function).

These values are representable as normal numbers in the Decimal128 format. As a consequence, the sine, cosine, tangent, cotangent, secant, cosecant of a Decimal128 number not near zero cannot underflow nor overflow.

The function is null at zero

A frequent case with the common elementary functions is the case where the derivative of the function at zero is 1. Let us call f the function.

In many cases (log(1 + x) for x < 0, tan(x), arcsin(x), sinh(x), tanh -1 (x)), |f (x)| is (very slightly) larger than |x| for x near zero. This means that near zero these functions shall not return a subnormal number (hence, we shall not signal underflow) if x is not a subnormal number. Still with the same functions, if x is a subnormal number, with any "reasonable" format (see below for an explanation of what is a "reasonable" format):

• in round-to-nearest, roundTowardsZero, roundTowardsPositive (for x < 0) and roundTowardsNegative (for x > 0) modes, the correctly rounded value of f (x) will be a subnormal number;

• in roundTowardsPositive (for x > 0) and roundTowardsNegative (for x < 0) modes, f (x) will be a subnormal number, unless |x| is the largest subnormal number (i.e., b emin -b emin+1-p , where b is the base and p the precision). In that last case, the correctly rounded value of f (x) will be sign(x) times b emin (hence, the correctly rounded value of f (x) will be a normal number). Now, when |f (x)| is (very slightly) less than |x| for x near zero (which happens for functions log(1 + x) for x < 0, sin(x) arctan(x), sinh -1 (x), tanh(x)), the situation is symmetrical. If x is a subnormal number, then the correctly rounded value of f (x) is a subnormal (or zero) number too. Still with the same functions, if x is a normal number, then with any "reasonable" format:

• in round-to-nearest, roundTowardsPositive (for x > 0) and roundToward-sNegative (for x < 0) modes, the correctly rounded value of f (x) will be a normal number too, so we shall not signal underflow;

• in roundTowardsZero, roundTowardsPositive (for x < 0) and roundTo-wardsNegative (for x > 0) modes, the correctly rounded value of f (x) will be a normal number, unless |x| is the smallest normal number b emin . In that case, the correctly rounded value of f (x) is sign(x) times the largest subnormal number (ie., sign(x) times b emin -b emin+1-p ). Now, let us explain with an example what we mean by a "reasonable" format. Consider function arctan, and rounding towards zero, with base b and precision p. We know that when computing arctan(b emin ) (reminder: b emin is the smallest normal number), we should return a subnormal number (hence, we have an underflow). Can this happen with larger input numbers? Let us try to see at which condition we are sure that arctan(nextU P (b emin )) is larger than b emin . From the power series arctan(x) = x - This will be larger than b emin as soon as

b 2emin+p-1 (1 + b -p+1 ) 3 ≤ 3.
This condition is satisfied by far by all formats of IEEE-754 and the current draft format. For instance, with the Binary64 format, b 2emin+p-1 (1+b -p+1 ) 3 ≈ 2.23× 10 -600 , and with the Decimal128 format b 2emin+p-1 (1 + b -p+1 ) 3 ≈ 10 -12253 .

The function goes to infinity at zero

Unless log(b)|emin + 1 -p| > b emax (b -b 1-p ) (which would require a pretty stupid FP format), the absolute value of the logarithm of a positive FP number is much smaller than the overflow threshold. Since csc(x) ∼ 1/x near zero, it can overflow (the study is very similar to that of the previous section).

  P (b emin )) ≥ b emin (1 + b -p+1 ) -1 3 b 3emin (1 + b -p+1 ) 3 .

One could argue that the value of the function at zero could be nonzero yet close to the underflow threshold: we remind here that we are not giving "general" rules, we are just dealing with the most common functions.

Maple program

worstcases := proc(radix,precision,emin,emax) local DigitsRadix,epsilonmin,powerofradixoverC,e,a,Plast,r,Qlast, Q,P,NewQ,NewP,epsilon, numbermin,expmin,l; epsilonmin := 12345.0 ; DigitsRadix := (emax+precision+20); Digits := ceil(evalf(DigitsRadix*log(radix)/log(10))); printf("Intermediate precision: %a decimal digits\n",Digits); powerofradixoverC := 2*radix^(emin-precision)/Pi; for e from emin-precision+1 to emax-precision+1 do powerofradixoverC := radix*powerofradixoverC; a := floor(powerofradixoverC); Plast := a; r := 1/(powerofradixoverC-a); a := floor(r); Qlast := 1; Q := a; P := Plast*a+1; while Q < radix^precision-1 do r := simplify(1/(r-a)); a := floor(evalf(r)); NewQ := Q*a+Qlast; NewP := P*a+Plast; Qlast := Q; Plast := P; Q := NewQ; P := NewP od; epsilon := evalf((Pi/2)*abs(Plast-Qlast*powerofradixoverC)); if (e+precision-1) mod 50 = 0 then printf("I am processing exponents %a to %a \n",e+precision-1,min(e+precision+48,emax)) fi; if epsilon < epsilonmin then epsilonmin := epsilon; numbermin := Qlast; expmin := e fi od; printf("The FP number closest to a multiple of Pi/2 is %a * %a ^%a\n",numbermin, radix, expmin); printf("Its distance to a multiple of Pi/2 is %a\n",evalf(epsilonmin,15)); l := evalf(log(epsilonmin)/log(radix),10); printf("which is %a ^%a\n",radix,l) end;

2 When the input argument is near zero First, with the usual functions if the value of the function at zero is a nonzero representable number, there is no problem 1 . So we have to deal with two cases.