domain: info math

text:
Anupam Das
email: anupam.das@inria.fr

On the Pigeonhole and Related Principles in Deep Inference and Monotone Systems

We construct quasipolynomial-size proofs of the propositional pigeonhole principle in the deep inference system KS, addressing an open problem raised in previous works and matching the best known upper bound for the more general class of monotone proofs.

We make significant use of monotone formulae computing boolean threshold functions, an idea previously considered in works of Atserias et al. The main construction, monotone proofs witnessing the symmetry of such functions, involves an implementation of merge-sort in the design of proofs in order to tame the structural behaviour of atoms, and so the complexity of normalization. Proof transformations from previous work on atomic flows are then employed to yield appropriate KS proofs.

As further results we show that our constructions can be applied to provide quasipolynomial-size KS proofs of the parity principle and the generalized pigeonhole principle. These bounds are inherited for the class of monotone proofs, and we are further able to construct n O(log log n) -size monotone proofs of the weak pigeonhole principle with (1 + ε)n pigeons and n holes for ε = 1/ log k n, thereby also improving the best known bounds for monotone proofs.

Introduction

The pigeonhole principle states that if m pigeons are sitting in n holes, and m > n, then two pigeons must be in the same hole. It can be expressed in propositional logic as follows,

PHP m n : m i=1 n j=1 pij → n j=1 m-1 i=1 m i ′ =i+1 pij ∧ p i ′ j
where pij should be interpreted as "pigeon i sits in hole j". 1 This encoding forms a class of propositional tautologies, for m > n, that has become a benchmark in proof complexity [START_REF] Razborov | Proof complexity of pigeonhole principles[END_REF]. For the case of m = n + 1 many propositional proof systems, such as the cut-free sequent calculus, Resolution and bounded-depth Frege, only have proofs of size exponential in n [21] [START_REF] Pitassi | Exponential lower bounds for the pigeonhole principle[END_REF], whereas small proofs (of size polynomial in n) have been constructed for Frege systems, and so also sequent calculi with cut [START_REF] Buss | Polynomial size proofs of the propositional pigeonhole principle[END_REF]. This paper presents a novel proof structure for PHP m n , inspired by previous works of Atserias et al. [START_REF] Atserias | Monotone proofs of the pigeon hole principle[END_REF] [START_REF] Atserias | Monotone simulations of nonmonotone proofs[END_REF], implemented in a representation of monotone proofs2 as rewriting derivations [START_REF] Jeřábek | Proof complexity of the cut-free calculus of structures[END_REF]. Consequently, we obtain quasipolynomial 3 -size proofs of PHP n+1 n in the minimal deep inference system for propositional logic, KS. This answers questions previously raised in [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] [25] [START_REF] Das | Complexity of deep inference via atomic flows[END_REF] on the complexity of KS proofs of PHP m n by matching the best known bound for the more general class of monotone proofs [START_REF] Atserias | Monotone proofs of the pigeon hole principle[END_REF].

By making certain generalizations we are able to apply our methods to obtain quasipolynomial-size KS proofs of the parity principle and the generalized pigeonhole principle, bounds that are inherited by the class of monotone proofs. Finally we show that our proof structure can be applied to yield n O(log log n) -size monotone proofs of PHP (1+ε)n n where ε = 1/ = 1/ log k n for k > 1, significantly improving the best known bound of n O(log n) inherited from proofs of PHP n+1 n in [START_REF] Atserias | Monotone proofs of the pigeon hole principle[END_REF]. 4 We point out that this is the first example where considerations in the complexity of deep inference have yielded improved results for more mainstream systems in proof complexity.

Deep inference systems for classical propositional logic were introduced by Guglielmi et al. [START_REF] Guglielmi | A system of interaction and structure[END_REF] [START_REF] Brünnler | A local system for classical logic[END_REF] and, despite significant progress in recent years on the complexity of deep inference, the classification of the system KS remains open.

In [START_REF] Bruscoli | On the proof complexity of deep inference[END_REF] it was shown that KS polynomially simulates (tree-like) cut-free sequent calculi but not vice-versa. This result was strengthened in [START_REF] Das | Complexity of deep inference via atomic flows[END_REF] where it was shown that KS polynomially simulates certain fragments of Resolution and dag-like cut-free sequent calculi, and it was also shown that these systems, as well as boundeddepth Frege systems, cannot polynomially simulate KS. This work made significant use of proof transformations induced by certain graph rewriting techniques from [START_REF] Guglielmi | Normalisation control in deep inference via atomic flows[END_REF]. In this way the complexity of normalizing a monotone proof to a KS proof was reduced to counting the number of paths in the associated atomic flow, the graph obtained by tracing the journey of each atom through the proof.

It was asked in [START_REF] Straßburger | Extension without cut[END_REF] and [START_REF] Bruscoli | On the proof complexity of deep inference[END_REF] whether polynomial-size proofs of PHP m n exist in KS, and in [START_REF] Straßburger | Extension without cut[END_REF] it was conjectured that no polynomial-size proofs exist. On the other hand, in [START_REF] Jeřábek | Proof complexity of the cut-free calculus of structures[END_REF] Jeřábek gives proofs in an extended system of weaker variants of the pi-geonhole principle, where the mapping from pigeons to holes is required to be functional or onto, which normalize to KS proofs of polynomial size [START_REF] Das | Complexity of deep inference via atomic flows[END_REF]. He uses an elegant black-box construction relying on the existence of the aforementioned Frege proofs, although he notes that this method does not seem to generalize to PHP m n . In this work we rely heavily on a propositional encoding of threshold functions, yielding formulae that count how many of their arguments are true, and our construction is inspired by the monotone proofs of PHP m n given by Atserias et al. [START_REF] Atserias | Monotone proofs of the pigeon hole principle[END_REF]. They use the same threshold formulae as us but our main construction, short proofs that permute the arguments of a threshold formula, is considerably more involved than the analogous construction in their paper due to technicalities of the weaker system KS. The tradeoff is that this more sophisticated proof structure enables us to later achieve the aforementioned improvement in upper bounds on the size of monotone proofs for the weak pigeonhole principle.

In [START_REF] Atserias | Monotone proofs of the pigeon hole principle[END_REF] simple proofs are provided for each transposition, whence the result follows since each permutation can be expressed as a product of at most polynomially many transpositions, resulting in monotone proofs whose atomic flows have polynomial length. However due to this length bound such proofs normalize to exponential-size KS proofs under the aforementioned transformations. Instead we notice in Sect. 3 that the specific permutation required, corresponding to the transposition of a matrix, has a particularly simple decomposition into logarithmically many interleavings, which we implement as monotone proofs whose atomic flows have polylogarithmic length and hence normalize to KS proofs in quasipolynomial time.

In Sect. 4 we generalize this construction by noticing that any permutation can be decomposed into a product of logarithmically many riffle shuffles; this is equivalent to the action of applying merge-sort to the inverse of a permutation. In Sect. 5, we show that these techniques can be applied to yield the aforementioned proofs of the parity principle, generalized pigeonhole principle and the weak pigeonhole principle. In the final result the polylogarithmic length of the atomic flows of our proof structure is crucial since it allows us to use smaller monotone formulae that only approximate threshold functions, and to maintain a sufficiently accurate approximation throughout the various permutations of their arguments.

Preliminaries

Deep inference systems for classical logic were introduced in [START_REF] Brünnler | A local system for classical logic[END_REF] and studied in detail in [START_REF] Brünnler | Deep Inference and Symmetry in Classical Proofs[END_REF] and [START_REF] Bruscoli | On the proof complexity of deep inference[END_REF]. The representation of proofs we use here was introduced in [START_REF] Guglielmi | A proof calculus which reduces syntactic bureaucracy[END_REF].

Propositional Logic

Propositional formulae are constructed freely from atoms (propositional variables and their duals), also known as literals, over the basis {⊤, ⊥, ∧, ∨}, with their usual interpretations. The variables a, b, c, d range over atoms, with ā, b, . . . denoting their duals, and A, B, C, D range over formulae. There is no object-level symbol for negation; instead we may write Ā to denote the De Morgan dual of A, obtained by the following rules:

⊥ = ⊤, ⊤ = ⊥, ā = a, A ∨ B = Ā∧ B, A ∧ B = Ā∨ B
For convenience, we consider formulae equivalent under the smallest equivalence relation generated by the equations below.

[A ∨ B] ∨ C = A ∨ [B ∨ C] (A ∧ B) ∧ C = A ∧ (B ∧ C) A ∨ B = B ∨ A A ∧ B = B ∧ A A ∨ ⊥ = A A ∧ ⊤ = A ⊤ ∨ ⊤ = ⊤ ⊥ ∧ ⊥ = ⊥ If A = B, ⋆ ∈ {∧, ∨}, then C ⋆ A = C ⋆ B
For this reason we generally omit internal brackets of a formula, under associativity, as well as external brackets. For clarity we also use square brackets [, ] for disjunctions and round ones (, ) for conjunctions.

Remark 1 (Equality). Equality of formulae =, as defined above, is usually implemented as an inference rule in deep inference. It is decidable in polynomial time [START_REF] Bruscoli | On the proof complexity of deep inference[END_REF], and whether it is implemented as an inference rule or equivalence relation is purely a matter of convention. Nonetheless we sometimes use it as a 'fake' inference rule, to aid the reader.

It will sometimes be convenient to represent the arguments of a boolean function as a vector or matrix of atoms. However the order in which the atoms are to be read is sensitive, and so we introduce the following notation.

Notation 2 (Vectors and Matrices of Variables). We use bold lowercase letters a, b, . . . to denote (row-)vectors of atoms and bold uppercase letters A, B, . . . to denote matrices of atoms. Vectors are read in their natural order, and we associate a matrix with the vector obtained by reading it rows-first. In this way the transpose of a matrix is equivalent to the vector obtained by reading it columnsfirst.

The notation (a, b) denotes the horizontal concatenation of vectors a and b, and compound matrices are similarly written in the usual way. The notation (ai) n i=1 denotes the vector (a1, . . . , an).

Definition 3 (Rules and Systems

). An inference rule is a binary relation on formulae decidable in polynomial time, and a system is a set of rules. We define the deep inference system SKS as the set of all inference rules in Fig. 1, and also the subsystem KS = {ai↓, aw↓, ac↓, s, m}. Note in particular the distinction between variables for atoms and formulae.

Remark 4. It is worth pointing out that the formulation of deep inference with units is very convenient for proof-theoretic manipulation of derivations, and we exploit this throughout. However we could equally formulate our systems without units with no significant change in complexity; this approach is taken in [START_REF] Straßburger | Extension without cut[END_REF] and the equivalence of these two formulations is shown in [START_REF] Das | On the proof complexity of cut-free bounded deep inference[END_REF].

Definition 5 (Proofs and Derivations). We define derivations, and premiss and conclusion functions, pr, cn resp., inductively:

1. Each formula A is a derivation with premiss and conclusion A.

2. If Φ, Ψ are derivations and ⋆ ∈ {∧, ∨} then Φ⋆Ψ is a derivation with premiss pr(Φ) ⋆ pr(Ψ) and conclusion cn(Φ) ⋆ cn(Ψ).

3. If Φ, Ψ are derivations and cn(Φ)

ρ ------- pr(Ψ) is an instance of a rule ρ then Φ ρ --
Ψ is a derivation with premiss pr(Φ) and conclusion cn(Ψ).

If pr(Φ) = ⊤ then we call Φ a proof. If Φ is a derivation where all inference steps are instances of rules in a system S with premiss A, conclusion B, we write

A Φ S B
. Furthermore, if A = ⊤, i.e. Φ is a proof in a system S, we write

- Φ S B .
We extend our structural rules beyond atoms, to general formulae, below.

Proposition 6 (Generic Rules). Each rule below has polynomialsize derivations in the system containing s, m, and its respective Extended version of paper from CSL-LICS 2014.

2 2014/5/17

Atomic structural rules

Logical rules

⊤ ai↓ ----- a ∨ ā ⊥ aw↓ -- a a ∨ a ac↓ ----- a A ∧ [B ∨ C] s -------------- (A ∧ B) ∨ C identity weakening contraction switch a ∧ ā ai↑ ----- ⊥ a aw↑ -- ⊤ a ac↑ ----- a ∧ a (A ∧ B) ∨ (C ∧ D) m ---------------------- [A ∨ C] ∧ [B ∨ D] cut coweakening cocontraction medial Figure 1.
Rules of the deep inference system SKS.

