I saw in an old logic paper that the ParisHarrington theorem can be proved via Overspill. The presentation is unfortunately too technical for me to follow. Does somebody have any insight into this?

3$\begingroup$ It would be helpful if you could include a reference to the paper you mention. $\endgroup$– Sam HopkinsCommented May 16 at 13:53

2$\begingroup$ @SamHopkins, it's in Smorynski's paper "Lectures on nonstandard models of arithmetic". $\endgroup$– Mikhail KatzCommented May 16 at 13:57

7$\begingroup$ When you refer to a proof of the PH theorem, do you mean proving the assertion that the PH partition property is true or rather proving that the assertion is independent of PA? $\endgroup$– Joel David HamkinsCommented May 16 at 14:04

4$\begingroup$ Thanks. I am a little confused by the question and what kind of answer you want, since nearly every argument and construction in models of PA is using overspill. It is a basic method, which amounts simply to induction. Every instance of overspill is simply an application of induction. $\endgroup$– Joel David HamkinsCommented May 16 at 14:12

2$\begingroup$ Overspill is the principle that if $\varphi(n)$ holds in a nonstandard model $M\models\text{PA}$ for every standard $n$, then it holds of some nonstandard element as well. This is an immediate consequence of induction, since the least failure of $\varphi$ must be nonstandard, and there will be other nonstandard elements below that at which it therefore holds. $\endgroup$– Joel David HamkinsCommented May 16 at 14:57
1 Answer
This edit includes a fleshedout version of Smorynski's remark about taking advantage of a nonstandard model of arithmetic (instead of König's lemma) to prove the ParisHarrington (PH) principle from the Infinite Ramsey Theorem. A and B below are preliminary comments; see C for the proof of PH using a nonstandard model.
A. The usual way of showing that PH (the ParisHarrington variant of the finite Ramsey theorem) is true, is to derive it from the infinite Ramsey theorem using König's (tree) Lemma using a proof by contradiction. This proof method goes back to Paris and Harrington's original article in the Handbook of Mathematical Logic. This proof method was preceded by the folklore observation that the finite Ramsey Theorem can be derived from the infinite Ramsey Theorem using König's Lemma.
B. In Corollary 6.5 of Smorynski's paper "Lectures on nonstandard model of Arithmetic" (published in the proceedings of Logic Colloquium 82), a proof of the finite Ramsey theorem from the infinite Ramsey theorem is presented, with the key difference that the appeal to König's Lemma is replaced with a compactness argument plus an overspill argument that allows one contradict the infinite Ramsey theorem by first building a proper elementary extension $\mathcal{N}$ of the standard model of arithmetic in which the negation of a specific instance of the finite Ramsey theorem fails, and then to use overspill in $\mathcal{N}$. Smorynski then points out that a similar strategy yields the veracity of PH.
C. For a set $X$ and $e\in \mathbb{N},$ $\left[ X\right] ^{e}$ is the set of $e$element subsets of $X$, i.e., $$\left[ X\right] ^{e}=\left\{ Y\subseteq X:\left\vert Y\right\vert =e\right\}. $$
For $f:\mathbb{N}\rightarrow \mathbb{N}$, $\mathsf{PHP}(f)$ (The ParisHarrington Principle for $f$) is the following statement:
$\mathsf{PHP}(f)$: For all nonzero $e$ (exponent), $m$ (monochromatic), and $c$ (color) in $\mathbb{N}$ there is some $b$ (big enough) in $\mathbb{% N}$ such that $b\longrightarrow ^{f}\left( m\right) _{c}^{e},$ where $% b\longrightarrow ^{f}\left( m\right) _{c}^{e}$ is shorthand for:
For all functions (colorings) $g:\left[ \{1,...,b\}\right] ^{e}\rightarrow \{1,...,c\}$, there is some $M\subseteq \{1,...,b\}$ such that the following three statements hold:
(1) $g$ is constant (monochromatic) on $\left[ M\right] ^{e}.$
(2) $m\leq \left\vert M\right\vert .$
(3) $f(\min (M))\leq \left\vert M\right\vert .$
Note that the Finite Ramsey Theorem is $\mathsf{PHP}(f)$ for $f$ = the constant zero function, which is equivalent to removing condition (3) above. Also what is commonly referred to as the ParisHarrington Principle ($\mathsf{PHP}$) is $\mathsf{PHP}(f)$ for $f(n)=n.$ As shown by Paris and Harrington, in contrast to the Finite Ramsey Theorem, $\mathsf{PHP}$ is not provable in $\mathsf{PA}$. Thus $\mathsf{PHP}$ is a true but $\mathsf{PA}$unprovable statement. This is in sharp contrast to the fact that the proof of $\mathsf{PHP}$ below using a nonstandard model from Infinite Ramsey Theorem is a minor variant of the proof of Finite Ramsey Theorem from the Infinite Ramsey Theorem using a nonstandard model. As indicated by Smorynski, the idea of using nonstandard models of arithmetic to prove Finite Ramsey Theorem from Infinite Ramsey Theorem is due to Joram Hirschfeld.
Below $(\mathbb{N},+,\times ,f)$ is the result of adjoining the function $f$ to the standard model $(\mathbb{N},+,\times )$ of PA.
Proof of $\mathsf{PHP(f)}$. Suppose to the contrary. Then there is some $e$, $m$, and $c$ in $\mathbb{N}$ such that for all $b\in \mathbb{N},(\mathbb{N},+,\times ,f)\models \lnot \varphi (b),$ where $\varphi (b)$ expresses $% b\longrightarrow ^{f}\left( m\right) _{c}^{e}$. Here we are invoking the fact that finite combinatorial statements can be translated into the language of arithmetic via coding devices, such as Ackermann coding (one can avoide the coding issue by working directly with a model of set theory, but that has its own cost: ease with working with nonstandard models of set theory). Using the compactness theorem, let $(% \mathbb{N}^{\ast },+^{\ast },\times ^{\ast },f^{\ast })$ be a proper elementary extension of $(\mathbb{N},+,\times ,f).$ By overspill applied to $% \lnot \varphi (x)$, there is some nonstandard (infinite) element $s$ of $\mathbb{N}^{\ast }$ such that $(\mathbb{N}^{\ast },+^{\ast },\times ^{\ast },f^{\ast })\models \lnot \varphi (s).$ Thus, as viewed in the structure $(\mathbb{N}^{\ast },+^{\ast },\times ^{\ast },f^{\ast })$, there is some $$g:\left[ \{1,...,s\}\right] ^{e}\rightarrow \{1,...,c\}$$ with the property:
$(\ast )$ There is no $M\subseteq \{1,...,b\}$ that satisfies (1), (2), and (3) of the statement of $\mathsf{PHP}(f)$.
Consider the trace of $g$ on $\mathbb{N}$ (namely $g$ restricted to $[\mathbb{N}]^{e})$. By Infinite Ramsey Theorem $g$ has an infinite monochromatic subset $H\subseteq \mathbb{N}$. List the elements of $H$ in increasing order as $h_{1},h_{2},...$ and then define the finite set $M_{0} = \{h_{1},...,h_{k} \}$, where $k=\max \{m, f(h_1)\}$. Clearly (1) through (3) of the statement of $\mathsf{PHP}(f)$ are satisfied for $M=M_{0}$. But this contradicts $(\ast )$. QED

2$\begingroup$ Just to clarify, here by PH you mean a certain Ramsey theoretic statement (and not the claim that this statement is independent of PA), right? I ask because the questionasker himself seems unclear about this point. $\endgroup$ Commented May 21 at 15:36

2$\begingroup$ Yes indeed, by PH I just mean a particular Ramseytheoretic statement. The fact that PH is not provable in PA is a different story. $\endgroup$ Commented May 21 at 16:25