ON THE STRENGTH OF KÖNIG’S DUALITY THEOREM FOR COUNTABLE BIPARTITE GRAPHS

STEPHEN G. SIMPSON

September 18, 1992

Published in Journal of Symbolic Logic, 59, 1994, pp. 113-123.

Abstract. Let CKDT be the assertion that, for every countably infinite bipartite graph G, there exist a vertex covering C of G and a matching M in G such that C consists of exactly one vertex from each edge in M. (This is a theorem of Podewski and Steffens [12].) Let ATR_{0} be the subsystem of second order arithmetic with arithmetical transfinite recursion and restricted induction. Let RCA_{0} be the subsystem of second order arithmetic with recursive comprehension and restricted induction. We show that CKDT is provable in ATR_{0}. Combining this with a result of Aharoni, Magidor and Shore [2], we see that CKDT is logically equivalent to the axioms of ATR_{0}, the equivalence being provable in RCA_{0}.

1. Introduction

A bipartite graph is an ordered triple G = (X, Y, E) such that X and Y are sets, X ∩ Y = ∅, and E ⊆ {{x, y} : x ∈ X, y ∈ Y }. The vertices of G are the elements of X ∪ Y. The edges of G are the elements of E.

A covering of G is a set C ⊆ X ∪ Y such that every edge of G has a vertex in C, i.e. we have C ∩ e ≠ ∅ for all e ∈ E.

A matching in G is a pairwise disjoint set M ⊆ E. Here pairwise disjointness means that no two edges in M have a common vertex, i.e. we have e_{1} ∩ e_{2} = ∅ for all e_{1}, e_{2} ∈ M such that e_{1} ≠ e_{2}.

For any set S we use |S| to denote the cardinality of S, i.e. the number of elements in S. If G is any bipartite graph and C is any covering of G and M is any matching in G, then clearly |C| ≥ |M|. The König duality theorem [7] asserts that, for any

1991 Mathematics Subject Classification. 03B30, 03F35, 05D15. Key words and phrases. matchings, coverings, bipartite, graph, reverse mathematics, second

order arithmetic, subsystems.

Research partially supported by NSF Grant DMS 9002072. The referee provided some useful suggestions.

finite bipartite graph G, there exist a covering C of G and a matching M in G such that |C| = |M|. In other words,

min{|C| : C is a covering of G} = max{|M| : M is a matching in G} .

Definition 1.1. For any bipartite graph G, a König covering of G is an ordered pair (C, M) such that C is a covering of G, M is a matching in G, and C consists of exactly one vertex from each edge of M. (The last condition means that C ⊆ ⋃ M and |C ∩ e| = 1 for each e ∈ M.)

Clearly if (C, M) is a König covering of G then |C| = |M|. König [7] showed that every finite bipartite graph has a König covering. From this the König duality theorem follows immediately.

Podewski, Steffens and Aharoni extended the König duality theorem to infinite bipartite graphs. In order to make such extensions meaningful, they considered König coverings. Podewski and Steffens [12] showed that every countably infinite bipartite graph has a König covering. Aharoni [1] showed that every uncountable bipartite graph has a König covering. We refer to the Podewski–Steffens theorem (respectively Aharoni’s theorem) as the König duality theorem for countable (respectively uncountable) bipartite graphs.

Aharoni, Magidor and Shore [2] considered the following logical or foundational question: Which set existence axioms are needed to prove the König duality theorem for countable bipartite graphs? Aharoni, Magidor and Shore obtained a partial answer to this question, but they did not answer it completely. The purpose of this paper is to finish the work which was begun by Aharoni, Magidor and Shore.

The general question of which set existence axioms are needed to prove specific mathematical theorems is of basic importance for the foundations of mathematics. This general question has been studied fruitfully in the context of subsystems of second order arithmetic. For this purpose, five of the most important subsystems of second order arithmetic are RCA_{0}, WKL_{0}, ACA_{0}, ATR_{0}, and Π_{1}^{1}-CA_{0}. It is known that these five systems are of strictly increasing strength as regards their ability to prove mathematical theorems. Moreover, for many particular mathematical theorems, it turns out that one can determine the weakest natural subsystem of second order arithmetic in which the given mathematical theorem is provable. Such results are established by showing that the given mathematical theorem is logically equivalent to the axioms of the specified subsystem of second order arithmetic, the equivalence being proved in a weaker system. Consider for example the Bolzano–Weierstrass theorem: every bounded sequence of real numbers has a convergent subsequence. It is known that the weakest subsystem of second order arithmetic in which the Bolzano–Weierstrass theorem is provable is ACA_{0}. This is established by showing that the Bolzano-Weierstrass theorem is logically equivalent to the axioms of ACA_{0}, the equivalence being proved in the weaker system RCA_{0}.

For a survey of subsystems of second order arithmetic and their role in foundational studies, see my article [16]. A fuller treatment will appear in [17]. For additional results and open problems concerning logical and foundational aspects of combinatorics, see the articles in Logic and Combinatorics [8], especially [3].