atomic structural rule. ⊤ i↓ ------- A ∨ Ā ⊥ w↓ -- A A ∨ A c↓ ------- A A ∧ Ā i↑ ------- ⊥ A w↑ -- ⊤ A c↑ ------- A ∧ A
Proof Sketch. See [START_REF] Brünnler | A local system for classical logic[END_REF] for full proofs. We just consider the case for contraction, since that is the only structural rule Gentzen calculi cannot reduce to atomic form [START_REF] Brünnler | Two restrictions on contraction[END_REF]. The proof is by induction on the depth of the conclusion of a c↓-step.

[A ∨ B] ∨ [A ∨ B] c↓ -------------------- A ∨ B → [A ∨ B] ∨ [A ∨ B] = ----------------------- A ∨ A c↓ ------- A ∨ B ∨ B c↓ ------- B (A ∧ B) ∨ (A ∧ B) c↓ ---------------------- A ∧ B → (A ∧ B) ∨ (A ∧ B) m ----------------------- A ∨ A c↓ ------- A ∧ B ∨ B c↓ -------

B

Note that the case for c↑ is dual to this: one can just flip the derivations upside down and replace every formula with its De Morgan dual. c↓-steps become c↑-steps and s and m steps remain valid.

We often use these 'generic' rules in proof constructions, which should be understood as abbreviations for the derivations mentioned above.

Definition 7 (Complexity). The size of a derivation Φ, denoted |Φ|, is the number of atom occurrences in it. For a vector a or matrix A, let |a|, |A| denote its number of elements, respectively.

We will generally omit complexity arguments when they are routine, for convenience. However we outline the main techniques used to control complexity in the following sections.

Monotone and Normal Derivations

We define monotone and normal derivations and relate them to proof systems in deep inference. We point out that the notion of monotone derivation given here is polynomially equivalent to the tree-like monotone sequent calculus [START_REF] Jeřábek | Proof complexity of the cut-free calculus of structures[END_REF], and so is consistent with the usual terminology from the point of view of proof complexity.

C

The significance of normal derivations is that they can be efficiently transformed into KS-proofs of the implication they derive, as demonstrated in the following proposition.

⊤ i↓ --------- B Φ Ā ∨ B Ψ C .
We emphasize that it is the existence of an 'intermediate' formula in normal derivations, e.g. B in the proof above, that allows us to isolate all the ↑ steps and flip them into ↓ steps, resulting in a KS proof. If we started with an arbitrary monotone derivation there may be no such formula, and so any choice of an intermediate formula would also flip some ↓ steps into ↑ steps.

Atomic Flows and Normalization

We are particularly interested in those monotone derivations that can be efficiently transformed to normal ones. A thorough analysis of the complexity of such transformations is carried out in [START_REF] Das | Complexity of deep inference via atomic flows[END_REF] in the setting of graph rewriting. We state informally the main concepts and results here.

Atomic flows and various rewriting systems on them were introduced formally in [START_REF] Guglielmi | Normalisation control in deep inference via atomic flows[END_REF].

Definition 10 (Atomic Flows and Dimensions). The atomic flow, or simply flow, of a monotone derivation is the vertically directed graph obtained by tracing the paths of each atom through the derivation, designating the creation, destruction and duplication of atom occurrences by the following nodes:

⊥ aw↓ -- a → a ∨ a ac↓ ----- a → a aw↑ -- ⊤ → a ac↑ ----- a ∧ a → Extended version of paper from CSL-LICS 2014. 3 2014/5/17 → , → , → → , → , → Figure 2.
Graph rewriting rules for atomic flows.

We do not have nodes for s and m steps since they do not create, destroy or duplicate any atom occurrences, and we generally consider flows equivalent up to continuous deformation preserving the vertical order of edges.

The size of a flow is its number of edges. The length of a flow is the maximum number of times the node type changes in a (vertically directed) path. The width of a flow is the maximum number of input or output edges in a subgraph of a connected component.

For intuition, the width of a flow can be thought of as a measure of how much a configuration of ac↑ nodes increases the number of edges in a connected component before a configuration of ac↓ nodes decreases it.

Example 11. We give an example of a monotone derivation and its flow below:

a ac↑ ----- a ∧ a ∨ ⊥ aw↑ -- a ac↑ ----- a ∧ a m -------------------------- a ∨ a ac↓ ----- a = ----------- a ∨ ⊥ aw↓ -- b ∧ a ∨ a ac↓ ----- a s -------------------------- a ac↑ ----- a ∧ a ∨ b aw↑ -- ⊤ ∧ a = ----------- a
The flow has length 3, measured from the top-right aw↓ node to the bottom-left ac↑ node, and width 4, measured either as the outputs of the two top ac↑ nodes or the inputs of the two bottom ac↓ nodes.

Observation 12. A normal derivation has flow length 1.

Theorem 13 (Normalization). A monotone derivation Φ whose flow has width w and length l can be transformed into a normal derivation of size |Φ|•w l+O (1) , preserving premiss and conclusion.

While the proof of the above theorem can be found in [START_REF] Das | Complexity of deep inference via atomic flows[END_REF], we outline the main ideas to give the reader an intuition of the argument.

Proof Sketch. The graph rewriting rules in Fig. 2 induce transformations on monotone derivations by consideration of the corresponding rule permutations; note that, due to atomicity of the structural rules, permutations with logical steps are trivial. The system is terminating and the flows of normal derivations are all normal forms of this system. Each rewrite step preserves the number of maximal paths between pending edges, and a normal derivation has size polynomial in this measure.

Consequently the complexity of normalizing a monotone derivation is polynomial in its size and the number of maximal paths in its flow, and this is estimated by the given bound.

Notice, in particular, that any rewrite derivation on atomic flows acts independently on different connected components. Therefore the complexity of normalization is determined by the structural behaviour of individual atoms -there is no interaction between distinct atoms during normalization.

Finally, most of the proofs in this work are inductions, and for the base cases it will typically suffice to build any monotone proof of a single formula or simple class of formulae, since we are interested in how the size (or width, length) of the proofs grow and not their initial values. For this reason, the following result will be useful, and we implicitly assume it when omitting base cases of inductions. . Clearly each conjunction of A ′ logically implies each disjunction of B ′ and so there must be derivations in {aw↓, aw↑} witnessing this fact. Using these derivations and applying c↓, c↑ appropriately we can construct a monotone derivation

Proposition 14 (Monotone Implicational Completeness). Let A, B be negation-free formulae such that

A ′ B ′
, whence the result follows by sequential composition of these derivations.

By appealing to Thm. 13 we then obtain the following result.

Corollary 15. Normal derivations are monotone implicationally complete.

Short Proofs of the Pigeonhole Principle

Throughout this section the variables m and n are powers of 2 and m ≤ n. All proofs in this section are monotone unless otherwise mentioned.

Threshold Formulae and Permutations

Threshold functions are a class of boolean functions

TH n k : {0, 1} n → {0, 1} by TH n k (σ1 • • • σn) = 1 just if n i=1 σi ≥ k.
In this section we define quasipolynomial-size monotone formulae computing such functions and construct derivations whose Definition 16 (Threshold Formulae). We define the formulae,

th 1 k (a) :=      ⊤ k = 0 a k = 1 ⊥ k > 1 th 2n k (a, b) := i+j=k th n i (a) ∧ th n j (b)
for vectors a, b of length n. Definition 19 (Distributivity). We define distributivity rules as abbreviations for the following derivations: Proof. We use the following identity:

dist ↑ : A c↑ ------- A ∧ A ∧ [B ∨ C] 2•s --------------------- (A ∧ B) ∨ (A ∧ C) dist ↓ : (A ∧ B) ∨ (A ∧ C) m --------------------- A ∨ A c↓ ------- A ∧ [B ∨ C]
(a, b) m (c, d) = (a m c, b m d)
We give an inductive step from n to 2n in Fig. 3 where derivations marked IH are obtained by the inductive hypothesis.

The dist ↑ steps duplicate each atom at most r times and so, analyzing the associated flow, each inductive step adds O(r) configurations of ac↑ and ac↓ nodes of width O(r) on top of O(r) copies of the inductive hypothesis in parallel. The induction terminates in log n m steps, whence the bound on length is obtained.

Observation 21. For matrices B and C of equal dimensions we have:

5 A B C D ⊺ = A ⊺ C ⊺ B ⊺ D ⊺
Recall that a matrix of atoms is equivalent to the vector obtained from a rows-first reading of it.

Theorem 22 (Transposition).

There are monotone derivations,

th n k (X)
th n k (X ⊺ ) 5 Of course, in any such situation, A and D will also have equal dimensions.

whose flows have length O(log 2 n) and width O(n).

Proof. Let A, B, C, D be the four quadrants of X. We give an inductive step from n to 2n,

th 2n k A B C D ---------------------------------------------- i+j=k      th n i A B IH th n i A ⊺ B ⊺ ∧ th n j C D IH th n j C ⊺ D ⊺      ---------------------------------------------- th 2n k A ⊺ B ⊺ , C ⊺ D ⊺ interleave th 2n k A ⊺ C ⊺ B ⊺ D ⊺ interleave IH • • • IH
where the derivations marked IH are obtained by the inductive hypothesis and Obs. 21, and the derivation marked 'interleave' is obtained by applying Lemma 20 to interleave the rows of the two matrices.

Analyzing the associated flow, each inductive step adds an interleaving below O(k) copies of the inductive hypothesis in parallel, thereby adding O(log n) to the length and maintaining a width of O(n), by Lemma 20. The induction terminates in O(log n) steps, whence the upper bound on length is obtained.

From Threshold Formulae to the Pigeonhole Principle

The previous section showed that there are 'short' derivations transposing a matrix of arguments of a threshold formula. We show here how such derivations are used to obtain quasipolynomial-size proofs of the pigeonhole principle.

In this section almost all derivations are normal, so we omit their flows and complexity analysis.

Definition 23 (Pigeonhole Principle). We define the following:

LPHPn := n i=1 n-1 j=1 pij RPHPn := n-1 j=1 n i=1 n i ′ =i+1 (p i ′ j ∧ pij)
PHPn := LPHPn → RPHPn Definition 24. Let ⊥ ⊥ ⊥mn be the (m × n) matrix with the constant ⊥ at every entry. Define P n = (pij) ⊥ ⊥ ⊥n1 , with i, j ranging as in Dfn. 23. I.e. P n is obtained by extending (pij) with an extra column of ⊥-entries, so that it is a square matrix.

Our aim in this section is to prove the following theorem, from which we can extract proofs of PHPn in KS by the results in earlier sections.

Theorem 25. There are normal derivations, LPHPn

th n 2 n (P n) , th n 2 n (P ⊺ n ) RPHPn of size n O(log n) .
Before we can give a proof, we need some intermediate results. It should be pointed out that similar results were provided in [START_REF] Atserias | Monotone proofs of the pigeon hole principle[END_REF] for the monotone sequent calculus, which could be translated to deep inference by [START_REF] Brünnler | An algorithmic interpretation of a deep inference system[END_REF] [18], but we include them for completeness. Indeed, similar results appeared in [START_REF] Bruscoli | A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae[END_REF]. These intermediate results are fairly routine, and there is nothing intricate from the point of view of complexity.

Extended version of paper from CSL-LICS 2014.

5 2014/5/17 th 4n r (a, b, c, d) = ------------------------------------------------------------------------- s+t=r          th 2n s (a, b) = -------------------------- i+j=s th n i (a) ∧ th n j (b) ∧ th 2n t (c, d) = -------------------------- k+l=t th n k (c) ∧ th n l (d) dist↑ i+j=s k+l=t th n i (a) ∧ th n j (b) ∧ (th n k (c) ∧ th n l (d))          = ------------------------------------------------------------------------- s+t=r            i+k=s j+l=t (th n i (a) ∧ th n k (c)) ∧ (th n j (b) ∧ th n l (d)) dist↓ th 2n s (a, c) IH th 2n s (a m c) ∧ th 2n t (b, d) IH th 2n t (b m d)            = ---------------------------------------------------------------- th 4n r ((a, b) m (c, d)) • • • O(r) • • • • • • • • • O(r) • • • IH IH Figure 3.
Interleaving the arguments of a threshold formula.

Proposition 26. For l ≥ k there are normal derivations,

th n l (a) th n k (a) of size n O(log n) .
Proof. We give an inductive step from n to 2n,

