The computational strength of matchings in countable graphs

TL;DR

This paper explores the logical strength of a criterion for perfect matchings in countable graphs, linking it to foundational subsystems of reverse mathematics and highlighting its significance for understanding the relationship between graph theory and logic.

Contribution

It analyzes the proof-theoretic strength of Steffens' criterion and related theorems, establishing their equivalence or relation to the big five subsystems of reverse mathematics.

Findings

Variants of the theorems are equivalent or closely related to the big five subsystems.

The existence of matchings in countable graphs relates to foundational logical systems.

The results deepen understanding of the interplay between graph theory and reverse mathematics.

Abstract

In a 1977 paper, Steffens identified an elegant criterion for determining when a countable graph has a perfect matching. In this paper, we will investigate the proof-theoretic strength of this result and related theorems. We show that a number of natural variants of these theorems are equivalent, or closely related, to the ``big five'' subsystems of reverse mathematics. The results of this paper explore the relationship between graph theory and logic by showing the way in which specific changes to a single graph-theoretic principle impact the corresponding proof-theoretical strength. Taken together, the results and questions of this paper suggest that the existence of matchings in countable graphs provides a rich context for understanding reverse mathematics more broadly.