We study the proof complexity of Paris-Harrington’s Large Ramsey Theorem for bi-colorings of graphs and of off-diagonal Ramsey’s Theorem. For Paris-Harrington, we prove a non-trivial conditional lower bound in Resolution and a non-trivial upper bound in bounded-depth Frege. The lower bound is conditional on a (very reasonable) hardness assumption for a weak (quasi-polynomial) Pigeonhole principle in R es (2). We show that under such an assumption, there is no refutation of the Paris-Harrington formulas of size quasi-polynomial in the number of propositional variables. The proof technique for the lower bound extends the idea of using a combinatorial principle to blow up a counterexample for another combinatorial principle beyond the threshold of inconsistency. A strong link with the proof complexity of an unbalanced off-diagonal Ramsey principle is established. This is obtained by adapting some constructions due to Erdős and Mills. We prove a non-trivial Resolution lower bound for a family of such off-diagonal Ramsey principles.

Abstract We characterize the effective content and the proof-theoretic strength of a Ramsey-type theorem for bi-colorings of so-called exactly large sets. An exactly large set is a set $X \subset {\bf{N}}$ such that ${\rm{card}}\left( X \right) = {\rm{min}}\left( X \right) + 1$ . The theorem we analyze is as follows. For every infinite subset M of N, for every coloring C of the exactly large subsets of M in two colors, there exists and infinite subset L of M such that C is constant on all exactly large subsets of L. This theorem is essentially due to Pudlák and Rödl and independently to Farmaki. We prove that—over RCA0 —this theorem is equivalent to closure under the ωth Turing jump (i.e., under arithmetical truth). Natural combinatorial theorems at this level of complexity are rare. In terms of Reverse Mathematics we give the first Ramsey-theoretic characterization of ${\rm{ACA}}_0^ +$ . Our results give a complete characterization of the theorem from the point of view of Computability Theory and of the Proof Theory of Arithmetic. This nicely extends the current knowledge about the strength of Ramsey’s Theorem. We also show that analogous results hold for a related principle based on the Regressive Ramsey’s Theorem. We conjecture that analogous results hold for larger ordinals.

We study the proof complexity of Paris-Harrington's Large Ramsey Theorem for bi-colorings of graphs. We prove a non-trivial conditional lower bound in Resolution and a quasi-polynomial upper bound in bounded-depth Frege. The lower bound is conditional on a (very reasonable) hardness assumption for a weak (quasi-polynomial) Pigeonhole principle in RES(2). We show that under such assumption, there is no refutation of the Paris-Harrington formulas of size quasi-polynomial in the number of propositional variables. The proof technique for the lower bound extends the idea of using a combinatorial principle to blow-up a counterexample for another combinatorial principle beyond the threshold of inconsistency. A strong link with the proof complexity of an unbalanced Ramsey principle for triangles is established. This is obtained by adapting some constructions due to Erdos and Mills.

Abstract We investigate a new paradigm in the context of learning in the limit, namely, learningcorrection grammarsfor classes ofcomputably enumerable (c.e.)languages. Knowing a language may feature a representation of it in terms oftwogrammars. The second grammar is used to make corrections to the first grammar. Such a pair of grammars can be seen as a single description of (or grammar for) the language. We call such grammarscorrection grammars. Correction grammars capture the observable fact that peopledocorrect their linguistic utterances during their usual linguistic activities. We show that learning correction grammars for classes of c.e. languages in theTxtEx-mode(i.e., converging to a single correct correction grammar in the limit) is sometimes more powerful than learning ordinary grammars even in theTxtBc-model (where the learner is allowed to converge to infinitely many syntactically distinct but correct conjectures in the limit). For eachn≥ 0. there is a similar learning advantage, again in learning correction grammars for classes of c.e. languages, but where we compare learning correction grammars that maken+ 1 corrections to those that makencorrections. The concept of a correction grammar can be extended into the constructive transfinite, using the idea of counting-down from notations for transfinite constructive ordinals. This transfinite extension can also be conceptualized as being about learning Ershov-descriptions for c.e. languages. Forua notation in Kleene's general system (O, <o) of ordinal notations for constructive ordinals, we introduce the concept of anu-correction grammar, whereuis used to bound the number of corrections that the grammar is allowed to make. We prove a general hierarchy result: ifuandvare notations for constructive ordinals such thatu