Aharoni, Magidor and Shore [2] made a major contribution to the foundational program of [16]. They obtained two important results. First, the König duality theorem for countable bipartite graphs (ı.e. CKDT) is provable in Π_{1}^{1}-CA_{0}. Second, CKDT logically implies the axioms of ATR_{0}, this implication being provable in the weak system RCA_{0}. (Aharoni, Magidor and Shore also obtained results concerning logical aspects of some other infinitistic variants of the König duality theorem.)

The main result of the present paper is that the König duality theorem for countable bipartite graphs is provable in ATR_{0}. This is established in Section 3 below. Combining this with the results of Aharoni, Magidor and Shore, we see that CKDT is logically equivalent to the axioms of ATR_{0}, the equivalence being provable in RCA_{0}. Thus ATR_{0} is the weakest natural subsystem of second order arithmetic in which CKDT is provable.

2. Subsystems of Second Order Arithmetic

In this section we present some background material concerning ATR_{0} and related systems. We present little more than what is needed for our main result, the provability of CKDT in ATR_{0}. For a broad survey of subsystems of second order arithmetic, see [16]. For detailed information on ATR_{0}, see [6], [14], [15], [16], and [17].

All of the systems which we shall consider are first-order theories in the language of second order arithmetic. This is a first-order language with two sorts of variables: number variables i, j, k, m, n, …, and set variables U, V, W, X, Y, Z, …. Number variables are intended to range over the set of natural numbers ω = {0, 1, 2, … }, while set variables are intended to range over subsets of ω. Numerical terms are built up as usual from number variables, the constant symbols 0 and 1, and the binary operations of addition and multiplication. The atomic formulas of the language are t_{1} = t_{2}, t_{1} < t_{2}, and t_{1} ∈ X, where t_{1} and t_{2} are numerical terms and X is any set variable. Formulas are built up from atomic formulas by means of propositional connectives, number quantifiers ∀n and ∃n where n is any number variable, and set quantifiers ∀X and ∃X where X is any set variable. A sentence is a formula with no free variables. The universal closure of a formula is the sentence obtained from the formula by prefixing it with universal quantifiers on all of its free number variables and free set variables. Note that X = Y is not a formula of our language. Rather, equality for sets is defined by extensionality:

X = Y ≡ ∀n (n ∈ X ↔ n ∈ Y) .

All of the systems which we shall consider include the Basic Arithmetical Axioms and the Restricted Induction Axiom, expressing elementary properties of the natural number system. The Basic Arithmetical Axioms are the universal closures of the formulas n + 1 ≠ 0, m + 1 = n + 1 → m = n, m + 0 = m, m + (n + 1) = (m + n) + 1, m · 0 = 0, m · (n + 1) = m · n + m, ∼ m < 0, and m < n + 1 ↔ (m < n ∨ m = n). The Restricted Induction Axiom is the universal closure of

(0 ∈ X ∧ ∀n (n ∈ X → n + 1 ∈ X)) → ∀n (n ∈ X) .

The Comprehension Scheme consists of the universal closures of all formulas of the form

∃X ∀n (n ∈ X ↔ φ(n)) (1)

where φ(n) is any formula in which X does not occur freely. The idea here is that the given instance of the Comprehension Scheme asserts the existence of an explicitly defined set X = {n : φ(n)} consisting of all natural numbers n such that φ(n) holds. Second order arithmetic, also called Z_{2}, is the first-order theory whose axioms are the Basic Arithmetical Axioms, the Restricted Induction Axiom, and the Comprehension Scheme.

A theorem of Z_{2} is any sentence which is deducible from the axioms of Z_{2}. A subsystem of Z_{2} is any first-order theory T in the language of Z_{2} whose axioms are included in the theorems of Z_{2}. A theorem of T is any sentence which is deducible from the axioms of T. Theorems of T are also said to be provable in T. At all times we employ the usual axioms and deduction rules of classical first-order logic, with equality for the numerical sort. The intended model of the language of Z_{2} is

(P (ω), ω, +, ·, 0, 1, <, =)

where (ω, +, ·, 0, 1, <, =) is the standard natural number system and P (ω) is the power set of ω. Clearly all of the axioms of Z_{2} are true in the intended model. If T is any subsystem of Z_{2}, a model of T is any structure M such that all of the axioms of T are true in M. Here we are employing the well known Tarski truth definition for models of a first-order theory. By the Gödel completeness theorem for first-order logic, the theorems of T are precisely the sentences which are true in all models of T.

An ω-model of T is a model M of T whose numerical part is the standard natural number system. Thus we have

M = (S, ω, +, ·, 0, 1, <, =)

where S ⊆ P (ω). We shall sometimes identify M with S.