th 2n l (a, b) = ------------------------------- i+j=l    th n i (a) IH th n i ′ (a) ∧ th n j (b) IH th n j ′ (b)    {w↓,c↓}
th 2n k (a, b) where i ′ and j ′ are chosen such that i ′ ≤ i, j ′ ≤ j and i ′ + j ′ = k, and derivations marked IH are obtained by the inductive hypothesis.

Lemma 27 (Evaluation). There are normal derivations,

th 2n r+s (a, b) th n r+1 (a) ∨ th n s (b) of size n O(log n) .
Proof. Notice that if i + j = r + s then i > r or j ≥ s. We give a construction in Fig. 4, where Φ and Ψ denote derivations obtained by Prop. 26.

Lemma 28. For vectors a 1 , . . . , a m of atoms there are normal derivations,

m r=1 th n k (a r ) th mn k (a r ) n r=1 , m r=1 th n k (a r ) th mn mk (a r ) n r=1 of size n O(log n) .
Proof. By induction on m. Simply apply = and w↓ to fill out the formula.

We are now in a position to prove Thm. 25.

Proof Sketch of Thm. [START_REF] Straßburger | Extension without cut[END_REF]. Repeatedly apply Lemma 27 to th n 2 n (P ⊺ n ), always setting r = s or r = s + 1, until a disjunction of threshold formulae with n arguments each is obtained. By the ordering of the atoms in P ⊺ n these threshold formulae will have as arguments (pij) n i=1 for some j, or all ⊥; in the latter case any such formula is equivalent to ⊥, since the threshold will be at least 1.

In the former case, by the choice of r and s at each stage, we have that the threshold of each of these formulae is at least 2. From here Prop. 26 can be applied so that all thresholds are 2, whence RPHPn can be easily derived.

For the other direction, construe each variable pij as a threshold formula th 1 1 (pij) and apply Lemma 28 to obtain a derivation from LPHPn to th n 2 n (P ). In both cases normality is established by the normalization procedure of Thm. 13. We have chained together finitely many normal derivations so the length of the associated flows is bounded by a constant, whence the upper bound on size is obtained.

= ---------------------------- i+j=r+s th n i (a) ∧ th n j (b) = -------------------------------------------------------------------------------------------- i>r j=r+s-i         th n i (a) ∧ th n j (b) w↑ ------- ⊤ = ---------------------- th n i (a) Φ th n r+1 (a)         s•c↓ ---------------------------------------- th n r+1 (a) ∨ j≥s i=r+s-j         th n i (a) w↑ -------- ⊤ ∧ th n j (b) = ---------------------- th n j (b) Ψ th n s (b)         r•c↓ ---------------------------------------- th n s (b)

3.3

The Case when n is not a Power of 2

Though we have assumed that n is a power of 2 throughout this section, the proof is actually sufficient for all n, as pointed out in [START_REF] Atserias | Monotone proofs of the pigeon hole principle[END_REF].

Definition 31. For r ≤ s given, define LPHPs(r) by substituting ⊥ for every atom pij where i > r or j ≥ r. Define RPHPs(r) analogously.

Observation 32. For all r ≤ s we have that LPHPs(r) = LPHPr and RPHPs(r) = RPHPr. 6 Consequently a proof of PHPr is just a proof of PHPn, where n is the power of 2 such that r ≤ n < 2r.

Arbitrary Permutations

Interleavings by themselves do not form a generating set for the symmetric group, and so cannot be used to generate derivations for arbitrary permutations of arguments of threshold formulae. However a generalization of them, corresponding to the set of riffle shuffles on a deck of cards, do form such a set. In this section we show how they may be used to generate arbitrary permutations on the arguments of threshold formulae. The proofs in this section are similar to those in Sect. 3, and so we omit them for brevity, instead providing the general proof structure as intermediate results.

Recall that our original definition of threshold formulae used a symmetric divide-and-conquer strategy, generated from a complete binary tree in the natural way. In this section it will be useful to have a more general definition of threshold formulae, based on any tree decomposition of the divide-and-conquer strategy.

Throughout this section we assume all trees are binary.

Definition 33. For a tree T , let d(T ) denote its depth, l(T ) its number of leaves and |T | denote its number of nodes. For a binary tree T , let T0 denote its left subtree (from the root) and T1 its right. Thus any string σ ∈ {0, 1} k determines a unique subtree Tσ of T , for k ≤ d(T ).

Definition 34 (General Threshold Formulae). For a binary tree T and vectors a, b with |a| = l(T0), |b| = l(T1), define

th T k (a, b) = i+j=k th T 0 i (a) ∧ th T 1 j (b)
with the base case the same as in Dfn. 16.

The following proposition gives an estimate of the size of these threshold formulae.

Proposition 35. For a binary tree T , |th T k (a)| = l(T ) O(d(T )) . 6 Recall that formulae are equivalent up to =.

Proof. In the worst case, every level of the binary tree is full, whence the bound is obtained by Obs. 17.

What we define as a shuffle below corresponds to the common riffle method of shuffling a deck of cards: cut the deck anywhere, partitioning it into a left and right part, and then interleave these in any way, maintaining the relative order of cards in either partition. Under this analogy each card of the deck will correspond to a leaf of the tree determining a threshold formula.

Definition 36 (Cuts and Shuffles). A cut of a vector (a1, . . . , an) is a pair {(a1, . . . , am), (am+1, . . . , an)}. A riffle shuffle, or simply shuffle, of length n is a string σ ∈ {0, 1} n .

For a vector a and shuffle σ of length n = |a| we write σ(a) to denote the following action of σ on a: let Σi denote the number of 1s in σ1 • • • σi, so that i -Σi is the number of 0s in σ1 • • • σi and k = Σn is the number of 1s in σ; we give a componentwise definition of σ(a):

(σ(a))i = ai-Σ i σi = 0 a n-k+Σ i σi = 1
In the above definition, one should think of σ determining a cut {(a1, . . . , a n-k ), (a n-k+1 , . . . , an), and where each bit indicates which side of the cut the next element of σ(a) comes from.

Lemma 37 (Cutting). For any tree T and cut {a, b} there are trees S0, S1 with d(S0), d(S1) ≤ d(T ) such that there are monotone derivations,

th T k (a, b) i+j=k th S 0 i (a) ∧ th S 1 j (b)
whose flows have length O(d(T )) and width O(l(T )).

Proof of Lemma 37. By induction on l(T ). Without loss of generality, suppose b is contained entirely in T1 (otherwise, a is contained entirely in T0 and the argument is symmetric). We construct the

th T r (a, b) = -------------------------------------------------------------- s+t=r                  th T 0 s a 1 ∧ th T 1 t (a 2 , b) IH i+j=t th S ′ 0 i a 2 ∧ th S 1 j (b)      dist↑ i+j=t th T 0 s a 1 ∧ th S ′ 0 i a 2 ∧ th S 1 j (b)             = ------------------------------------------------------------------- s ′ +t ′ =r          k+l=s ′ th T 0 k a 1 ∧ th S ′ 0 l a 2 ∧ th S 1 t ′ (b) dist↓   k+l=s ′ th T 0 k a 1 ∧ th S ′ 0 l a 2 = ---------------------------------- th S 0 s ′ (a) ∧ th S 1 t ′ (b)           
where the derivation marked IH is obtained by the inductive hypothesis.

Lemma 38 (Shuffling). Let S be a tree and σ a shuffle of length l(S). There is a tree T with d(T ) = O(d(S)) and monotone derivations,

th S k (v) th T k (σ(v)) whose flows have length O(d(S) 2 )

and width O(l(S)).

Proof of Lemma 38. By induction on l(S), we give the inductive step in Fig. 5. In the construction we set v = (w, x), defined by l(S0) and l(S1), and σ(v) = (y, z). The argument is analogous to the one in Lemma 3, with derivations marked 'cut' obtained from Lemma 37 and derivations marked IH obtained from the inductive hypothesis.

In particular the cuts are chosen 7 such that |b 2 | = |c 1 | and so that there are shuffles σ1, σ2 with

σ(v) = (σ1(a, b 1 , c 1 ), σ2(b 2 , c 2 , d))
Theorem 39 (Merge Sort). For any tree S and permutation π on {1, . . . , l(S)} there is a tree T with d(T ) = O(d(S)) and monotone derivations,

th S k (aiπ) n i=1 th T k (ai) n i=1
whose flows have length O(d(S) 3 ) and width O(l(S)).

Proof of Thm. 39. By induction on l(S) = l(T ). We construct the following derivation, -----------------------------------------------

th S r (aiπ) n i=1 -
- s+t=r     th S 0 s (aiπ) m i=1 IH th T ′ 0 s (a 1 ) ∧ th S 1 t (aiπ) n i=m+1 IH th T ′ 1 t (a 2 )     shuffle th T r (ai) n i=1
7 Such a choice exists (and is unique) by the discrete intermediate value theorem.

where the derivations marked IH are obtained from the inductive hypothesis, sorting the inputs of the left and right subtrees of S to vectors a 1 and a 2 resp., and the derivation marked 'shuffle', obtained from Lemma 38, carries out the unique shuffle on (a 1 , a 2 ) resulting in a completely sorted vector.

Proposition 40 (Repartitionings). For trees S, T with the same number of leaves there are monotone derivations,

th S k (a)
th T k (a) whose flows have length O(d(S) 2 ) and width O(l(S)).

Proof of Prop. 40. By induction on l(S) = l(T ). Let {b, c} be the cut of a such that |b| = l(T0) and |c| = l(T1). We construct the following derivation, ,c) where the derivation marked 'cut' is obtained from Lemma 37 and the derivations marked IH are obtained from the inductive hypothesis.

