It is well known that S12 cannot prove the injective weak pigeonhole principle for polynomial time functions unless RSA is insecure. In this note we investigate the provability of the surjective weak pigeonhole principle in S12 for provably weaker function classes.

We study the extension 123) of the theory S21 by instances of the dual weak pigeonhole principle for p-time functions, dWPHPx2x. We propose a natural framework for formalization of randomized algorithms in bounded arithmetic, and use it to provide a strengthening of Wilkie's witnessing theorem for S21+dWPHP. We construct a propositional proof system WF , which captures the Π1b-consequences of S21+dWPHP. We also show that WF p-simulates the Unstructured Extended Nullstellensatz proof system of Buss et al. 256). (...) We prove that dWPHP is equivalent to a statement asserting the existence of a family of Boolean functions with exponential circuit complexity. Building on this result, we formalize the Nisan–Wigderson construction in a conservative extension of S21+dWPHP. (shrink)

This article is a continuation of our search for tautologies that are hard even for strong propositional proof systems like EF, cf. [Kra-wphp,Kra-tau]. The particular tautologies we study, the τ-formulas, are obtained from any.

We show, under the assumption that factoring is hard, that a model of PV exists in which the polynomial hierarchy does not collapse to the linear hierarchy; that a model of S21 exists in which NP is not in the second level of the linear hierarchy; and that a model of S21 exists in which the polynomial hierarchy collapses to the linear hierarchy. Our methods are model-theoretic. We use the assumption about factoring to get a model in which the (...) class='Hi'>weak pigeonhole principle fails in a certain way, and then work with this failure to obtain our results. As a corollary of one of the proofs, we also show that in S21 the failure of WPHP (for Σb1 definable relations) implies that the strict version of PH does not collapse to a finite level. (shrink)

We bring together some facts about the weak pigeonhole principle from bounded arithmetic, complexity theory, cryptography and abstract model theory. We characterize the models of arithmetic in which WPHP fails as those which are determined by an initial segment and prove a conditional separation result in bounded arithmetic, that PV + lies strictly between PV and S21 in strength, assuming that the cryptosystem RSA is secure.

We define the notion of approximate Euler characteristic of definable sets of a first order structure. We show that a structure admits a non-trivial approximate Euler characteristic if it satisfies weak pigeonhole principle WPHP2nn: two disjoint copies of a non-empty definable set A cannot be definably embedded into A, and principle CC of comparing cardinalities: for any two definable sets A, B either A definably embeds in B or vice versa. Also, a structure admitting a non-trivial (...) approximate Euler characteristic must satisfy WPHP2nn.Further we show that a structure admits a non-trivial dimension function on definable sets if and only if it satisfies weak pigeonhole principle WPHPn2n: for no definable set A with more than one element can A2 definably embed into A. (shrink)

The infinite pigeonhole principle for 2-partitions asserts the existence, for every set A, of an infinite subset of A or of its complement. In this paper, we study the infinite pigeonhole pr...

We consider exponentially large finite relational structures (with the universe {0.1}ⁿ) whose basic relations are computed by polynomial size (nO(1)) circuits. We study behaviour of such structures when pulled back by P/poly maps to a bigger or to a smaller universe. In particular, we prove that: 1. If there exists a P/poly map g: {0.1} → {0.1}m, n < m, iterable for a proof system then a tautology (independent of g) expressing that a particular size n set is dominating in (...) a size 2ⁿ tournament is hard for the proof system. 2. The search problem WPHP, decoding RSA or finding a collision in a hashing function can be reduced to finding a size m homogeneous subgraph in a size 22m graph. Further we reduce the proof complexity of a concrete tautology (expressing a Ramsey property of a graph) in strong systems to the complexity of implicit proofs of implicit formulas in weak proof systems. (shrink)

We shall investigate certain set-theoretic pigeonhole principles which arise as generalizations of the usual pigeonhole principle; and we shall show that many of them are equivalent to full AC. We discuss also several restricted cases and variations of those principles and relate them to restricted choice principles. In this sense the pigeonhole principle is a rich source of weak choice principles. It is shown that certain sequences of restricted pigeonhole principles form implicational hierarchies (...) with respect to ZF. We state also several open problems in order to indicate the extent to which the whole subject of pigeonhole principles requires further exploration. (shrink)