An arithmetical formula is a formula which contains no set quantifiers. Note that an arithmetical formula may contain free set variables, as well as free and bound number variables and number quantifiers. A Σ_{1}^{1} (respectively Π_{1}^{1}) formula is one of the form ∃X θ (respectively ∀X θ) where X is any set variable and θ is any arithmetical formula. More generally, for k ∈ ω, a formula is said to be Σ_{k}^{1} (respectively Π_{k}^{1}) if it is of the form ∃X_{1} ∀X_{2} … X_{k} θ (respectively ∀X_{1} ∃X_{2} … X_{k} θ) where θ is arithmetical.

Thus a Σ_{k}^{1} or Π_{k}^{1} formula consists of k alternating set quantifiers followed by a formula containing no set quantifiers. In a Σ_{k}^{1} formula the initial set quantifier is existential, while in a Π_{k}^{1} formula it is universal (assuming k > 0).

The Arithmetical Comprehension Scheme consists of all instances of the Comprehension Scheme (1) in which the formula φ(n) is arithmetical.

Definition 2.1. ACA_{0} is the subsystem of Z_{2} whose axioms are the Basic Arithmetical Axioms, the Restricted Induction Axiom, and the Arithmetical Comprehension Scheme.

The letters ACA stand for arithmetical comprehension axiom. More generally, for k ∈ ω, we define Π_{k}^{1}-CA_{0} to be the subsystem of Z_{2} consisting of ACA_{0} plus all instances of the Comprehension Scheme (1) in which the formula φ(n) is Π_{k}^{1}. One could define Σ_{k}^{1}-CA_{0} similarly, but nothing new is obtained, since Σ_{k}^{1}-CA_{0} is easily seen to be logically equivalent to Π_{k}^{1}-CA_{0}. Note also that Π_{0}^{1}-CA_{0} is the same as ACA_{0}. It can be shown that, for all k ∈ ω, Π_{k+1}^{1}-CA_{0} is stronger than Π_{k}^{1}-CA_{0}. In particular, Π_{1}^{1}-CA_{0} is stronger than ACA_{0}.

Π_{1}^{1}-CA_{0} and ACA_{0} are two of the most important subsystems of Z_{2}. There are at least two other important subsystems, RCA_{0} and WKL_{0}, both of which are weaker than ACA_{0}. Although RCA_{0} and WKL_{0} are of great interest, we shall not define these systems here because they are not essential to our purpose.

When reasoning within a subsystem of Z_{2}, we use the symbol ℕ to denote the set of natural numbers within the system, i.e. ℕ = {n : n = n}. Thus ∀n (n ∈ ℕ) is provable in ACA_{0}. We introduce the numerical pairing function

(m, n) = (m + n)^{2} + m .

The usual properties such as

∀i ∀j ∀m ∀n ((i, j) = (m, n) ↔ (i = m ∧ j = n))

can be proved as theorems of ACA_{0}. We shall also need a set pairing function,

(X, Y) = X ⊕ Y = {2n : n ∈ X} ∪ {2n + 1 : n ∈ Y }

and again the usual properties can be proved in ACA_{0}.

Reasoning within ACA_{0} and using the numerical pairing function, we may view any set Y ⊆ ℕ as encoding a countable sequence of sets ⟨(Y)_{n} : n ∈ ℕ⟩ where

(Y)_{n} = {m : (m, n) ∈ Y } .

The Countable Choice Scheme consists of the universal closures of all formulas of the form

(∀n ∃X φ(n, X)) → ∃Y ∀n φ(n, (Y)_{n}) (2)

where φ(n, X) is any formula in which Y does not occur freely.

Definition 2.2. Σ_{1}^{1}-AC_{0} is the subsystem of Z_{2} consisting of ACA_{0} plus all instances of the Countable Choice Scheme ( 2) in which the formula φ(n, X) is Σ_{1}^{1}.

The letters AC stand for axiom of choice. It can be shown that the system Σ_{1}^{1}-AC_{0} is intermediate in strength between ACA_{0} and Π_{1}^{1}-CA_{0}.

Still reasoning within ACA_{0} and using the numerical pairing function, we may view any set X ⊆ ℕ as encoding a binary relation R ⊆ ℕ × ℕ, where (i R j) ≡ (i, j) ∈ X. We therefore say that X is a linear ordering of ℕ, abbreviated LO(X), if ∀i ∀j ∀k (((i, j) ∈ X ∧ (j, k) ∈ X) → (i, k) ∈ X) and ∀i (i, i) ∉ X and ∀i ∀j (i = j ∨ (i, j) ∈ X ∨ (j, i) ∈ X). We say that X is a well ordering of ℕ, abbreviated WO(X), if LO(X) and

∀Y ((∀j (∀i ((i, j) ∈ X → i ∈ Y) → j ∈ Y)) → ∀j (j ∈ Y)) . (3)

Let φ(n, j, W) be any formula with two distinguished free number variables n and j and a distinguished free set variable W. If Z is a set and X is a well ordering of ℕ, we say that Z is obtained by transfinite recursion along X via φ(n, j, W), abbreviated Rec(X, φ, Z), if