th S k (a) cut i+j=k     th R 0 i (b) IH th T 0 i (b) ∧ th R 1 j (c) IH th T 1 j (c)     = --------------------------------- th T k (b
Corollary 41. For any tree T and permutation π on {1, . . . , l(T )} there are normal derivations,

th T k (ai) n i=1 th T k (aiπ) n i=1 of size l(T ) O(d(T ) 3 ) .
Proof. By Thm. 39, Prop. 40 and Thm. 13.

Further Results and Applications

We give some examples of how the techniques developed in previous sections can be applied to yield further results, namely quasipolynomial-size normal proofs of the Generalized Pigeonhole principle and the Parity principle. Both bounds are also inherited for monotone proofs although, while these have not appeared in the literature, we point out that such monotone proofs could also have been constructed using the permutation arguments of Atserias et al. in [START_REF] Atserias | Monotone proofs of the pigeon hole principle[END_REF]. More interestingly we provide n O(log log n) -size monotone proofs for the weak pigeonhole principle, with (1+ε)n pigeons and n holes for every ε = 1/ log Ω(1) n, improving the previous best known bound of n O(log n) inherited from the proofs of PHP n+1 n given in [START_REF] Atserias | Monotone proofs of the pigeon hole principle[END_REF].

Generalized Pigeonhole Principle

If there are 45 hats that are either red or green, then there must be 23 of the same colour. This exemplifies a generalization of the pigeonhole principle where sufficiently many pigeons may guarantee more than two in some hole [START_REF] Dijkstra | The undeserved status of the pigeon-hole principle[END_REF]. If k + 1 pigeons in some hole are required then nk + 1 pigeons are necessary, so this principle can be encoded as follows: th S r (w, x) --------------------------------------------------------------------------------------th T r (y, z) This formula has size O(n k+1 ), polynomial for fixed k. If, however k is large relative to n, e.g. n/2 or √ n, then one can always express the right hand side using threshold formulae to obtain an encoding of quasipolynomial-size.

= ---------------------------------------------------------------------------------------- s+t=r                   th S 0 (w) cut i+j=s th S ′ 0 i (a, b 1 ) ∧ th R 0 j (b 2 ) ∧ th S 1 (x) cut k+l=t th R 1 k (c 1 ) ∧ th S ′ 1 l (c 2 , d)      dist↑ i+j=s k+l=t th S ′ 0 i a, b 1 ∧ th R 0 j b 2 ∧ th R 1 k c 1 ∧ th S ′ 1 l c 2 , d              = ---------------------------------------------------------------------------------------- s+t=r             i+k=s j+l=t th S ′ 0 i a, b 1 ∧ th R 1 k c 1 ∧ th R 0 j b 2 ∧ th S ′ 1 l c 2 , d dist↓     th T ′ 0 s (a, b 1 , c 1 ) IH th T 0 s (y) ∧ th T ′ 1 t (b 2 , c 2 , d) IH th T 1 t (z)                 = -
It is simple to see that our proofs of PHPn can be generalized to this class of tautologies, by the same arguments as in Sect. 3.

Parity Principle

The parity principle states that one cannot partition an odd-size set into pairs, and is usually encoded by the following tautologies,

PARn : 2n i=0 j =i a {i,j} → j =i>i ′ =j a {i,j} ∧ a {i ′ ,j}
where a {i,j} should be interpreted as "element i is paired with element j".

These tautologies have similar structure to PHPn, but in many proof systems these tautologies are in fact harder to prove. For example, in bounded-depth Frege systems PHPn can be efficiently derived from PARn but not vice-versa [1] [4].

However, in KS, we can construct quasipolynomial-size proofs of PARn using similar methods to those for PHPn, and we give an outline of these constructions in this subsection.

We omit proofs corresponding to basic properties of threshold functions, since they are fairly routine inductions of which Sect. 3 has given many examples, and also often do not specify precise orderings of variables or tree-structures of a threshold formulae, since these can all be reduced to any other in quasipolynomial time, by the results of Sect. 4.

Let LPARn and RPARn denote the left and right hand sides of PARn respectively. By a similar argument to Prop. 25 we obtain normal derivations of the following form,

LPARn th 2n(2n+1) 2n+1 (a 2 )
where a 2 is an appropriate sequence of the variables a {i,j} in which each variable occurs exactly twice, as in LPARn.

Let (a, a) be a permutation of a 2 so that each variable occurs exactly once in a. Now we can construct the following derivation, -------------------------------

- th n(2n+1) n+1 (a)
where the derivation marked 'permute' applies the results of Sect. 4, namely Cor. 41, to permute the arguments of a threshold formula, and the derivation marked 'evaluate' is obtained by Lemma 27, setting r = n and s = n + 1. Now notice that, if n + 1 of the variables a {i,j} are true, i.e. we have n + 1 pairs out of 2n + 1 variables, we must have some j which is paired with two distinct variables, and this can be realized as derivations,

th n(2n+1) n+1 (a)
RPARn in a similar way to Prop. [START_REF] Straßburger | Extension without cut[END_REF].

Chaining all these normal derivations together gives us monotone derivations

LPARn

RPARn of quasipolynomial size and with flows of bounded length, and from here we can construct quasipolynomialsize KS-proofs of PARn in the usual way.

Monotone Proofs of the Weak Pigeonhole Principle

The results of this section provide the first example of considerations in the complexity of deep inference yielding new results for more mainstream systems in proof complexity. Unlike the previous two results our proofs of the weak pigeonhole principle rely crucially on the fact that the proofs permuting threshold arguments we constructed have flows of polylogarithmic length. The basic idea is to begin with formulae approximating threshold functions and

Extended version of paper from CSL-LICS 2014. 9 2014/5/17

bound how much worse the approximation develops as the interleaving and transposition arguments of Sect. 3.1 are applied.

Approximating Threshold Functions

It is not quite correct to call the formulae we define below as ε-approximators of threshold functions, since in fact they output incorrectly on a large proportion of inputs. Rather they output 1 just if the actual threshold is within some predetermined factor of the threshold being measured. The tradeoff is that we are able to define monotone formulae that are much smaller than the usual threshold formulae we have used until now.

Definition 42 (Threshold Approximators). Let |a| = |b| = n. We define the (p, q)-approximator

T n k [p, q] of TH n k as follows, T n k [p, q](a, b) = i+j=p T n ik q [p, q](a) ∧ T n jk q [p, q](b)
where we assume that k is some power of q and n is a power of 2, for example by adding a string of ⊤s and ⊥s of appropriate format to the arguments. 8It is not easy to understand the semantics of these approximators, and in the next section we provide solely proof-theoretic arguments rather than semantic intuition. We do, however, make the following observations, provable by straightforward inductions.

Observation 43. We have the following properties,

1. TH n k ⇒ T n k [p, q] for all p < q. 2. T n k [p, q] ⇒ TH n k(p/q) log n . 3. |T n k [p, q](a)| = O(p log n )
where ⇒ denotes logical implication.

Manipulating Arguments in Threshold Approximators

In this section we return to the derivations proved in Sect. 3.1 on interleaving and transposing arguments of a formula. Since the approximators we now consider do not exactly compute threshold functions, they are no longer symmetric and so similar derivations cannot be constructed. Rather we show that witnessing certain permutations requires a bounded deterioration in the accuracy of the approximation. Ultimately we will choose an initial approximation that is accurate enough to ensure that this deterioration does not become too excessive.

We first state a basic fact allowing us to infer weaker approximations from stronger ones. The proof is straightforward and follows the same kind of induction argument as previous proofs.

Lemma 44. For p ≥ p ′ , k ≥ k ′ there are normal derivations,

T n k [p, q](a) T n k ′ [p ′ , q](a) of size p O(log n) .
The following is the main result that will control the deterioration in approximation throughout our overall argument.

Lemma 45. There are normal derivations,

T n k [p, q](a, b, c, d) T n k [p -1, q](a, c, b, d) of size p O(log n) .
We first need the following result, whose proof is straightforward.

Proposition 46. For x, y ≥ 0, if (x + y) ∈ N then (x + y) -(⌊x⌋ + ⌊y⌋) ≤ 1.

Proof of Lemma 45. We construct appropriate derivations in Fig. 6 where,

s ′ = ⌊ is+kt p ⌋ t ′ = ⌊ js+lt p ⌋ and, i ′ = ⌊ isp is+kt ⌋ j ′ = ⌊ jsp js+lt ⌋ k ′ = ⌊ ktp is+kt ⌋ l ′ = ⌊ ltp js+lt ⌋ so we have s ′ + t ′ , i ′ + j ′ , k ′ + l ′ ≥ p -1 by Prop. 46 and also i ′ s ′ ≤ is, j ′ t ′ ≤ js, k ′ s ′ ≤ kt, l ′ t ′ ≤
lt, so that the derivations marked 'decrease' are obtained by Lemma 44.

The following result has proof similar to that of Lemma 20, using the above lemma in the inductive steps to measure the deterioration of the approximator.

Proposition 47. There are monotone derivations,

T n k [p, q](a, b) T n k [p -log n, q](a b) of size p O(log n) whose flows have length O(log n) and width O(p).
The following result has proof similar to that of Thm. 22.

Theorem 48. There are monotone derivations,

T n k [p, q](X)

T n k [p -log 2 n, q](X ⊺ ) of size p O(log n) whose flows have length O(log 2 n) and width O(p).

From Approximators to the Weak Pigeonhole Principle

Recall the definition of PHP m n , where m denotes an arbitrary number of pigeons greater than the number of holes n, and define LPHP m n and RPHP n m analogously to Dfn. 23. In this section we essentially mimic the results of Sect. 3.2 to complete our proofs of the weak pigeonhole principle.

First we will need the following well known result whose proof follows, for example, by consideration of the inclusion-exclusion principle in the binomial expansion.

Proposition 49. For ε ≤ 1 we have that (1 -ε) k ≥ 1 -εk.
Proof. Let X0, . . . , X k-1 be independent identically distributed Bernoulli random variables with Pr[Xi = 1] = ε and Pr[Xi = 0] = (1 -ε) for each i. Then: The following result has proof similar to that of Thm. 25.

(1 -ε) k = Pr
Extended version of paper from CSL-LICS 2014. 10 2014/5/17 -------------------------------------------------------T 2n sr q [p -1, q](a, c)

T 4n r [p, q](a, b, c, d) = ---------------------------------------------------------------------------------------------------------------------------------- s+t=p                    T 2n sr q [p, q](a, b) = ------------------------------------------- i+j=p T n isr q 2 [p, q] (a) ∧ T n jsr q 2 [p, q] (b) ∧ T 2n tr q [p, q](c, d) = ------------------------------------------- k+l=p T n ktr q 2 [p, q] (c) ∧ T n ltr q 2 [p, q] (d) dist↑ i+j=p k+l=p T n isr q 2 [p, q] (a) ∧ T n jsr q 2 [p, q] (b) ∧ T n ktr q 2 [p, q] (c) ∧ T n ltr q 2 [p, q] (d) = ------------------------------------------------------------------------------------------------------------      T n isr q 2 [p, q](a) decrease T n i ′ s ′ r q 2 [p -1, q](a) ∧ T n ktr q 2 [p, q](c) decrease T n k ′ s ′ r q 2 [p -1, q](c)      ∧      T n jsr q 2 [p, q](b) decrease T n j ′ t ′ r q 2 [p -1, q](b) ∧ T n ltr q 2 [p, q](d) decrease      i+k=p-1 j+l=p-1 T n isr q 2 [p -1, q] (a) ∧ T n ktr q 2 [p -1, q] (c) ∧ T n jsr q 2 [p -1, q] (b) ∧ T n ltr q 2 [p -1, q] (d) dist↓ i+k=p-1 T n isr q 2 [p -1, q] (a) ∧ T n ksr q 2 [p -1, q] (c) = -
∧ i+k=p-1
T n jtr q 2

[p -1, q] (b) ∧ T n ltr q 2

[p -1, q] (d)

= -------------------------------------------------------

T 2n

tr q

[p -1, q](b, d)

          
= ---------------------------------------------------------------------------------------------------------------------------------------T 4n r [p -1, q](a, c, b, d) Proof. For ε = 1/ log d n, choose q = 3 log d+3 n and p = q -1. Since ε > 1 q , there is a trivial derivation from LPHP n

(1-ε)n

to LPHP n

(1-1 q )n in w↓, and by chaining this to the derivations from Lemmata 50 and 48 we obtain monotone derivations from LPHP n

(1-ε)n to T

(1-1 q )n 2 n [p -log 2 n, q](pij) ⊺ .

We now need to check that n > (1-ε)n , for ε = 1/ log Ω(1) n, of size n O(log n log log n) .

Final Comments

We constructed explicit quasipolynomial-size proofs of the pigeonhole principle in KS, and generalized our techniques to further yield quasipolynomial-size proofs of the parity principle and quite strong variants of the weak pigeonhole principle. In particular the existence of n O(log log n) -size monotone proofs of the most common variant, with 2n pigeons and n holes, are implied by our construction. We repeat that this is the first time when considerations in the complexity of deep inference proofs have led to improvements for systems in mainstream proof complexity.

The various proof structures used throughout this work are similar in concept and fairly uniform, and so it might be pertinent to design high-level tools to more easily manipulate deep inference proofs, respecting certain complexity properties. One such approach might be to design an associated theory of bounded artithmetic, as done for other propositional proof systems, e.g. the theory I∆0 for bounded-depth Frege systems [START_REF] Paris | δ 0 sets and induction[END_REF]. Work in this direction is ongoing.

A natural question is whether the methods used here could be generalized to yield a simulation of Frege proofs, as done for KS + in [START_REF] Bruscoli | A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae[END_REF] [START_REF] Jeřábek | Proof complexity of the cut-free calculus of structures[END_REF]. That construction is also relies heavily on threshold formulae, however it is not clear how to restrict the length of flows in the same way as we did here.

Note that the proofs we have given, albeit n O(log 2 n) so quasipolynomial in size, are not in polynomial correspondence with those Extended version of paper from CSL-LICS 2014.

11 2014/5/17

constructed in [START_REF] Atserias | Monotone proofs of the pigeon hole principle[END_REF] for the monotone sequent calculus, and so KS + , which have smaller quasipolynomial size n O(log n) . In fact it is conjectured that there are polynomial-size proofs in KS + , due to the more general conjecture that the monotone sequent calculus polynomially simulates the full sequent calculus over monotone sequents. Consequently we cannot rule out the possibility that proofs of PHPn witness a superpolynomial separation between KS and KS + .

Proposition 9 .

 9 A normal derivation A Φ {aw↑,ac↑,s,m} B Ψ {aw↓,ac↓,s,m} C can be transformed in linear time to a KS-proof of Ā ∨ C. Proof Sketch. Define the derivation B Φ {aw↓,ac↓,s,m} Ā by flipping Φ upside-down, replacing every atom with its dual, ∧ for ∨ and vice-versa. aw↑-steps become aw↓-steps, ac↑-steps become ac↓steps and s and m steps remain valid. Now construct the required derivation:

  A → B is valid. Then there is a monotone derivation A B . Proof Sketch. Construct a disjunctive normal form A ′ of A and conjunctive normal form B ′ of B by distributivity. Note that all distributivity laws are derivable by Dfn. 19 and duality, so there are monotone derivations B ′ B and A A ′

  Extended version of paper from CSL-LICS 2014. 4 2014/5/17 flows have length log O(1) n and width O(n) that conduct certain permutations on the arguments of such formulae.

Observation 17 .

 17 th n k computes the threshold function TH n k , and has size n O(log n) and depth O(log n). Definition 18 (Interleaving). For a = (a1, . . . , an), b = (b1, . . . , bn) let a b denote the interleaving of a with b: (a1, b1, . . . , an, bn). More generally, we denote by a m b the m-interleaving: (a1, . . . , am, b1, . . . bm, • • • , an-m+1, . . . , an, bn-m+1, . . . , bn)

Lemma 20 .

 20 There are monotone derivations, th 2n k (a, b) th 2n k (a m b) whose flows have length O(log n) and width O(n).

Theorem 29 .

 29 There are normal derivations, LPHPn RPHPn of size n O(log 2 n) . Proof. By Thms. 22 and 25 there are monotone derivations with same premiss and conclusion of length O(log 2 n) and width O(n). The result then follows by Thm. 13. Corollary 30. There are KS proofs of PHPn of size n O(log 2 n) . Proof. By Prop. 9. Extended version of paper from CSL-LICS 2014. 6 2014/5/17 th 2n r+s (a, b)

Figure 4 .

 4 Figure 4. Proof of Lemma 27.

  Extended version of paper from CSL-LICS 2014.8 2014/5/17

Figure 5 .

 5 Figure 5. Riffle shuffling the inputs of a threshold formula.

1

 1 -i<k Pr [Xi = 1]by the union bound.≥ 1 -εk

Figure 6 .

 6 Figure 6. Single interleaving step for threshold approximators.

( 1 -≥ 1 - 1 log d n 1 - 2 3 log d n < 1

 111121 ε)n ((p-log 2 n)/q) log n before applying Lemma 50. Now we have that, 2 log n 3 log d+1 n ≥ 1 -2 3 log d n by Prop. 49. Consequently we have that,(1 -ε) ((p -log 2 n)/q) log n ≤ 1 -giving monotone derivations from LPHP n (1-ε)n to RPHP n (1-ε)n by Lemma 50. From previous bounds, the size of these derivations is p O(log n) = (log n) O(log n) = n O(log log n) as required.Since the width of these derivations is O(log n) we also gain a minor improvement in the complexity of KS proofs of PHP n (1-ε)n over those appearing in Sect. 3. Corollary 52. There are KS proofs of PHP n

Notice that the above formula allows the mapping from pigeons to holes to be many-many. Additional restrictions can be placed on the mapping, demanding that it is a function or that it is onto, resulting in a logically weaker formula, but here we consider only the version above.[Copyright notice will appear here once 'preprint' option is removed.]

A monotone proof is a proof in the sequent calculus free of negation-steps.

A quasipolynomial in n is a function of size n log Θ(1) n .

This result also supports the more general conjecture in the community that the class of monotone proofs polynomially simulates Frege systems[START_REF] Atserias | Monotone simulations of nonmonotone proofs[END_REF] [19][START_REF] Jeřábek | Proofs with monotone cuts[END_REF].

This increases the number of arguments by at most multiplication by 2q.


Mourad Choulli
email: mourad.choulli@univ-lorraine.fr

AND Yavar Kian
email: yavar.kian@univ-amu.fr

Eric Soccorsi
email: eric.soccorsi@univ-amu.fr

DOUBLE LOGARITHMIC STABILITY IN THE IDENTIFICATION OF A SCALAR POTENTIAL BY A PARTIAL ELLIPTIC DIRICHLET-TO-NEUMANN MAP

We examine the stability issue in the inverse problem of determining a scalar potential appearing in the stationary Schrödinger equation in a bounded domain, from a partial elliptic Dirichlet-to-Neumann map. Namely, the Dirichlet data is imposed on the shadowed face of the boundary of the domain and the Neumann data is measured on its illuminated face. We establish a log log stability estimate for the L 2 -norm (resp. the H -1 -norm) of H t , for t > 0, and bounded (resp. L 2 ) potentials.

1. Introduction 1.1. Settings and main result. In the present paper Ω is a bounded domain of R n , n ≥ 3, with C 2 boundary Γ. We denote by ν(x) the outward unit normal to Γ computed at x ∈ Γ. For ξ ∈ S n-1 fixed, we introduce the two following subsets of Γ In what follows Γ + (ξ) (resp. Γ -(ξ)) will sometimes be referred to as the ξ-shadowed (resp., ξ-illuminated) face of Γ. Next, given q ∈ L ∞ (Ω), real-valued, we consider the unbounded self-adjoint operator A q in L 2 (Ω), acting on his domain D(A q ) = H 1 0 (Ω) ∩ H 2 (Ω), as A q = -∆ + q.

We assume throughout the entire text that 0 is in the resolvent set of A q (i.e. 0 is not in the spectrum of A q ) and put Q = {q ∈ L ∞ (Ω; R); 0 is not an eigenvalue of A q }.

Date: December 16, 2014.

1

We establish in Section 2 for any q ∈ Q and g ∈ H -1/2 (Γ) that the boundary value problem (abbreviated to BVP in the sequel)

(1.2) (-∆ + q)u = 0 in Ω, u = g on Γ, admits a unique transposition solution u ∈ H ∆ (Ω) = {w ∈ L 2 (Ω); ∆w ∈ L 2 (Ω)} and that the so-called Dirichlet-to-Neumann (DN in short) map

(1.3) Λ q : g → ∂ ν u is a bounded operator from H -1/2 (Γ) into H -3/2 (Γ). For q j ∈ Q, j = 1, 2, we denote by u j the solution to (1.2) where q j is substituted for q. Since u = u 1u 2 satisfies (-∆ + q 1 )u = (q 2q 1 )u 2 in Ω, u = 0 on Γ, and (q 2q 1 )u 2 ∈ L 2 (Ω), it holds true that u ∈ D (A q1 ). Therefore ∂ ν u ∈ H 1/2 (Γ) and

(1.4) Λ q1,q2 = Λ q1 -Λ q2 ∈ B(H -1/2 (Γ), H 1/2 (Γ)), hence the operator

(1.5) Λ q1,q2 : g ∈ H -1/2 (Γ) ∩ E ′ (F ) → Λ q1,q2 (g) |G ,
is bounded from H -1/2 (Γ) ∩ E ′ (F ), endowed with the norm of H -1/2 (Γ), into H 1/2 (G). We denote by Λ q1,q2 the norm of Λ q1,q2 in B(H -1/2 (Γ) ∩ E ′ (F ), H 1/2 (G)).

In the present paper we examine the stability issue in the inverse problem of determining the potential q ∈ Q appearing in (1.2) from the knowledge of Λ q0,q , where q 0 is an priori known suitable potential of Q.

Upon denoting by B X the unit ball of any Banach space X, we may now state the main result of this article as follows.

Theorem 1.1. For any δ > 0 and t > 0 we may find two constants c > 0 and c > 0, both of them depending only on δ and t, such that we have (1.6) q 1q 2 L 2 (Ω) ≤ c Λ q1,q2 + ln c ln Λ q1,q2 -t

, for any q 1 , q 2 ∈ Q ∩ δB L ∞ (Ω) satisfying (q 2q 1 )χ Ω ∈ δB H t (R n ) , and

(1.7) q 1 -q 2 H -1 (Ω) ≤ c Λ q1,q2 + ln c ln Λ q1,q2 -1 , for any q 1 , q 2 ∈ Q ∩ δB L 2 (Ω) .
Let us now briefly comment on Theorem 1.1.

Remarks 1.1. (a) We suppose in Theorem 1.1 that q j , j = 1, 2, are real-valued but it is not hard to see that the statement can be adapted at the expense of greater technical difficulties, to the case of complex-valued potentials. Nevertheless, for the sake of clarity, we shall restrict ourselves to real-valued potentials in the remaining part of this text. (b) For s > n/2 and ǫ ∈ (0, sn/2) we recall from the interpolation theorem [START_REF] Lions | Non-homogenuous boundary value problems and applications I[END_REF]Theorem 12.4,page 73] that