There exist two main notions of typicality in computability theory, namely, Cohen genericity and randomness. In this article, we introduce a new notion of genericity, called partition genericity, which is at the intersection of these two notions of typicality, and show that many basis theorems apply to partition genericity. More precisely, we prove that every co-hyperimmune set and every Kurtz random is partition generic, and that every partition generic set admits weak infinite subsets, for various notions of weakness. In (...) particular, we answer a question of Kjos-Hanssen and Liu by showing that every Kurtz random admits an infinite subset which does not compute any set of positive effective Hausdorff dimension. Partition genericity is a partition regular notion, so these results imply many existing pigeonhole basis theorems. (shrink)

We prove that the theory IΔ0, extended by a weak version of the Δ0-Pigeonhole Principle, proves that every integer is the sum of four squares (Lagrange's theorem). Since the required weak version is derivable from the theory IΔ0 + ∀x (xlog(x) exists), our results give a positive answer to a question of Macintyre (1986). In the rest of the paper we consider the number-theoretical consequences of a new combinatorial principle, the ‘Δ0-Equipartition Principle’ (Δ0EQ). In (...) particular we give a new proof, which can be formalized in IΔ0 + Δ0EQ, of the fact that every prime of the form 4n + 1 is the sum of two squares. (shrink)

Hirst investigated a natural restriction of Hindman’s Finite Sums Theorem—called Hilbert’s Theorem—and proved it equivalent over \ to the Infinite Pigeonhole Principle for all colors. This gave the first example of a natural restriction of Hindman’s Theorem provably much weaker than Hindman’s Theorem itself. We here introduce another natural restriction of Hindman’s Theorem—which we name the Adjacent Hindman’s Theorem with apartness—and prove it to be provable from Ramsey’s Theorem for pairs and strictly stronger than Hirst’s Hilbert’s Theorem. The (...) lower bound is obtained by a direct combinatorial implication from the Adjacent Hindman’s Theorem with apartness to the Increasing Polarized Ramsey’s Theorem for pairs introduced by Dzhafarov and Hirst. In the Adjacent Hindman’s Theorem homogeneity is required only for finite sums of adjacent elements. (shrink)

We show that for each n ≥ 1, if T2n does not prove the weak pigeonhole principle for Σbn functions, then the collection scheme B Σ1 is not finitely axiomatizable over T2n. The same result holds with Sn2 in place of T 2n.

We investigate the provability of some properties of abelian groups and quadratic residues in variants of bounded arithmetic. Specifically, we show that the structure theorem for finite abelian groups is provable in S22 + iWPHP, and use it to derive Fermat's little theorem and Euler's criterion for the Legendre symbol in S22 + iWPHP extended by the pigeonhole principle PHP. We prove the quadratic reciprocity theorem in the arithmetic theories T20 + Count2 and I Δ0 + Count2 with (...) modulo-2 counting principles. (shrink)

Journal of Mathematical Logic, Volume 22, Issue 03, December 2022. We study a new class of NP search problems, those which can be proved total using standard combinatorial reasoning based on approximate counting. Our model for this kind of reasoning is the bounded arithmetic theory [math] of [E. Jeřábek, Approximate counting by hashing in bounded arithmetic, J. Symb. Log. 74(3) (2009) 829–860]. In particular, the Ramsey and weak pigeonhole search problems lie in the new class. We give a (...) purely computational characterization of this class and show that, relative to an oracle, it does not contain the problem CPLS, a strengthening of PLS. As CPLS is provably total in the theory [math], this shows that [math] does not prove every [math] sentence which is provable in bounded arithmetic. This answers the question posed in [S. Buss, L. A. Kołodziejczyk and N. Thapen, Fragments of approximate counting, J. Symb. Log. 79(2) (2014) 496–525] and represents some progress in the program of separating the levels of the bounded arithmetic hierarchy by low-complexity sentences. Our main technical tool is an extension of the “fixing lemma” from [P. Pudlák and N. Thapen, Random resolution refutations, Comput. Complexity, 28(2) (2019) 185–239], a form of switching lemma, which we use to show that a random partial oracle from a certain distribution will, with high probability, determine an entire computation of a [math] oracle machine. The introduction to the paper is intended to make the statements and context of the results accessible to someone unfamiliar with NP search problems or with bounded arithmetic. (shrink)

In this paper we generalize the pigeonhole principle by using isols as our fundamental counting tool.

We establish a course-of-values induction principle for K-finite sets in intuitionistic type theory. Using this principle, we prove a pigeonhole principle conjectured by Bénabou and Loiseau. We also comment on some variants of this pigeonhole principle.

We give a level-by-level analysis of the Weak Vopěnka Principle for definable classes of relational structures ( $\mathrm {WVP}$ ), in accordance with the complexity of their definition, and we determine the large-cardinal strength of each level. Thus, in particular, we show that $\mathrm {WVP}$ for $\Sigma _2$ -definable classes is equivalent to the existence of a strong cardinal. The main theorem (Theorem 5.11) shows, more generally, that $\mathrm {WVP}$ for $\Sigma _n$ -definable classes is equivalent to the (...) existence of a $\Sigma _n$ -strong cardinal (Definition 5.1). Hence, $\mathrm {WVP}$ is equivalent to the existence of a $\Sigma _n$ -strong cardinal for all $n<\omega $. (shrink)

We show that short bounded-depth Frege proofs of matrix identities, such as PQ=I⊃QP=I (over the field of two elements), imply short bounded-depth Frege proofs of the pigeonhole principle. Since the latter principle is known to require exponential-size bounded-depth Frege proofs, it follows that the propositional version of the matrix principle also requires bounded-depth Frege proofs of exponential size.

The combinatorial parity principle states that there is no perfect matching on an odd number of vertices. This principle generalizes the pigeonhole principle, which states that for a fixed bipartition of the vertices, there is no perfect matching between them. Therefore, it follows from recent lower bounds for the pigeonhole principle that the parity principle requires exponential-size bounded-depth Frege proofs. Ajtai previously showed that the parity principle does not have polynomial-size bounded-depth Frege (...) proofs even with the pigeonhole principle as an axiom schema. His proof utilizes nonstandard model theory and is nonconstructive. We improve Ajtai's lower bound from barely superpolynomial to exponential and eliminate the nonstandard model theory. Our lower bound is also related to the inherent complexity of particular search classes . In particular, oracle separations between the complexity classes PPA and PPAD, and between PPA and PPP also follow from our techniques. (shrink)

Cook and Reckhow defined a propositional formulation of the pigeonhole principle. This paper shows that there are Frege proofs of this propositional pigeonhole principle of polynomial size. This together with a result of Haken gives another proof of Urquhart's theorem that Frege systems have an exponential speedup over resolution. We also discuss connections to provability in theories of bounded arithmetic.

The pigeonhole principle is a well-known mathematical principle and is quite simple to understand. It goes as follows: If n items are placed into m containers, and if m (...) (cardinal) instead of an identifier (nominal). They suggest quantities first need to be turned into categories. We believe this difference can instead be explained by pragmatic factors not taken into account in their study. We disambiguate the problems given to participants and study the effects of their disambiguation and the influence of different kinds of quantities: countable and mass. We show that using a problem with countable quantities instead of hair, usually understood as non-countable, increase the performance of participants, no longer distinguishable from that of the nominal problem. (shrink)

The Pigeonhole Principle states that if n items are sorted into m categories and if n > m, then at least one category must contain more than one item. For instance, if 22 pigeons are put into 17 pigeonholes, at least one pigeonhole must contain more than one pigeon. This principle seems intuitive, yet when told about a city with 220,000 inhabitants none of whom has more than 170,000 hairs on their head, many people think that (...) it is merely likely that two inhabitants have the exact same number of hair. This failure to apply the Pigeonhole Principle might be due to the large numbers used, or to the cardinal rather than nominal presentation of these numbers. We show that performance improved both when the numbers are presented nominally, and when they are small, albeit less so. We discuss potential interpretations of these results in terms of intuition and reasoning. (shrink)

A proof of the (propositional) Craig interpolation theorem for cut-free sequent calculus yields that a sequent with a cut-free proof (or with a proof with cut-formulas of restricted form; in particular, with only analytic cuts) with k inferences has an interpolant whose circuit-size is at most k. We give a new proof of the interpolation theorem based on a communication complexity approach which allows a similar estimate for a larger class of proofs. We derive from it several corollaries: (1) Feasible (...) interpolation theorems for the following proof systems: (a) resolution (b) a subsystem of LK corresponding to the bounded arithmetic theory S 2 2 (α) (c) linear equational calculus (d) cutting planes. (2) New proofs of the exponential lower bounds (for new formulas) (a) for resolution ([15]) (b) for the cutting planes proof system with coefficients written in unary ([4]). (3) An alternative proof of the independence result of [43] concerning the provability of circuit-size lower bounds in the bounded arithmetic theory S 2 2 (α). In the other direction we show that a depth 2 subsystem of LK does not admit feasible monotone interpolation theorem (the so called Lyndon theorem), and that a feasible monotone interpolation theorem for the depth 1 subsystem of LK would yield new exponential lower bounds for resolution proofs of the weak pigeonhole principle. (shrink)

We develop approximate counting of sets definable by Boolean circuits in bounded arithmetic using the dual weak pigeonhole principle (dWPHP(PV)), as a generalization of results from [15]. We discuss applications to formalization of randomized complexity classes (such as BPP, APP, MA, AM) in PV₁ + dWPHP(PV).

We study the long-standing open problem of giving$\forall {\rm{\Sigma }}_1^b$separations for fragments of bounded arithmetic in the relativized setting. Rather than considering the usual fragments defined by the amount of induction they allow, we study Jeřábek’s theories for approximate counting and their subtheories. We show that the$\forall {\rm{\Sigma }}_1^b$Herbrandized ordering principle is unprovable in a fragment of bounded arithmetic that includes the injective weak pigeonhole principle for polynomial time functions, and also in a fragment that includes (...) the surjective weak pigeonhole principle for FPNPfunctions. We further give new propositional translations, in terms of random resolution refutations, for the consequences of$T_2^1$augmented with the surjective weak pigeonhole principle for polynomial time functions. (shrink)

In 2007. Terence Tao wrote on his blog an essay about soft analysis, hard analysis and the finitization of soft analysis statements into hard analysis statements. One of his main examples was a quasi-finitization of the infinite pigeonhole principle IPP, arriving at the "finitary" infinite pigeonhole principle FIPP₁. That turned out to not be the proper formulation and so we proposed an alternative version FIPP₂. Tao himself formulated yet another version FIPP₃ in a revised version of (...) his essay. We give a counterexample to FIPP₁ and discuss for both of the versions FIPP₂ and FIPP₃ the faithfulness of their respective finitization of IPP by studying the equivalences IPP ↔ FIPP₂ and IPP ↔ FIPP₃ in the context of reverse mathematics ([9]). In the process of doing this we also introduce a continuous uniform boundedness principle CUB as a formalization of Tao's notion of a correspondence principle and study the strength of this principle and various restrictions thereof in terms of reverse mathematics, i.e., in terms of the "big five" subsystems of second order arithmetic. (shrink)

We investigate the possibility to characterize (multi) functions that are Σ b i -definable with small i (i = 1, 2, 3) in fragments of bounded arithmetic T 2 in terms of natural search problems defined over polynomial-time structures. We obtain the following results: (1) A reformulation of known characterizations of (multi)functions that are Σ b 1 - and Σ b 2 -definable in the theories S 1 2 and T 1 2 . (2) New characterizations of (multi)functions that are (...) Σ b 2 - and Σ b 3 -definable in the theory T 2 2 . (3) A new non-conservation result: the theory T 2 2 (α) is not ∀Σ b 1 (α)-conservative over the theory S 2 2 (α). To prove that the theory T 2 2 (α) is not ∀Σ b 1 (α)-conservative over the theory S 2 2 (α), we present two examples of a Σ b 1 (α)-principle separating the two theories: (a) the weak pigeonhole principle WPHP (a 2 , f, g) formalizing that no function f is a bijection between a 2 and a with the inverse g, (b) the iteration principle Iter (a, R, f) formalizing that no function f defined on a strict partial order ( $\{0,\dots,a\}$ , R) can have increasing iterates. (shrink)

Pudlák shows that bounded arithmetic proves an upper bound on the Ramsey number Rr . We will strengthen this result by improving the bound. We also investigate lower bounds, obtaining a non-constructive lower bound for the special case of 2 colors , by formalizing a use of the probabilistic method. A constructive lower bound is worked out for the case when the monochromatic set size is fixed to 3 . The constructive lower bound is used to prove two “reversals”. To (...) explain this idea we note that the Ramsey upper bound proof for k=3 uses the weak pigeonhole principle in a significant way. The Ramsey upper bound proof for the case in which the upper bound is not explicitly mentioned, uses the totality of the exponentiation function in a significant way. It turns out that the Ramsey upper bounds actually imply the respective principles used to prove them, indicating that these principles were in some sense necessary. (shrink)

We consider a modification of the pigeonhole principle, M P H P, introduced by Goerdt in [7]. M P H P is defined over n pigeons and log n holes, and more than one pigeon can go into a hole (according to some rules). Using a technique of Razborov [9] and simplified by Impagliazzo, Pudlák and Sgall [8], we prove that any Polynomial Calculus refutation of a set of polynomials encoding the M P H P, requires degree Ω(log (...) n). We also prove a simple Lemma giving a simulation of Resolution by Polynomial Calculus. Using this lemma, and a Resolution upper bound by Goerdt [7], we obtain that the degree lower bound is tight. Our lower bound establishes the optimality of the tree-like Resolution simulation by the Polynomial Calculus given in [6]. (shrink)

We show how to formalize approximate counting via hash functions in subsystems of bounded arithmetic, using variants of the weak pigeonhole principle. We discuss several applications, including a proof of the tournament principle, and an improvement on the known relationship of the collapse of the bounded arithmetic hierarchy to the collapse of the polynomial-time hierarchy.

We look for a converse to a result from [N. Thapen, A model-theoretic characterization of the weak pigeonhole principle, Annals of Pure and Applied Logic 118 175–195] that if the weak pigeonhole principle fails in a model K of bounded arithmetic, then there is an end-extension of K interpretable inside K. We show that if a model J of an induction-free theory of arithmetic is interpretable inside K, then either J is isomorphic to an (...) initial segment of K , or K is isomorphic to an initial segment of J and in this case the weak pigeonhole principle fails in K. This result is formulated in terms of a theory of bounded arithmetic with a greatest element. We go on to consider structures defined by oracles, and use the probabilistic witnessing theorem for to give a general criterion for what can be proved about these using the weak pigeonhole principle. We also show that the injective WPHP is not provable in this theory in the relativized case. (shrink)

The design argument for God’s existence was critically assessed when in the growth of modern science the cognitive value of teleological categories was called into question. In recent discussions dealing with anthropic principles there has appeared a new version of the design argument, in which cosmic design is described without the use of teleological terms. The weak anthropic principle (WAP), a most critical version of all these principles, describes the fine-tuning of physical parameters necessary to the genesis of (...) carbon-based life. Consequently, a new version of the philosophical design argument can be developed on the basis of the weak anthropic principle.(edited). (shrink)

It is shown to be consistent with set theory that every set of reals of size ℵ1 is null yet there are ℵ1 planes in Euclidean 3-space whose union is not null. Similar results will be obtained for other geometric objects. The proof relies on results from harmonic analysis about the boundedness of certain harmonic functions and a measure theoretic pigeonhole principle.

A modern assessment of the classical Boltzmann-Schuetz argument for large-scale entropy fluctuations as the origin of our observable cosmological domain is given.The emphasis is put on the central implication of this picture which flatly contradicts the weak anthropic principle as an epistemological statement about the universe. Therefore, to associate this picture with the anthropic principle as it is usually done is unwarranted. In particular, Feynman's criticism of theanthropic principle based on the entropy-fluctuation picture is a product (...) of this semantic confusion. (shrink)

The set-theoretic axiom WISC states that for every set there is a set of surjections to it cofinal in all such surjections. By constructing an unbounded topos over the category of sets and using an extension of the internal logic of a topos due to Shulman, we show that WISC is independent of the rest of the axioms of the set theory given by a well-pointed topos. This also gives an example of a topos that is not a predicative topos (...) as defined by van den Berg. (shrink)

Sam Buss produced the first polynomial size Frege proof of thepigeonhole principle. We introduce a variation of that problem and producea simpler proof based on parity. The proof appearing here has an upperbound that is quadratic in the size of the input formula.

Goncharov and Peretyat'kin independently gave necessary and sufficient conditions for when a set of types of a complete theory is the type spectrum of some homogeneous model of. Their result can be stated as a principle of second order arithmetic, which is called the Homogeneous Model Theorem (HMT), and analyzed from the points of view of computability theory and reverse mathematics. Previous computability theoretic results by Lange suggested a close connection between HMT and the Atomic Model Theorem (AMT), which (...) states that every complete atomic theory has an atomic model. The authors show that HMT and AMT are indeed equivalent in the sense of reverse mathematics, as well as in a strong computability theoretic sense and do the same for an analogous result of Peretyat'kin giving necessary and sufficient conditions for when a set of types is the type spectrum of some model. (shrink)

The rigid relation principle, introduced in this article, asserts that every set admits a rigid binary relation. This follows from the axiom of choice, because well-orders are rigid, but we prove that it is neither equivalent to the axiom of choice nor provable in Zermelo-Fraenkel set theory without the axiom of choice. Thus, it is a new weak choice principle. Nevertheless, the restriction of the principle to sets of reals is provable without the axiom of choice.