∀j ∀n (n ∈ (Z)_{j} ↔ φ(n, j, (Z)_{X}^{j})))

where

(Z)_{X}^{j} = {(m, i) : m ∈ (Z)_{i} ∧ (i, j) ∈ X} .

The idea here is that, for each j, the set (Z)_{j} is defined recursively in terms of the sets (Z)_{i} for all i preceding j in the well ordering X. The Transfinite Recursion Scheme consists of the universal closures of all formulas of the form

∀X (WO(X) → ∃Z Rec(X, φ, Z)) (4)

where Z does not occur freely in φ(n, j, W). Thus the Transfinite Recursion Scheme asserts the existence of sets defined by transfinite recursion along arbitrary well orderings of ℕ.

Definition 2.3. ATR_{0} is the subsystem of Z_{2} consisting of ACA_{0} plus all instances of the Transfinite Recursion Scheme ( 4) in which the formula φ is arithmetical.

The letters ATR stand for arithmetical transfinite recursion. It can be shown that ATR_{0} is intermediate in strength between Σ_{1}^{1}-AC_{0} and Π_{1}^{1}-CA_{0}. The system ATR_{0} was introduced by Friedman ([5], [4]), who also emphasized its importance for the foundations of mathematics. It is known [16] that many mathematical theorems are provable in ATR_{0} and indeed logically equivalent to ATR_{0}, the equivalence being provable in ACA_{0} (in fact in RCA_{0}). For example, this is the case for the open Ramsey theorem (see [6] and [17]).

An important technique for proving mathematical theorems within ATR_{0} is the use of inner models ([6], [10], [17]). Within ATR_{0}, any subset Z of ℕ determines a countable set S = {(Z)_{n} : n ∈ ℕ} of subsets of ℕ. This set of sets S may be identified with a countable ω-model M = (S, ℕ, +, ·, 0, 1, <, =) and in this way Z may be regarded as a code of the inner model M. In particular, for any set W ⊆ ℕ, we have W ∈ M if and only if ∃n(W = (Z)_{n}). Given such a countable coded ω-model M, we can carry out the Tarski truth definition within ATR_{0} to obtain a full satisfaction predicate for M. Here formulas of the language of Z_{2} are identified with their Gödel numbers. Thus within ATR_{0} we may speak of countable coded ω-models of T, where T is any recursively axiomatized subsystem of Z_{2}.

The following result from [17] will be used to prove our main theorem, in Section 3 below.

Lemma 1. The following is provable in ATR_{0}. For any set W ⊆ ℕ, there exists a countable coded ω-model M of Σ_{1}^{1}-AC_{0} such that W ∈ M.

Proof. We shall use the formalization within ATR_{0} of some facts and techniques from recursive function theory and hyperarithmetical theory [13]. For details of the formalization within ATR_{0}, see [4], [6], and [17].

We shall use the arithmetical formula

WO(X, Z) ≡ LO(X) ∧ ∀Y (Y Turing reducible to Z → Ind(X, Y)) ,

where ∀Y Ind(X, Y) is the formula (3). Trivially we have

∀X (WO(X) ↔ ∀Z WO(X, Z)) .

Reasoning within ATR_{0}, fix a set W ⊆ ℕ. Consider the arithmetical formula

η(W, X, Z) ≡ WO(X, Z) ∧ ∀j ((Z)_{j} = Turing jump of (W ⊕ X) ⊕ (Z)_{X}^{j}) .

By arithmetical transfinite recursion we have

∀X (WO(X) → ∃Z η(W, X, Z)) .

On the other hand, the formula WO(X) is complete Π_{1}^{1} and hence not equivalent to any Σ_{1}^{1} formula (see [13], Chapter 16). In particular, WO(X) is not equivalent to the Σ_{1}^{1} formula ∃Z η(W, X, Z). These considerations imply that there exist sets X and Z such that η(W, X, Z) ∧ ∼WO(X). Fix such an X and Z.

Using WO(X, Z) and the fact that X is Turing reducible to Z, it is easy to see that the linear ordering X has the following properties: there is a least element, and any element other than the greatest element (if there is one) has an immediate successor. Using ∼WO(X), let J ⊆ ℕ be such that Ind(X, J) fails, and put I = {j : ∀i ((i, j) ∈ X → i ∈ J)}. Then clearly I is a cut in X, i.e. we have ∃i ∃j (i ∈ I ∧ j ∉ I) and ∀i ∀j ((i ∈ I ∧ j ∉ I) → (i, j) ∈ X)) and ∀i (i ∈ I → ∃k ((i, k) ∈ X ∧ k ∈ I)) and ∀j (j ∉ I → ∃k ((k, j) ∈ X ∧ k ∉ I)).