H n/2+ǫ (Ω) = [H s (Ω), H -1 (Ω)] θ with θ = (s -(n/2 + ǫ))/(s + 1
). Therefore we have

q 1 -q 2 L ∞ (Ω) ≤ C(s) q 1 -q 2 1-θ H s (Ω) q 1 -q 2 θ H -1 (Ω) ≤ C(s)δ 1-θ q 1 -q 2 θ H -1 (Ω)
, for any q 1 , q 2 ∈ Q such that q 2 ∈ q 1 + δB H s (Ω) , and some constant C(s) > 0, depending only on s. From this and (1.7) then follows that (1.8)

q 1 -q 2 L ∞ (Ω) ≤ c Λ q1,q2 + ln c ln Λ q1,q2 -1 θ .
(c) Fix t ∈ (0, +∞). Then, arguing as in the derivation of (1.8), we find two positive constants c and c such that the estimate

q 1 -q 2 L 2 (Ω) ≤ c Λ q1,q2 + ln c ln Λ q1,q2 -1 t t+1
, holds uniformly in q 1 , q 2 ∈ Q obeying q 2 ∈ q 1 + δB H t (Ω) . However in the particular case where ∂Ω is C [t]+1 , we point out that the above estimate is weaker than (1.6).

1.2. State of the art and comments. The celebrated inverse problem of determining q from the knowledge of Λ q was first proposed (in a slightly different setting) by Calderón in [C]. The uniqueness issue was treated by Sylvester and Uhlmann in [SU] and a log-type stability estimate was derived by Alessandrini in [A]. As shown by Mandache in [M], this log-type estimate is optimal.

All the above mentioned results were obtained with the full data, i.e. when measurements are performed on the whole boundary Γ. Taking the Neumann data on Γ -(ξ), while the Dirichlet data is imposed on the whole boundary Γ, Bukhgeim and Uhlmann proved in [BU] that partial information of Λ q still determines uniquely the potential. Their result was improved by Kenig, Sjöstrand and Uhlmann in [KSU] by measuring the Dirichlet data on the shadowed face of Γ and the Neumann data on the illuminated one. Moreover a reconstruction result was derived by Nachman and Street in [NS] from the same data as in [KSU].

Stability estimates with partial data go back to Heck and Wang's article [HW], where the L ∞ (Ω)-norm of q is log log stably recovered from Λ q with partial Neumann data. The same type of estimate was derived in [START_REF] Caro | Stability estimates for the Calderón problem with partial data[END_REF]. Both papers require that the Dirichlet data be known on the whole boundary. This constraint was weakened by Caro,Dos Santos Ferreira and Ruiz in [CDR1]. These authors proved log-log stability of q with respect to a partial DN map associated with Dirichlet (resp. Neumann) data measured on a neighborhood of ∪ ξ∈N Γ -(ξ) (resp. ∪ ξ∈N Γ + (ξ)) where N in a subset of S n-1 . Their result, which is similar to (1.6), is established for the L p -norm, p ∈ (1, +∞), of bounded and W λ,p -potentials q with λ ∈ (0, 1/p]. Therefore (1.7) is valid for a wider class of allowable potentials than in [START_REF] Caro | Stability estimates for the Radon transform with restricted data and applications[END_REF].

The derivation of Theorem 1.1 relies on complex geometrical optics (CGO in short) solutions to (1.2) and the Carleman inequality established by Bukhgeim and Uhlmann in [BU]. These are the two main ingredients of the analysis carried out in [HW], but in contrast to [HW], we use here this Carleman estimate to construct CGO solutions vanishing on a definite part of the boundary Γ.

Notice that usual stability estimates in the inverse problem of determining a potential from the full DN map are of log type, while they are of log log type for partial data. Indeed, it turns out that the low frequencies of the Fourier transform of the potential are bounded uniformly in all directions by the DN map, but that this is no longer the case with the partial data. This technical issue can be remedied by using the analytic properties of the Fourier transform. The additional log in the stability estimate for the potential may thus be seen as the price to pay for recovering this analytic function by its values in a subdomain, which is an ill-posed problem.

1.3. Outline. The paper is organized as follows. In Sect. 2 we introduce the transposition solution associated with the BVP (1.2) and rigorously define the various DN maps required by the analysis of the inverse problem. Sect. 3 is devoted to building CGO solutions that vanish on some part of the boundary Γ. These functions are useful for the proof of Theorem 1.1, given in Sect. 4.

Transposition solutions

In this section we define the transposition solution to the BVP associated with suitable data (f, g),

