Feasible combinatorial matrix theory

Original · EN

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 with induction restricted to Σ₁ᵇ formulas. This is an improvement over the standard textbook proof of KMM which requires Π₂ᵇ induction, and hence does not yield feasible proofs --- while our new approach does. is a weak theory that essentially captures the ring properties of matrices; however, equipped with Σ₁ᵇ induction 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.