By arithmetical comprehension, there exists a countable coded ω-model M consisting of all sets A such that A is Turing reducible to (Z)_{i} for some i ∈ I. Clearly W ∈ M and X ∈ M. It is also clear that M is closed under ⊕ and Turing reducibility and the Turing jump operator. From this it follows by Post’s theorem ([13], Chapter 14) that M is an ω-model of ACA_{0}.

We claim that M is an ω-model of Σ_{1}^{1}-AC_{0}. To see this, let φ(n, U) be any Σ_{1}^{1} formula. Let n_{1}, …, n_{k}, U_{1}, …, U_{m} be the free variables of φ(n, U) other than n and U. Fix a_{1}, …, a_{k} ∈ ℕ and A_{1}, …, A_{m} ∈ M and suppose that M satisfies ∀n ∃U φ̄(n, U), where

φ̄(n, U) ≡ φ(n, U)[n_{1}/a_{1}, …, n_{k}/a_{k}, U_{1}/A_{1}, …, U_{m}/A_{m}] .

Let us write

φ(n, U) ≡ ∃V θ(n, U, V)

where θ(n, U, V) is arithmetical, and put

θ̄(n, U, V) ≡ θ(n, U, V)[n_{1}/a_{1}, …, n_{k}/a_{k}, U_{1}/A_{1}, …, U_{m}/A_{m}] .

Then M satisfies ∀n ∃U ∃V θ̄(n, U, V). It follows that for each n ∈ ℕ there exists i ∈ I such that

(5) ∃U ∃V (θ̄(n, U, V) ∧ U and V are Turing reducible to (Z)_{i}) .

Hence by WO(X, Z) we have that for each n ∈ ℕ there exists a least such i with respect to the linear ordering of ℕ given by X. Define f : ℕ → ℕ by f(n) = the least i ∈ ℕ with respect to the linear ordering X such that (5) holds. Since f(n) ∈ I for all n ∈ ℕ, it follows that f is Turing reducible to (Z)_{j} for any j ∉ I. Hence by WO(X, Z) there exists k ∈ ℕ such that k is the least upper bound, with respect to the linear ordering X, of the range of f. Since f(n) ∈ I for all n ∈ ℕ, it follows that k ∈ I. Thus we have a set (Z)_{k} ∈ M such that ∀n ∃U ∃V (θ̄(n, U, V) ∧ U and V are Turing reducible to (Z)_{k}). We can now use arithmetical comprehension within M to find a set T ∈ M such that ∀n θ̄(n, ((T)_{n})_{0}, ((T)_{n})_{1}). Putting Y = {(m, n) : ((m, 0), n) ∈ T }, we obtain Y ∈ M such that ∀n θ̄(n, (Y)_{n}, ((T)_{n})_{1}). Thus M satisfies ∃Y ∀n ∃V θ̄(n, (Y)_{n}, V), i.e. ∃Y ∀n φ̄(n, (Y)_{n}). Thus M is an ω-model of Σ_{1}^{1}-AC_{0} and the proof of Lemma 1 is complete.

Remark. The assertion considered in the previous lemma (“for all W there exists a countable coded ω-model of Σ_{1}^{1}-AC_{0} containing W ”) is in fact equivalent to ATR_{0} over RCA_{0}. This is shown in [17].

3. Proof of the Main Theorem

The purpose of this section is to prove our main result:

Theorem 1. The König duality theorem for countable bipartite graphs (i.e. CKDT) is provable in ATR_{0}.

In order to prove Theorem 1, the following notions will be useful. Let G = (X, Y, E) be a bipartite graph. For y ∈ Y, the neighborhood of y in G is

N_{G}(y) = {x ∈ X : {x, y} ∈ E} .

For A ⊆ X, the demand of A with respect to G is

D_{G}(A) = {y ∈ Y : N_{G}(y) ⊆ A} .

For A ⊆ X and B ⊆ Y, a matching of A into B is a matching M such that X ∩ (⋃ M) = A and Y ∩ (⋃ M) ⊆ B. In this case we write

M : A → B

and, for x ∈ A, M(x) = the unique y such that {x, y} ∈ M. Thus

M = {{x, M(x)} : x ∈ A} .

If M is any matching in G and if v and w are vertices of G, an M-alternating path from v to w is a sequence of vertices v = v_{0}, v_{1}, …, v_{n} = w such that {v_{i}, v_{i+1}} ∈ E for all i < n, {v_{i}, v_{i+1}} ∈ M for all odd i < n, and {v_{i}, v_{i+1}} ∉ M for all even i < n.

We now begin the proof of Theorem 1. We reason in ATR_{0}. Let G = (X, Y, E) be a countable bipartite graph. We shall prove in ATR_{0} that a König covering of G exists.

By Lemma 1, there exists a countable coded ω-model M of Σ_{1}^{1}-AC_{0} such that G ∈ M. Fix such an M. Let A^{∗} be the union of all sets A ⊆ X such that A ∈ M and in M there is a matching F : A → D_{G}(A). Note that A^{∗} is definable over M. Hence A^{∗} exists by arithmetical comprehension, using a code of M as a parameter.

