The Galvin-Prikry theorem and set existence axioms (Q1117221)

This exceptionally efficient paper is written in terms of so-called Reverse Mathematics (RM), a filigree variant of traditional formalist idea(l)s on classifying formulae by equivalences w.r.t. suitable `base' systems (\(\vdash)\). The critique of RM at the end of \textit{A. Macintyre}'s: ``The strength of weak systems'' [Proc. 11th Wittgenstein Symp. 1986 (P. Weingartner and G. Schurz (eds.)), 43-59 (Hölder- Pichler-Tempski, 1987)] queries the then-widespread assumption of RM that its bold face equivalences are `typical'. More precisely, let F and M be prominent propositions in logical (here, set-theoretic) foundations, resp. (here, combinatorial) mathematics, where both F and M contain (set) parameters, which are restricted to some established category in \(F^-\) and \(M^-\). The broad assumption is that, if \(\vdash (F\leftrightarrow M)\) then also \(\vdash (F^-\leftrightarrow M^-)\). (Otherwise, F and M would hardly be `natural' formalizations of the objects meant in natural mathematical language.) By the result stressed in the author's abstract this fails when M is the theorem in the title, F the principle of monotone inductive definitions, and parameters are restricted to the (logical) so-called light face category \(\Sigma^ 1_ 1\). For a less parochial view than RM this is a case of using a sledge hammer to crack or smash a nut since the general ideals of RM were discredited long before they were formulated; cf. artefacts of formal equivalences by Gödel's incompleteness theorem, to be compared to (impeccably precise, and sometimes ingenious) numerical equivalences in numerology, let alone, (temporary) aberrations about theorems being equivalent to the right axioms (since commutativity is right for proving \(5.7=7.5)\). The sledge hammer above has of course other uses, too, even if not in ordinary combinatorics, where F (and hence (M\(\wedge F)\leftrightarrow M)\) is evident. So only \(F\to M\) is significant, \(F\leftrightarrow M\) being then a ritual (modulo (M\(\wedge F)\leftrightarrow M)\). But there are also other objects, called `logical' in the jargon of ordinary mathematics; for example, the (particular) segments \(L_{\alpha}\) of L cultivated in logic, which satisfy the base system(s) of RM. For these \(L_{\alpha}\), F and \(F^-\) can often be decided much more easily than M or \(M^-\). Depending on whether F or \(\neg F\) holds, \(F\to M\) or \(M\to F\) is of use. At least, by the motto: dégager les hypothèses utiles, it is an error to stress \(\leftrightarrow\) (even when this holds) rather than the relevant, less flashy conjunct. In particular, the failure of the assumption does not spoil the potential of the work for effective knowledge. Perhaps, `crack' is the wrong word since it suggests unheard- of control, and the kind of use above is old hat; familiar from the sixties, for example, in the fanfare to reference [17].