This is a comment on a post by Andreas Blass here.

I have not read Kripke's statement, apart from Andreas's sketch above, but it sounds familiar from elsewhere, so let me comment a bit on the family of results and the many discussions about a family of unprovable statements of the form "for every n there is a finite set that approximates a model of your theory T to the degree n" (where "to the degree n" is specified separately each time).

The first such statement found in print belongs to Paris and Harrington (see the original article in the Handbook for Mathematical Logic), and is sometimes referred to as "half-baked Paris-Harrington Principle". It says "for every n there exists a finite sequence of points that acts as diagonal indiscernibles for the first n Delta_0 formulas", where "diagonal indiscernibility" or "Paris indiscernibility" is the condition that for any c_i_0 < c_i_1< ... < c_i_k < c_j_1 < ... < c_j_k in the sequence, we have: for every parameter a < c_i_0, the following holds:

\forall x_1 < c_i_1 \exists x_2 < c_i_2.... \phi(a, x_1, x_2... x_k) < -- > \forall x_1 < c_j_1 \exists x_2 < c_j_2... \phi(a, x_1, x_2, ...x_k).

Since that time statements of this form became routine intermediate steps in unprovability proofs. For example Shelah tried to modify this statement and came up with something that should be of strength Pi_1^1-CA_0 (see "On logical sentences in PA").

The same idea is the core of most of Harvey Friedman's proofs in the last 25 years, but at higher levels of sophistication. For example for Proposition C, Friedman has 9 intermediate statements of this shape ("the Transmutations"), where the notion of indiscernibility changes at each step. And for Proposition B you need perhaps only 6 transmutations.

When I was entering the subject in 2002 -- 2003, I wrote a naive article draft on half-baked PH and beyond, tinkering and trying to generalize. But then I realized that this topic is widely developed and discussed in the unprovability community, so since this piece already entered the unprovability community's knowledge pot long before me, perhaps none of it is publishable.

One more thought: there are two or three ways of dressing unprovability proofs. Paris's original dressing was via cuts in models of arithmetic, but after Harrington's simplification of n-densities, they wrote the proof for the Handbook in the finitistic way, via half-baked Paris-Harrington + compactness as I sketched above. After that Paris and his co-workers returned to thinking in terms of cuts in models of arithmetic. Both ways of dressing the proof are equally good, but each person usually chooses one.