Feasible combinatorial matrix theory

TL;DR

This paper demonstrates that Konig's Min-Max Theorem can be proven within a weak logical framework with limited induction, making the proof feasible and formalizable in computational terms.

Contribution

It shows that a fundamental combinatorial matrix theorem can be proven with restricted induction, improving the proof's feasibility compared to traditional methods.

Findings

KMM provable in $ ext{LA}$ with $ ext{Sigma}_1^B$ induction

Enables formalization of Min-Max reasoning in feasible frameworks

Supports proof of other combinatorial theorems like Menger's, Hall's, and Dilworth's

Abstract

We show that the well-known Konig's Min-Max Theorem (KMM), a fundamental result in combinatorial matrix theory, can be proven in the first order theory $\LA$ with induction restricted to $\Sigma_1^B$ formulas. This is an improvement over the standard textbook proof of KMM which requires $\Pi_2^B$ induction, and hence does not yield feasible proofs --- while our new approach does. $\LA$ is a weak theory that essentially captures the ring properties of matrices; however, equipped with $\Sigma_1^B$ induction $\LA$ is capable of proving KMM, and a host of other combinatorial properties such as Menger's, Hall's and Dilworth's Theorems. Therefore, our result formalizes Min-Max type of reasoning within a feasible framework.