Lemma 2. There exists a matching F^{∗} : A^{∗} → D_{G}(A^{∗}).

Proof. By arithmetical comprehension using a code of M as a parameter, we can find an enumeration ⟨(A_{n}, F_{n}) : n ∈ ℕ⟩ of all pairs (A, F) ∈ M such that F is a matching of A into D_{G}(A). Then A^{∗} = ⋃{A_{n} : n ∈ ℕ}. For x ∈ A^{∗} define F^{∗}(x) = F_{n}(x) where n = the least n such that x ∈ A_{n}. To see that F^{∗} is oneto-one, suppose F^{∗}(x_{1}) = F^{∗}(x_{2}) = y. For i = 1, 2 put n_{i} = the least n such that x_{i} ∈ A_{n}. Then F_{n_{1}}(x_{1}) = F_{n_{2}}(x_{2}) = y. Hence y ∈ D_{G}(A_{n_{1}}) ∩ D_{G}(A_{n_{2}}). Hence x_{1}, x_{2} ∈ A_{n_{1}} ∩ A_{n_{2}}. It follows that n_{1} = n_{2}. Hence x_{1} = x_{2}. Thus F^{∗} is a matching, and clearly F^{∗} : A^{∗} → D_{G}(A^{∗}). This proves the lemma.

Put X^{∗} = X − A^{∗} and Y^{∗} = Y − D_{G}(A^{∗}). We shall need to consider certain subgraphs of G of the form

G′ = G − {x_{0}, …, x_{n−1}, y_{0}, …, y_{n−1}}

where x_{0}, …,x_{n−1} ∈ X^{∗} and y_{0}, …, y_{n−1} ∈ Y^{∗}. For any such graph G′ we shall use the notation G′ = (X′, Y′, E′) where X′ = X − {x_{0}, …, x_{n−1}}, Y′ = Y − {y_{0}, …, y_{n−1}}, and E′ = E ∩ {{x, y} : x ∈ X′, y ∈ Y′}. Note that for any such graph G′ we have G′ ∈ M.

Let G′ be a subgraph of G as above. We say that G′ is good if there is no set A ⊆ X′ such that A ∈ M and in M there is a matching F : A → D_{G′}(A) such that

(D_{G′}(A) − ⋃ F ) ∩ Y^{∗} ≠ ∅ .

Lemma 3. G is good.

Proof. Let A ⊆ X be such that A ∈ M and in M there is a matching F : A → D_{G}(A). Then A ⊆ A^{∗}. Hence D_{G}(A) ⊆ D_{G}(A^{∗}). Hence by the definition of Y^{∗} we have D_{G}(A) ∩ Y^{∗} = ∅. This shows that G is good.

Lemma 4. Suppose G′ is good. Suppose x ∈ X′ ∩ X^{∗} and y ∈ Y′ ∩ Y^{∗} are such that G′ − {x, y} is not good. Then there exists A′ ⊆ X′ such that x ∈ A′ and A′ ∈ M and in M there is a matching F′ : A′ → D_{G′}(A′) such that y ∉ ⋃ F′.

Proof. Since G′ − {x, y} is not good, we can find a set A ⊆ X′ − {x}, A ∈ M, a matching F : A → D_{G′−{x,y}}(A), F ∈ M, and a vertex y^{∗} ∈ (D_{G′−{x,y}}(A)−⋃ F)∩Y^{∗}.

We claim that there exists an F -alternating path in G′ from y^{∗} to x. To see this, let S be the set of all x′ ∈ X′ − {x} such that there exists an F -alternating path in G′ − {x, y} from y^{∗} to x′, and let T be the set of all y′ ∈ Y′ − {y} such that there exists an F -alternating path in G′ − {x, y} from y^{∗} to y′. For any x′ ∈ S we clearly have F (x′) ∈ T. Thus F_{S} = {{x′, F (x′)} : x′ ∈ S} is a matching of S into T. Note also that S, T, and F_{S} belong to M. Moreover, for any y′ ∈ T we clearly have N_{G′−{x,y}}(y′) ⊆ S. Thus T ⊆ D_{G′−{x,y}}(S). However, since G′ is good and y^{∗} ∈ (T − ⋃ F_{S}) ∩ Y^{∗}, we cannot have T ⊆ D_{G′}(S). Hence there must exist y′ ∈ T such that {x, y′} ∈ E′. Let y^{∗} = y′_{0}, x′_{0}, y′_{1}, x′_{1}, …,y′_{n} = y′ be an F -alternating path in G′ − {x, y} from y^{∗} to y′. Then y^{∗} = y′_{0}, x′_{0}, y′_{1}, x′_{1}, …, y′_{n}, x′_{n} = x is an F -alternating path in G′ from y^{∗} to x. This proves the claim.

