Reverse mathematics and marriage problems with finitely many solutions (Q335003)

This paper is a follow up to [the first author, Contemp. Math. 106, 181--196 (1990; Zbl 0701.03032)] and [the authors, Arch. Math. Logic 55, No. 7--8, 1015--1024 (2016; Zbl 1355.03011)], dealing with the reverse mathematics of marriage theorems. By a \textit{marriage theorem} we mean the statement of a necessary and sufficient condition for the existence of a solution to a marriage problem. By a \textit{marriage problem} we mean a triple \((B,G,R)\) where \(B\) is a set of ``boys'', \(G\) is a set of ``girls'' and \(R \subseteq B\times G\) is the ``acquaintance relation'' between boys and girls. A \textit{solution} to a marriage problem is an injection from \(B\) to \(G\) mapping each boy to a girl he is acquainted with. A marriage problem is called: (1) \textit{finite} if \(B\) and \(G\) are finite sets, (2) \textit{with finite acquaintance} if each boy knows only finitely many girls, (3) \textit{bounded} if there is a function bounding the number of girls that a boy is acquainted with. The pattern emerging from Hirst's first results [loc. cit.] is the following: Finite marriage theorems (such as \textit{P. Hall}'s, see [J. Lond. Math. Soc. 10, 26--30 (1935; Zbl 0010.34503)]) are provable in \(\mathrm{RCA}_0\), bounded marriage problems are equivalent to \(\mathrm{WKL}_0\), and infinite marriage theorems with finite acquaintance (such as \textit{M. Hall jun.}'s, see [Bull. Am. Math. Soc. 54, 922--926 (1948; Zbl 0032.27101)]) are equivalent to \(\mathrm{ACA}_0\). The results of Hirst and Hughes in [loc. cit.] essentially confirmed this pattern for theorems stating conditions on the existence of \textit{unique solutions}. The present paper further confirms this pattern for theorems stating conditions on the existence of \textit{finitely many solutions}. For example, the following marriage theorem is equivalent to \(\mathrm{WKL}_0\): A bounded marriage problem \(M=(B,G,R)\) has exactly \(k\) solutions if and only if there is a finite set \(F \subseteq B\) such that \(M\) restricted to \(F\) has exactly \(k\) solutions, each of which extends uniquely to a solution of \(M\).