The equivalence of finite-path perfect matching and ATR0\mathsf{ATR}_0

Let athsfPMathsf{PM} denote the perfect matching principle, and let extFinitePathPMext{Finite Path }\mathsf{PM} denote its restriction to finite-path instances. Let peratornameATR0peratorname{\mathsf{ATR}}_0 and peratornameRCA0peratorname{\mathsf{RCA}}_0 be the indicated systems of reverse mathematics.

Finite-path perfect matching conjecture. extFinitePathPMext{Finite Path }\mathsf{PM} is equivalent to peratornameATR0peratorname{\mathsf{ATR}}_0 over peratornameRCA0peratorname{\mathsf{RCA}}_0.

The paper proves that finite-path perfect matching is close in strength to peratornameATR0peratorname{\mathsf{ATR}}_0 and asks whether it implies that system, as well as whether peratornameATR0peratorname{\mathsf{ATR}}_0 proves finite-path perfect matching or perfect matching. The supplied text does not resolve these questions.

Sources & referencesView supporting material

Primary source

Stephen Flood, Matthew Jura, Oscar Levin and Tyler Markkanen, “The computational strength of matchings in countable graphs”, arXiv:2006.11334 (2020).

Progress summary

Never refreshed

Nothing recorded yet. Refresh searches the literature and the public web for attempts on this problem, and writes the first summary here.

Solutions 0

No solutions have been posted yet.