Put A′ = A ∪ {x}. Then obviously D_{G′−{x,y}}(A) ⊆ D_{G′}(A′). Using our F - alternating path y^{∗} = y′_{0}, x′_{0}, y′_{1}, x′_{1}, …, y′_{n}, x′_{n} = x as above, put

F′ = (F − {{x′_{i}, y′_{i+1}} : i < n}) ∪ {{x′_{i}, y′_{i}} : i ≤ n} .

Since F is a matching of A into D_{G′−{x,y}}(A), and since x, y^{∗} ∉ ⋃ F and y^{∗} ∈ D_{G′−{x,y}}(A), it follows that F′ is a matching of A′ into D_{G′−{x,y}}(A). Therefore, F′ is a matching of A′ into D_{G′}(A′). It is also clear that x ∈ A′, A′ ∈ M, F′ ∈ M, and y ∉ ⋃ F′. This completes the proof of Lemma 4.

Lemma 5. Suppose that G′ is good. Then for all y ∈ Y′∩Y^{∗} there exists x ∈ X′∩X^{∗} such that {x, y} ∈ E′ and G′ − {x, y} is good.

Proof. Fix y ∈ Y′ ∩Y^{∗} and assume for a contradiction that there is no x ∈ X′ ∩X^{∗} such that {x, y} ∈ E′ and G′ − {x, y} is good.

We claim that for all x ∈ N_{G′}(y) there exists (A′, F′) ∈ M such that x ∈ A′, A′ ⊆ X′, F′ is a matching of A′ into D_{G′}(A′), and y ∉ ⋃ F′. We prove this claim by considering two cases, x ∈ A^{∗} and x ∉ A^{∗}. If x ∉ A^{∗}, then x ∈ X′ ∩ X^{∗} and by assumption G′ − {x, y} is not good, so the claim follows by Lemma 4. If x ∈ A^{∗}, then by the definition of A^{∗} we can find a set A ⊆ X, A ∈ M, x ∈ A, and a matching F : A → D_{G}(A), F ∈ M. Then A ⊆ A^{∗} ⊆ X′ and D_{G}(A) ⊆ D_{G}(A^{∗}) ⊆ Y′, hence D_{G}(A) ⊆ D_{G′}(A). Moreover y ∈ Y^{∗} = Y − D_{G}(A^{∗}), hence y ∉ D_{G}(A), hence y ∉ ⋃ F. Thus in this case our claim holds with (A′, F′) = (A, F). This completes the proof of the claim.

Working within M, let ⟨x′_{n} : n ∈ ℕ⟩ be an enumeration of the vertices in N_{G′}(y). The above claim implies that for all n ∈ ℕ there exists (A′, F′) ∈ M such that x′_{n} ∈ A′, A′ ⊆ X′, F′ is a matching of A′ into D_{G′}(A′), and y ∉ ⋃ F′. Applying the Σ_{1}^{1} Countable Choice Scheme within M, we obtain a sequence ⟨(A′_{n}, F′_{n}) : n ∈ ℕ⟩ ∈ M such that for all n ∈ ℕ we have x′_{n} ∈ A′_{n}, A′_{n} ⊆ X′, F′_{n} is a matching of A′_{n} into D_{G′}(A′_{n}), and y ∉ ⋃ F′_{n}.

Put A = ⋃{A′_{n} : n ∈ ℕ}. Then N_{G′}(y) = {x′_{n} : n ∈ ℕ} ⊆ A, i.e. y ∈ D_{G′}(A). Still working within M, define F (x) for all x ∈ A by F (x) = F′_{n}(x) where n = the least n such that x ∈ A′_{n}. To see that F is one-to-one, suppose F (x′) = F (x′′) = y′. Let n′ = the least n such that x′ ∈ A′_{n}, and let n′′ = the least n such that x′′ ∈ A′_{n}. Then F′_{n′}(x′) = F′_{n′′}(x′′) = y′. Hence y′ ∈ D_{G′}(A′_{n′})∩D_{G′}(A′_{n′′}). Hence x′, x′′ ∈ A′_{n′} ∩A′_{n′′}. It follows that n′ = n′′. Hence x′ = x′′. Thus F is a matching. Clearly F : A → D_{G′}(A) and we also clearly have A ∈ M, F ∈ M, and y ∈ (D_{G′}(A) − ⋃ F) ∩ Y^{∗}. This contradicts the assumption that G′ is good. The proof of Lemma 5 is complete.

We are now ready to finish the proof of Theorem 1. Still reasoning within ATR_{0}, fix a one-to-one enumeration y_{0}, y_{1}, …, y_{n}, … of all the vertices in Y^{∗}. The idea of this part of the proof is to apply Lemma 5 repeatedly to obtain a sequence of vertices x_{0}, x_{1}, …, x_{n}, … in X^{∗} so that

H = {{x_{0}, y_{0}}, {x_{1}, y_{1}}, …, {x_{n}, y_{n}}, … }

