Ramsey's theorem, Hales–Jewett and Hindman

Ramsey's theorem for sets and hypergraphs (including size Ramsey numbers and Paris–Harrington), Hales–Jewett and density Hales–Jewett, Hindman's and the pairwise sum theorem via ultrafilters, central, J-, C- and piecewise syndetic sets in semigroups, and grid Ramsey properties.

• Arithmetic progressions in CR-sets
• Density Hales–Jewett theorem
• Homogeneous sets of large logarithmic weight
• Large sets in semigroups
• Infinitary Hales–Jewett theorem
• Monochromatic L-shapes in grid colourings
• Monochromatic pairwise sums in the reals
• Pairwise sum theorem
• Piecewise syndetic sets
• Size Ramsey numbers of hypergraphs

TheoremFinite Ramsey theorem for pairs#✓fully proved

For every number of colors \(r \ge 1\) and every natural number \(k\) there is a natural number \(N\) such that for every coloring of the subsets of \(\{0, 1, \dots, N - 1\}\) with \(r\) colors there are a \(k\)-element subset \(S\) and a color \(c\) such that every \(2\)-element subset of \(S\) has color \(c\).

public theorem ramsey_two_uniform {r k : ℕ} (hr : 0 < r) :
    ∃ N : ℕ, ∀ φ : Finset (Fin N) → Fin r,
      ∃ S : Finset (Fin N), S.card = k ∧ ∃ c : Fin r, ∀ T ∈ S.powersetCard 2, φ T = c

Sources

• F. P. Ramsey, On a Problem of Formal Logic, Proc. London Math. Soc. s2-30 (1930), 264-286, DOI 10.1112/PLMS/S2-30.1.264.

Used by 1

Used bySchur's theorem

TheoremStrengthened finite Ramsey theorem (Paris–Harrington principle)#✓fully proved

For all integers \(c \ge 1\), \(k \ge 1\) and \(m \ge 1\) there is a natural number \(N\) such that for every coloring \(f\) of the finite subsets of \(\mathbb{N}\) with \(c\) colors there is a nonempty set \(H \subseteq \{1, \dots, N\}\) with \(|H| \ge m\) and \(\min H \le |H|\) such that all \(k\)-element subsets of \(H\) have the same color: some color \(t\) satisfies \(f(S) = t\) for every \(k\)-element subset \(S \subseteq H\).

theorem paris_harrington :
    ∀ c k m : ℕ, 0 < c → 0 < k → 0 < m → ∃ N : ℕ,
      ∀ f : Finset ℕ → Fin c,
        ∃ H : Finset ℕ, ∃ hH : H.Nonempty,
          H ⊆ Finset.Icc 1 N ∧
          m ≤ H.card ∧
          H.min' hH ≤ H.card ∧
          ∃ t : Fin c, ∀ S : Finset ℕ, S ⊆ H → S.card = k → f S = t

Sources

• J. Paris and L. Harrington, Handbook of Mathematical Logic, ed. Barwise (1977); Graham-Rothschild-Spencer, Ramsey Theory. The statement is the finite combinatorial form with the largeness condition; its independence from PA is not part of it.

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.