(2.1) (-∆ + q)u = f in Ω, u = g on Γ,
which play a pivotal role in the analysis of the inverse problem carried out in this paper. To this purpose we start by recalling two useful results for the Hilbert space

H ∆ (Ω) = {u ∈ L 2 (Ω); ∆u ∈ L 2 (Ω)} endowed with its natural norm u H∆(Ω) = u 2 L 2 (Ω) + ∆u 2 L 2 (Ω) 1/2
.

The first result is the following trace theorem, borrowed from [START_REF] Bukhgeim | Recovering a potential from partial Cauchy data[END_REF]Lemma 1.1].

Lemma 2.1. For j = 0, 1, the trace map

t j u = ∂ j ν u |Γ , u ∈ D(Ω)
, extends to a continuous operator, still denoted by t j , from H ∆ (Ω) into H -j-1/2 (Γ). Namely, there exists c j > 0, such that the estimate

t j u H -j-1/2 (Γ) ≤ c j u H∆(Ω) ,
holds for every u ∈ H ∆ (Ω).

Let us denote by •, • j+1/2 , j = 0, 1, the duality pairing between H j+1/2 (Γ) and H -j-1/2 (Γ), where the second argument is conjugated. Then we have the following generalized Green formula, which can be found in [START_REF] Bukhgeim | Recovering a potential from partial Cauchy data[END_REF]Corollary 1.2

]. Lemma 2.2. Let q be in L ∞ (Ω). Then, for any u ∈ H ∆ (Ω) and v ∈ H 2 (Ω), we have Ω (∆ -q)uvdx = Ω u(∆ -q)vdx + t 1 u, t 0 v 3/2 -t 0 u, t 1 v 1/2 .
Let q ∈ Q. By the usual H 2 -regularity property for elliptic BVPs (see e.g. [START_REF] Lions | Non-homogenuous boundary value problems and applications I[END_REF]Theorem 5.4,page 165]), we know that for each f ∈ L 2 (Ω) and g ∈ H 3/2 (Γ), there exists a unique solution S q (f, g) ∈ H 2 (Ω) to (2.1). Moreover the linear operator S q is bounded from L 2 (Ω) × H 3/2 (Γ) into H 2 (Ω), i.e. there exists a constant C > 0 such that we have

(2.2) S q (f, g) H 2 (Ω) ≤ C f L 2 (Ω) + g H 3/2 (Γ) .
For further reference we put S q,0 (f ) = S q (f, 0) and S q,1 (g) = S q (0, g), so we have S q (f, g) = S q,0 (f ) + S q,1 (g) from the linearity of S q . Next, applying Lemma 2.2, we get for all (f, g)

∈ L 2 (Ω) × H 3/2 (Γ) and v ∈ H = H 1 0 (Ω) ∩ H 2 (Ω) that (2.3) - Γ g∂ ν vdσ(x) + Ω f vdx = Ω u(-∆ + q)vdx, u = S q (f, g).
In view of the left hand side of (2.3) we introduce the following continuous anti-linear form on H

(2.4)

ℓ(v) = - Γ g∂ ν vdσ(x) + Ω f vdx, v ∈ H.
In light of (2.2), the operator L = ℓ • S q,0 is bounded in L 2 (Ω). Further, with reference to (2.4), we generalize the definition of the anti-linear form ℓ to (f, g) ∈ H * × H -1/2 (Γ), upon setting

ℓ(v) = -g, ∂ ν v 1/2 + f, v , v ∈ H,
where •, • denotes the duality pairing between H and H * , conjugate linear in its second argument. For any

h ∈ L 2 (Ω), L(h) = ℓ (S q,0 (h)) satisfies (2.5) |L(h)| ≤ g H -1/2 (Γ) ∂ ν S q,0 (h) H 1/2 (Γ) + f H * S q,0 (h) H ≤ C g H -1/2 (Γ) + f H * h L 2 (Ω) ,
according to (2.2). Hence L is a continuous anti-linear form on L 2 (Ω). By Riesz representation theorem, there is a unique vector S t q (f, g) ∈ L 2 (Ω) such that we have

-g, ∂ ν S q,0 (h) 1/2 + f, S q,0 (h) = Ω S t q (f, g)hdx, h ∈ L 2 (Ω).
Bearing in mind that A q is boundedly invertible in L 2 (Ω) (since 0 is in the resolvent set of A q ) and that S q,0 = A -1 q , we obtain upon taking h = A q v in above identity, where v is arbitrary in H, that

(2.6) -g, ∂ ν v 1/2 + f, v = Ω S t q (f, g)(-∆ + q)vdx, v ∈ H. Moreover (2.5) entails (2.7) S t q (f, g) L 2 (Ω) ≤ C g H -1/2 (Γ) + f H * .
For each (f, g) ∈ H * × H -1/2 (Γ), S t q (f, g) will be referred to as the transposition solution to the BVP (2.1). As a matter of fact we deduce from (2.6) that (2.8) (-∆ + q)S t q (f, g) = f in the distributional sense in Ω.

Let us establish now that the transposition solution S t q (f, g) coincides with the classical H 2 (Ω)-solution S q (f, g) to (2.1) in the particular case where (f, g)

∈ L 2 (Ω) × H 3/2 (Γ). Proposition 2.1. For any (f, g) ∈ L 2 (Ω) × H 3/2 (Γ) we have S t q (f, g) = S q (f, g).
Proof. Put u = S t q (f, g). We have u ∈ H ∆ (Ω) directly from (2.8) hence t 0 u ∈ H -1/2 (Γ). Further, given ϕ ∈ H 1/2 (Γ), we may find v ∈ H such that t 1 v = ϕ by the usual extension theorem (see e.g. [START_REF] Lions | Non-homogenuous boundary value problems and applications I[END_REF]Theorem 8.3,p. 39]). Applying Lemma 2.2 for such a test function v, we find that

Ω f vdx = Ω (-∆ + q)uvdx = Ω u(-∆ + q)vdx + t 0 u, ϕ 1/2 .
From this and (2.6) then follows that

Ω f vdx = Ω f vdx -g, ϕ 1/2 + t 0 u, t 1 v 1/2 , which entails g -t 0 u, ϕ 1/2 = 0.
Since the above identity holds for any ϕ ∈ H 1/2 (Γ) we obtain that t 0 u = g and hence u = g on Γ. This yields the desired result.

For g ∈ H -1/2 (Γ) we put S t q,1 (g) = S t q (0, g). We have S t q,1 (g) ∈ H ∆ (Ω) by (2.8), with

S t q,1 (g) H∆(Ω) ≤ C 1 + q L ∞ (Ω) g H -1/2 (Γ) , from (2.7). Hence S t q,1 ∈ B(H -1/2 (Γ), H ∆ (Ω)) so we get Λ q = t 1 • S t q,1 ∈ B(H -1/2 (Γ), H -3/2 (Γ))
, with the aid of Lemma 2.1.

Finally we have S t q (f, g) = S t q (f, 0) + S t q (0, g), by linearity of S t q . Put S t q,0 (f ) = S t q (f, 0) and S t q,1 (g) = S t q (0, g). Since S t q,0 ∈ B(H * , H ∆ (Ω)) and S t q,1 ∈ B(H -1/2 (Γ), H ∆ (Ω)), it follows from Lemma 2.1 that

Λ q = t 1 • S t q,1 B(H -1/2 (Γ), H -3/2 (Γ)).
Further, as S t q,1 (g) = S t 0,1 (g) + S q,0 (f ), with f = -qS t 0,1 (g), we get that Λ q = Λ 0 + R q , where the operatorR q

R q : g → t 1 S q,0 -qS t 0,1 (g) ∈ H 1/2 (Γ), is bounded from H -1/2 (Γ) into H 1/2 (Γ).
Remark 2.1. Let us denote by Σ q the (continuous) DN map

Σ q : g ∈ H 3/2 (Γ) → t 1 S q,1 (g) ∈ H 1/2 (Γ).
Then, since q is real-valued, we get from the Green formula that

Γ gΣ q (h)dσ(x) = Γ Σ q (g)hdσ(x), g, h ∈ H 3/2 (Γ),
which entails that Σ * q |H 3/2 (Γ) = Σ q . On the other hand, we deduce from Lemma 2.2 that Σ * q = Λ q .

3. CGO solutions vanishing on some part of the boundary

In this section we build CGO solutions to the Laplace equation appearing in (1.2), that vanish on a prescribed part of the boundary Γ. This is by means of a suitable Carleman estimate borrowed from [BU]. The corresponding result is as follows.

Proposition 3.1. For δ > 0 fixed, let q ∈ δB L ∞ (Ω) . Let ζ, η ∈ S n-1 satisfy ζ • η = 0 and fix ǫ > 0 so small that Γ ǫ -= Γ ǫ -(ζ) = {x ∈ Γ; ζ • ν(x) < -ǫ} = ∅.
Then there exists τ 0 = τ 0 (δ) > 0, such that for any τ ≥ τ 0 we may find ψ ∈ L 2 (Ω) obeying ψ L 2 (Ω) ≤ Cτ -1/2 for some constant C > 0 depending only on δ, Ω and ǫ, and such that the function u = e τ (ζ+iη

)•x (1 + ψ) ∈ H ∆ (Ω) is solution to the BVP (-∆ + q)u = 0 in Ω, u = 0 on Γ ǫ -. Proof.
The proof is made of three steps.

Step 1: A Carleman estimate. For notational simplicity we write Γ ± instead of Γ ± (ζ), which isdefined in (1.1), and recall from [BU] that we may find two constants τ 0 = τ 0 (δ) > 0 and C = C(δ) > 0 such the estimate

Cτ 2 Ω e -2τ x•ζ |v| 2 dx + τ Γ+ |ζ • ν(x)|e -2τ x•ζ |∂ ν v| 2 dσ(x) ≤ Ω e -2τ x•ζ |(∆ -q)v| 2 dx + τ Γ- |ζ • ν(x)|e -2τ x•ζ |∂ ν v| 2 dσ(x),
holds for all τ ≥ τ 0 and v ∈ H. Since Γ ± (-ζ) = Γ ∓ (ζ), the above inequality may be equivalently rewritten as

Cτ 2 Ω e 2τ x•ζ |v| 2 dx + τ Γ- |ζ • ν(x)|e 2τ x•ζ |∂ ν v| 2 dσ(x) (3.1) ≤ Ω e 2τ x•ζ |(∆ -q)v| 2 dx + τ Γ+ |ζ • ν(x)|e 2τ x•ζ |∂ ν v| 2 dσ(x), v ∈ H, τ ≥ τ 0 .
In view of more compact reformulation of (3.1) we introduce for each real number τ the two following scalar products:

(u, v) τ = Ω e 2τ x•ζ uvdx in L 2 (Ω), and φ, ψ τ,µ,± = Γ± µ(x)e 2τ x•ζ φψdσ(x), where µ(x) = |ζ • ν(x)|, in L 2 (Γ ± ).
We denote by L 2 τ (Ω) (resp., L 2 τ,µ (Γ ± )) the space L 2 (Ω) (resp., L 2 (Γ ± )) endowed with the norm • τ (resp. • τ,µ,± ) generated by the scalar product (•, •) τ (resp., •, • τ,µ,± ). With these notations, the estimate (3.1) simply reads

(3.2) Cτ 2 v 2 τ + τ ∂ ν v 2 τ,µ,-≤ (∆ -q)v 2 τ + τ ∂ ν v 2 τ,µ,+ , v ∈ H, τ ≥ τ 0 .
Step 2: Building suitable transposition solutions. Let us identify

L 2 0 (Ω) = L 2 (Ω) (resp., L 2 0,1 (Γ ± ) = L 2 (Γ ± )) with its dual space, so the space dual to L 2 τ (Ω) (resp., L 2 τ,µ (Γ ± ))can be identified with L 2 -τ (Ω) (resp. L 2 -τ,µ -1 (Γ ± )).
Next we consider the operator

(3.3) P : v ∈ H → ((∆ -q)v, ∂ ν v |Γ+ ) ∈ L 2 τ (Ω) × L 2 τ,µ (Γ + ),
which is injective by (3.1). Therefore, for each (f, g)

∈ L 2 -τ (Ω) × L 2 -τ,µ -1 (Γ -), the following anti-linear form (3.4) ℓ(w 1 , w 2 ) = (f, v) + g, ∂ ν v -, (w 1 , w 2 ) = P v, v ∈ H,
where (•, •) (resp., •, • ± ) denotes the usual scalar product in L 2 (Ω) (resp., L 2 (Γ ± )), is well defined on Ran(P ). Moreover it holds true for every (w 1 , w 2 ) = P v, where v is arbitrary in H, that