will be a matching. To begin, since G is good and y_{0} ∈ Y^{∗}, we can apply Lemma 5 with G′ = G and y = y_{0} to obtain x_{0} ∈ X^{∗} such that {x_{0}, y_{0}} ∈ E and G − {x_{0}, y_{0}} is good. Next, since G−{x_{0}, y_{0}} is good and y_{1} ∈ Y^{∗}−{y_{0}}, we can apply Lemma 5 with G′ = G − {x_{0}, y_{0}} and y = y_{1} to obtain x_{1} ∈ X^{∗} − {x_{0}} such that {x_{1}, y_{1}} ∈ E and G − {x_{0}, y_{0}, x_{1}, y_{1}} is good. At stage n of the construction, we assume inductively that G − {x_{0}, y_{0}, …, x_{n−1}, y_{n−1}} is good. Since y_{n} ∈ Y^{∗} − {y_{0}, …, y_{n−1}}, we can apply Lemma 5 with G′ = G − {x_{0}, y_{0}, …, x_{n−1}, y_{n−1}} and y = y_{n} to obtain x_{n} ∈ X^{∗} − {x_{0}, …, x_{n−1}} such that {x_{n}, y_{n}} ∈ E and G − {x_{0}, y_{0}, …, x_{n}, y_{n}} is good. The inductive construction of the sequence x_{0}, x_{1}, …, x_{n}, … is definable over M. Thus H exists by arithmetical comprehension, using a code of M as a parameter.

Clearly H is a matching, X ∩ (⋃ H) ⊆ X^{∗}, and Y ∩ (⋃ H) = Y^{∗}. In addition, Lemma 2 provides a matching F^{∗} : (X − X^{∗}) → (Y − Y^{∗}). Thus F^{∗} ∪ H is again a matching. Since D_{G}(X − X^{∗}) = Y − Y^{∗}, it follows that ((X − X^{∗}) ∪ Y^{∗}, F^{∗} ∪ H) is a König covering of G. This completes the proof of Theorem 1.

References

1. R. Aharoni, König’s duality theorem for infinite bipartite graphs, Journal of the London Mathematical Society (Second Series), 29, 1984, pp. 1-12.

2. R. Aharoni, M. Magidor, and R. A. Shore, On the strength of König’s duality theorem for infinite bipartite graphs, Journal of Combinatorial Theory (B), 54, 1992, pp. 257-290.

3. A. R. Blass, J. L. Hirst, and S. G. Simpson, Logical analysis of some theorems of combinatorics and topological dynamics, in [8], pp. 125-156.

4. H. Friedman, Subsystems of set theory and analysis, Ph. D. Thesis, M. I. T., 1967, 83 pp.

5. H. Friedman, Systems of second order arithmetic with restricted induction I, II (abstracts), Journal of Symbolic Logic, 41, 1976, pp. 557-559.

6. H. M. Friedman, K. McAloon, and S. G. Simpson, A finite combinatorial principle which is equivalent to the 1-consistency of predicative analysis, in [11], pp. 197-230.

7. D. König, Theorie der Endlichen und Unendlichen Graphen, Akademische Verlagsgesellschaft, Leipzig, 1936, reprinted by Chelsea, New York, 1950, 258 pp.

8. Logic and Combinatorics, edited by S. G. Simpson, Contemporary Mathematics, American Mathematical Society, Providence, 1987, 384 pp.

9. Logic Colloquium ’80 , edited by D. van Dalen, D. Lascar and J. Smiley, North-Holland, Amsterdam, 1982, 342 pp.

10. A. Marcone, Borel quasi-orderings in subsystems of second-order arithmetic, Annals of Pure and Applied Logic, 54, 1991, pp. 265-291.

11. Patras Logic Symposion, edited by G. Metakides, North-Holland, Amsterdam, 1982, 391 pp.

12. K. P. Podewski and K. Steffens, Injective choice functions for countable families, Journal of Combinatorial Theory (B), 21, 1976, pp. 40-46.

13. H. Rogers, Jr., Theory of Recursive Functions and Effective Computability, McGraw-Hill, New York, 1967, reprinted by M.I.T. Press, Cambridge, 1987, 482 pp.

14. S. G. Simpson, Set-theoretic aspects of ATR_{0}, in [9], pp. 255-271.

15. S. G. Simpson, Σ_{1}^{1} and Π_{1}^{1} transfinite induction, in [9], pp. 239-253.

16. S. G. Simpson, Subsystems of Z_{2} and Reverse Mathematics, in [18], pp. 432-446.

17. S. G. Simpson, Subsystems of Second Order Arithmetic, in preparation.

18. G. Takeuti, Proof Theory (Second Edition), North-Holland, Amsterdam, 1987, 490 pp.

Department of Mathematics, Pennsylvania State University, University Park, State College, PA 16802

E-mail address: simpson@math.psu.edu