Loading...
Please wait, while we are loading the content...
Similar Documents
A Note on Proofs of the Pigeonhole Principle in Deep Inference
| Content Provider | Semantic Scholar |
|---|---|
| Author | Das, Anupam |
| Copyright Year | 2012 |
| Abstract | It is known that the functional and onto variants of the propositional pigeonhole principle have polynomial-size proofs in the weakest deep inference systems. The unrestricted variant has quasipolynomial-size proofs when dag-like behaviour is permitted. Here we match that upper bound in systems free of dagness, and indeed other compression mechanisms, utilising a similar strategy to that of Atserias, Galesi and Gavalda for the monotone sequent calculus. Preliminaries. We assume general familiarity with deep inference. As introductory material consult [BG09] and [Das12b] for known results on the complexity of deep inference, [Jeř09] for the relationship between deep inference and the monotone sequent calculus, [AGG00] for monotone sequent proofs of the pigeonhole principle and basic properties of threshold formulae, and [GG08] for an introduction to streamlining and atomic flows. The proofs we ultimately obtain are free of compression mechanisms, or uncompressed, in the sense of [Das12a]. All proofs considered are monotone, i.e. there is no use of the negation rules, unless mentioned otherwise. Systems are construed with constants ⊥,> in the standard way, and we use the notation KS to denote the system KS∪ {aw↑, ac↑}. Bold lowercase letters a, b, . . . are used to denote vectors of propositional variables and bold uppercase letters A,B, . . . are used to denote matrices of propositional variables. Threshold formulae and permutations. Threshold formulae assert that at least k out of n inputs are true. Logically, the truth of these formulae is preserved under permutation of the inputs, but it is not an easy task to provide propositional proofs of this fact in the absence of dag-like behaviour, provided in deep inference by the presence of contraction loops. In this section we show that derivations with sequences of contraction loops of length log n can be constructed for certain permutations: interleavings and thereby switching of rows and columns. This ensures that, when eliminating these loops, the derivations only blow up quasipolynomially. Remark 1. Throughout, we will assume that m,n are powers of 2 and m ≤ n. Definition 2 (Threshold formulae). We define monotone divide-and-conquer threshold formulae inductively as follows: THk(a) ≡ > k = 0 a k = 1 ⊥ k > 1 , TH k (a, b) ≡ ∨ i+j=k THi (a) ∧ TH n j (b) Observation 3. THk (a) has size n n) and depth O(log n). Date: June 4, 2012. 1 |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://anupamdas.com/items/PHPProofs/PHPProofs.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