|ℓ(w 1 , w 2 )| ≤ f -τ v τ + g -τ,µ -1 ,-∂ ν v τ,µ,- (3.5) ≤ τ -1 f -τ + τ -1/2 g -τ,µ -1 ,-τ 2 v 2 τ + τ ∂ ν v 2 τ,µ,- 1/2 .
Thus, upon equipping the space

L 2 τ (Ω) × L 2 τ,µ (Γ + ) with the norm | (w 1 , w 2 ) | τ = w 1 2 τ + τ w 2 2 τ,µ,+ 1/2 ,
we derive from (3.2) and (3.5) that

|ℓ(w 1 , w 2 )| ≤ C τ -1 f -τ + τ -1/2 g -τ,µ -1 ,- (∆ -q)v 2 τ + τ ∂ ν v 2 τ,µ,+ 1/2 ≤ C τ -1 f -τ + τ -1/2 g -τ,µ -1 ,-| P v | τ ,
for some constant C > 0 depending only on δ. As a consequence we have

(3.6) |ℓ(w 1 , w 2 )| ≤ C τ -1 f -τ + τ -1/2 g -τ,µ -1 ,-| (w 1 , w 2 ) | τ , (w 1 , w 2 ) ∈ Ran(P ).
Let us identify the dual space of

L 2 τ (Ω) × L 2 τ,µ (Γ + ) with L 2 -τ (Ω) × L 2 -τ,µ -1 (Γ + ) endowed with the norm | (w 1 , w 2 ) | -τ = w 1 2 -τ + τ -1 w 2 2 -τ,µ-1,+
1/2 . Thus, with reference to (3.3)-(3.4), we deduce from (3.6) upon applying Hahn-Banach extension theorem that there exists

(v 1 , v 2 ) ∈ L 2 -τ (Ω) × L 2 -τ,µ -1 (Γ + ) obeying (3.7) | (v 1 , v 2 ) | -τ ≤ C τ -1 f -τ + τ -1/2 g -τ,µ -1 ,-,
where C > 0 is the same as in the right hand side of (3.6), such that we have

(v 1 , (∆ -q)v) + v 2 , ∂ ν v + = (f, v) + g, ∂ ν v -, v ∈ H.
Bearing in mind that f ∈ H * and gχ Γ-v 2 χ Γ+ ∈ H -1/2 (Γ), where χ Γ± is the characteristic function of Γ ± in Γ, the above identity reads

(-f ), v -gχ Γ--v 2 χ Γ+ , ∂ ν v 1/2 = Ω v 1 (∆ -q)vdx, v ∈ H.
Therefore, by (2.6), v 1 is the transposition solution to the following IBVP:

(3.8) (-∆ + q)v 1 = -f in Ω, v 1 = gχ Γ--v 2 χ Γ+ on Γ.
Step 3: End of the proof. Set ρ = τ (ζ + iη). The last step of the proof involves picking ϕ ∈ D(R n ; [0, 1]) such that ϕ(x) = 1 for x ∈ Γ ǫ -and supp(ϕ

) ∩ Γ ⊂ Γ ǫ/2
-, and considering the transposition solution v 1 to the BVP (3.8) associated with f = qe ρ•x and g = -ϕe ρ•x . Thus, putting ψ = e -ρ•x v 1 , we derive from (3.7) that

ψ 0 = v 1 -τ ≤ C τ -1 qe ρ•x -τ + τ -1/2 ϕe ρ•x -τ,µ -1 ,- ≤ Cτ -1/2 δτ 0 (δ) -1/2 + 2|Γ -| ǫ ,
where |Γ -| denotes the (n -1)-dimensional Lebesgue-measure of Γ -. Further, bearing in mind that ρ • ρ = 0, it easy to check that u = e ρ•x (1 + ψ) ∈ H ∆ (Ω) satisfies (-∆ + q)u = 0 in Ω. Finally, since v 1 = g on Γ -by (3.8), we obtain that ψ = -ϕ = -1 and consequently that u = 0 on Γ ǫ -. This proves the desired result.

Proof of Theorem 1.1

This section contains the proof of Theorem 1.1 which consists of a succession of five lemmas.

4.1.

A suitable set of Fourier variables. For ǫ > 0 we choose η = η(ǫ) ∈ (0, π/2) so small that

(4.1) (1 -sin θ) 2 + 4 cos 2 θ 1/2 < ǫ, θ ∈ (π/2 -η, π/2 + η),
and we define B ǫ as the set of vectors β = (β 1 , . . . , β n ) ∈ R n with the following spherical coordinates (4.2)

             β 1 = s cos θ 1 , β j = s cos θ j j-1 k=1 sin θ k , j = 2, . . . , n -2, β n-1 = s sin φ n-2 k=1 sin θ k , β n = s cos φ n-2
k=1 sin θ k , where s ∈ (0, 1), θ 1 ∈ (π/2η, π/2 + η), θ 2 (0, π/3), θ j ∈ (0, π) for j = 3, . . . , n -2, and φ ∈ (0, 2π). Notice that B ǫ has positive Lebesgue measure in R n given by:

(4.3) |B ǫ | = 1 0 π/2+η π/2-η π/3 0 π 0 . . . π 0 2π 0 s n-1 n-2 k=1 sin k θ n-1-k dsdθ 1 . . . dθ n-2 dφ > 0.
For further reference, we now establish the following result.

Lemma 4.1. Let T be any orthogonal transformation in R n that maps ξ onto e 1 = (1, 0, . . . , 0). Then for all ǫ > 0 and κ ∈ T * B ǫ , there exists ζ ∈ S n-1 satisfying κ • ζ = 0 and |ζ -ξ| < ǫ.

Proof. Let β = (β 1 , . . . , β n ) ∈ B ǫ be given by (4.1)-(4.2). Introduce ζ = ( ζ1 , ζ2 , 0, . . . , 0), where

ζ1 = sin θ 1 sin 2 θ 1 + cos 2 θ1 cos 2 θ2 1/2 , ζ2 = - cos θ1 cos θ2 sin 2 θ 1 + cos 2 θ1 cos 2 θ2 1/2 .
Evidently we have ζ ∈ S n-1 and β • ζ = 0. Moreover it follows from (4.1) that

| ζ -e 1 | 2 = (sin θ 1 -1) 2 + cos 2 θ1 cos 2 θ2 sin 2 θ 1 + cos 2 θ1 cos 2 θ2 ≤ (sin θ 1 -1) 2 + 4 cos 2 θ 1 < ǫ 2 .
Finally, bearing in mind that κ = T * β and e 1 = T ξ, we obtain the desired result upon taking ζ = T * ζ.

4.2. Alessandrini's identity and consequence. For ǫ > 0 put

F ǫ (ζ) = Γ \ Γ ǫ -(ξ) and G ǫ (ξ) = Γ \ Γ ǫ -(-ξ), where Γ ǫ -(±ξ) is the same as in Proposition 3.1. Since F ǫ (ξ) = {x ∈ Γ; ξ • ν(x) ≥ -ǫ} (resp., G ǫ (ξ) = {x ∈ Γ; ξ • ν(x) ≤ ǫ}), it holds true that ∩ ǫ>0 F ǫ (ξ) = {x ∈ Γ; ξ • ν(x) ≥ 0} = Γ + (ξ) (resp., ∩ ǫ>0 G ǫ (ξ) = {x ∈ Γ; ξ • ν(x) ≤ 0} = Γ -(ξ)
). Thus, from the very definitions of F and G, we may choose ǫ 0 = ǫ 0 (ξ, F, G) > 0 so small that (4.4)

F 2ǫ (ξ) ⊂ F and G 2ǫ (ξ) ⊂ G, ǫ ∈ (0, ǫ 0 ].
Having said that we turn now to proving the following statement.

Lemma 4.2. Let T be the same as in Lemma 4.1, let τ ∈ [τ 0 , +∞), where τ = τ 0 (δ) is defined in Proposition 3.1, and let ǫ ∈ [0, ǫ 0 ). Then, there exists a constant C > 0, depending only on Ω, δ and ǫ, such that the estimate

Ω (q 2 -q 1 )e -iκ•x dx ≤ C e 2dτ Λ q1,q2 + τ -1/2 , holds uniformly in κ ∈ rT * B ǫ and r ∈ (0, 2τ ). Here Λ q1,q2 is the B(H -1/2 (Γ) ∩ E ′ (F ), H 1/2 (G))-norm of the operator Λ q1,q2 defined in (1.3)-(1.5), and d = d(Ω) = max x∈Ω |x| < ∞.
Proof. Fix r ∈ (0, 2τ ), κ ∈ rT * B ǫ , and let ζ be given by Lemma 4.

1. Pick ℓ ∈ R n such that ℓ • κ = ℓ • ζ = 0 (which is possible since n ≥ 3) and |κ + ℓ| 2 = |κ| 2 + |ℓ| 2 = 4τ 2 . Set ρ j = (-1) j τ ζ -i κ + (-1) j ℓ 2 , j = 1, 2,
and let u j = e ρj •x (1 + ψ j ) ∈ H ∆ (Ω) be defined in accordance with Proposition 3.1, in such a way that we have (4.5) (-∆ + q j )u j = 0 in Ω, u j = 0 on Γ ǫ -((2j -3)ζ), and (4.6)

ψ j L 2 (Ω) ≤ Cτ -1/2 .
Put u = S t q1,1 (t 0 u 2 ) so we have w = uu 2 = S q1,0 ((q 1q 2 )u 2 ) ∈ H and (4.7)

t 1 w = Λ q1 (t 0 u 2 ) -Λ q2 (t 0 u 2 ).
Upon applying the generalized Green formula of Lemma 2.2 with u = u 1 and v = w, we derive from (4.5) that (4. 8)

Ω (q 2 -q 1 )u 1 u 2 dx = t 0 u 1 , t 1 w 1/2 .
Notice from the second line of (4.5) that the trace t 0 u 2 (resp.,

t 0 u 1 ) is supported in F ǫ (ζ) = Γ \ Γ ǫ -(ζ) (resp., G ǫ (ζ) = Γ \ Γ ǫ -(-ζ)), where Γ ǫ -(±ζ) is defined in Proposition 3.1. Otherwise stated we have F ǫ (ζ) = {x ∈ Γ; ζ • ν(x) ≥ -ǫ} (resp., G ǫ (ζ) = {x ∈ Γ; ζ • ν(x) ≤ ǫ}) and hence F ǫ (ζ) ⊂ F 2ǫ (ξ) (resp., G ǫ (ζ) ⊂ G 2ǫ (ξ))
since |ζ -ξ| < ǫ. From this and (4.4) then follows that supp(t 0 u 2 ) ⊂ F (resp., supp(t 0 u 1 ) ⊂ G), which together with (4.7)-(4.8) yields (4.9)

Ω (q 2 -q 1 )u 1 u 2 dx ≤ Λ q1,q2 t 0 u 1 H -1/2 (Γ) t 0 u 2 H -1/2 (Γ) .
Moreover, by (4.5)-(4.6) and the very definition of u j , j = 1, 2, we get that

t 0 u j H -1/2 (Γ) ≤ c j u j L 2 (Ω) + ∆u j L 2 (Ω) ≤ c j u j L 2 (Ω) + q j u j L 2 (Ω) (4.10) ≤ Ce dτ (1 + τ -1/2 ).
Upon possibly substituting max(1, τ 0 (δ)) for τ 0 (δ) (which does obviously not restrict the generality of the above reasoning) we deduce from (4.9)-(4.10) that (4.11) Ω (q 2q 1 )u 1 u 2 dx ≤ Ce 2dτ Λ q1,q2 . Now the desired result follows readily from (4.6) and (4.11) upon taking into account that u 1 u 2 = e -iκ•x (1 + ψ 1 )(1 + ψ 2 ). 4.3. Bounding the Fourier coefficients. We introduce the function q : R n → R by setting q = (q 2 -q 1 )χ Ω , where χ Ω denotes the characteristic function of Ω in R n . We aim to upper bound the Fourier transform q of q, on the unit ball B of R n , by means of the following direct generalization of [START_REF] Apraiz | Observability inequalities and measurable sets[END_REF]Theorem 4] for complex-valued real-analytic functions.

Theorem 4.1. Assume that the function F : 2B n → C is real-analytic and satisfies the condition

|∂ α F (κ)| ≤ K |α|! ρ |α| , κ ∈ 2B, α ∈ N n ,
for some (K, ρ) ∈ R * + × (0, 1]. Then for any measurable set E ⊂ B with positive Lebesgue measure, there exist two constants M = M (ρ, |E|) > 0 and θ = θ(ρ, |E|) ∈ (0, 1) such that we have

F L ∞ (B) ≤ M K 1-θ 1 |E| E |F (κ)|dκ θ .
The result is as follows.

Lemma 4.3. For all ǫ ∈ (0, ǫ 0 ] there exist two constants C = C(Ω, δ, ǫ) > 0 and θ = θ(Ω, ǫ) ∈ (0, 1), such that we have

| q(κ)| ≤ Ce (1-θ)r e dτ Λ q1,q2 + τ -1/2 θ , κ ∈ rB, r ∈ (0, 2τ ), τ ∈ [τ 0 , +∞).
Proof. Let τ ∈ [τ 0 , +∞) and r ∈ (0, 2τ ) be fixed. By Lemma 4.2, we have

(4.12) | q(rκ)| ≤ C e 2dτ Λ q1,q2 + τ -1/2 , κ ∈ T * B ǫ .
In view of (4.3) we apply Theorem 4.1 with E = T * B ǫ and F (κ) = q(rκ) for κ ∈ 2B n . Indeed, in this particular case it holds true for any α = (α 1 , . . . , α n ) ∈ N n and κ ∈ 2B n that

∂ α F (κ) = Ω q(x)(-ir) |α| n k=1 x α k k e -irκ•x dx 1 . . . dx n , whence (4.13) |∂ α F (κ)| ≤ q L 1 (Ω) r |α| d |α| ≤ q L 1 (Ω) r |α| |α|! |α|! (d -1 ) |α| ≤ q L 1 (Ω) e r |α|! (d -1 ) |α| ,
where we recall that d = d(Ω) = max x∈Ω |x|. Thus, with reference to (4.12)-(4.13), we obtain that

(4.14) | q(rκ)| ≤ Ce (1-θ)r e dτ Λ q1,q2 + τ -1/2 θ , κ ∈ B,
which immediately yields the result.

4.4. Stability inequalities. We turn now to proving the stability inequalities (1.6)-(1.7). We start with (1.6). For t > 0 fixed, we assume that q ∈ H t (R n ) and put M = q H t (R n ) . By Parseval inequality, it holds true for every r > 0 that

q 2 L 2 (Ω) = q 2 L 2 (R n ) = |κ|≤r | q(κ)| 2 dk + |κ|>r | q(κ)| 2 dk (4.15) ≤ |κ|≤r | q(κ)| 2 dk + 1 r 2t |κ|>r |(1 + |κ| 2 ) t | q(κ)| 2 dκ ≤ |κ|≤r | q(κ)| 2 dk + M 2 r 2t , since R n |(1 + |κ| 2 ) t | q(κ)| 2 dκ = q 2 H t (Ω)
. From this and Lemma 4.3 then follows that (4.16)

q 2 L 2 (Ω) ≤ Cr n e 2(1-θ)r e dτ Λ q1,q2 + τ -1/2 2θ + M 2 r 2t , r ∈ (0, 2τ ), τ ∈ [τ 0 , +∞). Let us suppose that (4.17) Λ q1,q2 ∈ (0, γ 0 ),
where γ 0 = υ(τ 0 ) and υ(τ ) = τ -1/2 e -dτ for τ ∈ (0, +∞). Notice that γ 0 ∈ (0, 1) since τ 0 ∈ [1, +∞). Moreover, υ being a strictly decreasing function on [τ 0 , +∞), there exists a unique τ * ∈ (τ 0 , +∞) satisfying 2d , upon recalling that ln x < x for all x ∈ (0, +∞). Further, taking τ = τ * in (4.16) we obtain for each r ∈ (0, 2τ * ) that q 2 L 2 (Ω) ≤ C2 2θ r n e 2r τ -θ * + M 2 /r 2t ≤ C ′ e (n+2)r (2dτ * ) -θ + M 2 /r 2t , where C ′ = C2 3θ d θ . This and (4.18) entail

υ(τ * ) = Λ q1,q2
(4.19) q 2 L 2 (Ω) ≤ C ′ e (n+2)r ln Λ q1,q2 -θ + M 2 r 2t , r ∈ (0, 2τ * ).
The next step of the derivation involves finding r * ∈ (0, 2τ * ) such that both terms C ′ e (n+2)r * ln Λ q1,q2

-θ and M 2 /r 2t * appearing in the right hand side of (4.19) are equal. This can be achieved upon assuming in addition to (4.17) that Λq1,q2 ∈ (0, γ 1 ), where

γ 1 = e - M 2 (n+2)C ′ 1 1+2t-θ
, in such a way that we have

(4.20) (n + 2) ln Λ q1,q2 1+2t-θ ≥ M 2 C ′ .
Indeed, we see from (4.18) that the function ι d : r → (dr) 2t e (n+2)dr satisfies

ι d (2τ * ) > ln Λ q1,q2 2t e (n+2)|ln Λq 1 ,q 2 | > ln Λ q1,q2 2t
+ (n + 2) ln Λ q1,q2 1+2t
,

and
2 L 2 (Ω) ≤ 2M 2 /r 2t * , yields (4.21) q L 2 (Ω) ≤ 2M 2t + n + 2 θ t ln M 2 C ′ 1/θ ln Λ q1,q2 -t
.

Summing up, we obtain (1.6) with c = 2M ((2t + n + 2)/θ) t and c = (M 2 /C ′ ) 1/θ provided Λ q1,q2 is smaller that γ = min j=0,1 γ j .

On the other hand, in the particular case where Λ q1,q2 ≥ γ, we have q L 2 (Ω) ≤ (M/γ) Λ q1,q2 . Putting this together with (4.21) we end up getting (1.6) upon possibly enlarging c.

Finally, we obtain (1.7) by arguing as in the derivation of (1.6) upon preliminarily substituting the estimate

q H -1 (Ω) = |κ|≤r |(1 + |κ| 2 ) -1 | q(κ)| 2 dκ + |κ|>r |(1 + |κ| 2 ) -1 | q(κ)| 2 dκ ≤ |κ|≤r | q(κ)| 2 dκ + 1 r 2 |κ|>r | q(κ)| 2 dκ ≤ |κ|≤r | q(κ)| 2 dκ + M 2 r 2
for (4.15). This completes the proof of Theorem 4.1.

Application to conductivity problem

In this section we examine the stability issue in the inverse problem of determining the conductivity coefficient σ appearing in the system (5.1)

-div(σ∇u) = f in Ω, u = g on Γ, from the partial DN map. The strategy is to link this inverse problem to the one studied in the first four sections of this paper and then apply Theorem 1.1 in order to derive a suitable stability estimate for σ.

Finally, taking into account that φ = σ 1/2 1 σ 1/2 2 is solution to the system (-∆ + q 1 )φ = σ 1/2 2 (q 2q 1 ) in Ω φ = 0 on Γ, we get φ L 2 (Ω) ≤ C q 2q 1 H -1 (Ω) upon taking f = σ 1/2 2 (q 2q 1 ) and g = 0 in (2.7). Thus, applying Theorem 1.1 and recalling (5.5), we obtain the: Corollary 5.1. Let F and G be the same as in section 1, and let δ > 0 and σ 0 > 0. Then for any σ j ∈ δB W 2,∞ (Ω) , j = 1, 2, obeying σ j ≥ σ 0 and the condition (5.6)

σ 1 = σ 2 on Γ and ∂ ν σ 1 = ∂ ν σ 2 on F ∩ G,
we may find a constant C > 0, independent of σ 1 and σ 2 , such that we have:

σ 1 -σ 2 L 2 (Ω) ≤ C Λ σ1,σ2 + ln C ln Λ σ1,σ2 -1
.

Remark 5.1. It is not clear how to weaken assumption (5.6) in Corollary 5.1. Indeed, to our knowledge, the best available result in the mathematical literature (this is a byproduct of [START_REF] Alessandrini | The local Calderòn problem and the determination at the boundary of the conductivity[END_REF]Theorem 2.2,p. 922 and Theorem 2.4,p. 923]) on the recovery of the conductivity at the boundary, claims for any non empty open subset Γ 0 of Γ, and for all σ m , m = 1, 2, taken as in Corollary 5.1 and satisfying the condition supp (σ 1σ 2 ) |Γ ⊂ Γ 0 instead (5.6), that

∂ j ν σ 1 -∂ j ν σ 2 L ∞ (Γ) ≤ C Λ 0 σ1,σ2
1/(1+j) , j = 0, 1.

Here Λ 0 σ1,σ2 denotes the operator g ∈ H -1/2 (Γ) ∩ E ′ (Γ 0 ) → (Λ σ1 -Λ σ2 )(g) |Γ0 ∈ H 1/2 (Γ 0 ), Λ 0 σ1,σ2 is the norm of Λ 0 σ1,σ2 in B(H -1/2 (Γ) ∩ E ′ (Γ 0 ), H 1/2 (Γ 0 )) and C > 0 is a constant that depends neither on σ 1 nor σ 2 .

  ξ) = {x ∈ Γ; ±ξ • ν(x) > 0},and denote by F (resp. G) an open neighborhood of Γ + (ξ) (resp. Γ -(ξ)) in Γ.

  . By elementary computation we find that τ * = 2 ln Λ q1,q2ln τ * /(2d), which entails τ * < ln Λ q1,q2 , since τ * ∈ (1, +∞) and d ∈ [1, +∞). As a consequence the real number τ * is greater than

	2 ln Λ q1,q2 -ln ln Λ q1,q2	/(2d), so we get that
	(4.18)	τ * >	ln Λ q1,q2

  hence ι d (2τ * ) > (M 2 /C ′ ) ln Λ q1,q2

θ according to (4.20). Thus there exists r * ∈ (0, 2τ * ) such that we

have ι d (r * ) = (M 2 /C ′ ) ln Λ q1,q2 θ

. This entails that (2t + n + 2)dr * ≥ 2t ln(dr * ) + (n + 2)dr * is greater that ln (M 2 /C ′ ) ln Λ q1,q2 θ , which combined with the estimate q

Assume that σ ∈ W 1,∞ + (Ω) = {c ∈ W 1,∞ (Ω; R); c(x) ≥ c 0 for some c 0 > 0}. Then for any (f, g) ∈ L 2 (Ω)× H 3/2 (Γ), we know from the standard elliptic theory that (5.1) admits a unique solution S σ (f, g) ∈ H 2 (Ω), and that the linear operator

is bounded. In the more general case where (f, g) ∈ H * × H -1/2 (Γ), we obtain by arguing in the exact same way as in Section 2 that there exists a unique u ∈ L 2 (Ω) obeying

Such a function u will be referred to as the transposition solution of (5.1) and will be denoted by S t σ (f, g). Let us introduce the Hilbert space

. By a slight modification of the proof of Lemma 2.1 (e.g. [BU]), the trace map t σ j u = σ j ∂ j ν u |Γ , u ∈ D(Ω), j = 0, 1, is extended to a linear continuous operator, still denoted by t σ j , from H div(σ∇) (Ω) into H -j-1/2 (Γ). Thus, bearing in mind that S t (0, g) ∈ H ∆ (Ω) for g ∈ H -1/2 (Γ), we see that the DN map

where q σ = σ -1/2 ∆σ 1/2 . As a consequence we have σ 1/2 S t σ (0, g) = S t qσ (0, σ 1/2 g), and hence σ 1/2 S t σ (0, σ -1/2 g) = S t qσ (0, g). From this and the identity t 1 (σ 1/2 w) = σ -1/2 t σ 1 w + 1 2 σ -1/2 (∂ ν σ)t 0 w, which is valid for every w ∈ H 2 (Ω), and generalizes to w ∈ H div(σ∇) (Ω) by duality, we get that

Thus, putting q j = q σj for j = 1, 2, we deduce from (5.3) that

We notice from (5.4) that Λ q1,q2 g = σ

In this case, we may find a constant C > 0, such that we have (5.5) Λ q1,q2 ≤ C Λ σ1,σ2 , where • still denotes the norm of B(H -1/2 (Γ)∩E ′ (F ), H 1/2 (G)). Here we used the fact that the multiplier by σ -1/2 1 is an isomorphism of H ±1/2 (Γ).