% =====================================================================
\section{Duality and certificates}\label{sec:duality}
% =====================================================================

Duality theorems assert the existence of a \emph{certificate}: a dual solution, a separating hyperplane, a vertex
cover, a cut. They are, formally, existence theorems, and the existence of a certificate behaves like the existence
of an optimal solution: cheap in finite dimensions, expensive when the certificate is an infinite object chosen
among infinitely many candidates.

\subsection{Finite-dimensional duality}\label{subsec:lp}

Finite linear programming is the base case. With real data it is not computable in any uniform sense: solving a
bounded feasible system of linear inequalities, and finding a Nash equilibrium of a bimatrix game, are both Weihrauch
equivalent to $\pr{AoUC}^\ast_{[0,1]}$, the finite parallelization of all-or-unique choice (for linear
inequalities \cite[Theorems 37 and 38]{Pauly2010Nash} with \cite[Proposition 7.60]{BrattkaGherardiPauly2021}; for
Nash equilibria \cite[Corollary 40]{Pauly2010Nash} and \cite[Theorem 8.5]{BrattkaGherardiPauly2021}), and no
Banach--Mazur computable map produces
maximizers of linear programs with computable data \cite{LeeBocheKutyniok2023}. In Bishop's constructive
mathematics, Farkas' lemma as an exclusive alternative is equivalent to $\LPO$ \cite{BergerSvindland2022Farkas}.
Classical reverse mathematics is kinder. We did not find the following statement in the literature.

\begin{theorem}\label{thm:lp-rca}
$\RCA$ proves linear programming strong duality: for all $m,n$ and all real $A\in\R^{m\times n}$, $b\in\R^m$,
$c\in\R^n$, if $\{x\ge0:Ax\le b\}$ and $\{y\ge0:A^\top y\ge c\}$ are nonempty, then there are $x^\ast$ and $y^\ast$
in them with $c^\top x^\ast=b^\top y^\ast$. Consequently $\RCA$ proves von Neumann's minimax theorem for real
matrix games of every size.
\end{theorem}

\begin{proof}[Proof sketch]
\Cref{app:lp} gives the details.
Write the primal in equality form with slack variables, $[A\ I]\,(x,s)=b$. First obtain the signs of the $b_i$ (by
the comprehension step described below) and multiply the rows with $b_i<0$ by $-1$; Phase~I then adds $m$ artificial
variables and minimizes their sum. For each phase let $M$ be the bordered matrix formed by the constraint matrix
of that phase, the right-hand side, and the cost row of that phase. For a basis $B$, every entry of the simplex
tableau, including the reduced costs and the objective value, is a quotient $\mu/\Delta_B$ of minors of $M$, where
$\Delta_B\neq0$ is the basis determinant. Every test that the two-phase simplex method with Bland's rule
\cite{Bland1977} performs is therefore the sign of a minor, or of an expression $\mu_1\mu_2-\mu_3\mu_4$ in minors
(a ratio test, after multiplying out positive denominators; ties are tests ``$=0$''). Let $(v_i)_{i<N}$ be the finite list
of all these reals, for both phases; its length $N$ is bounded by an explicit function of $m$ and $n$.

The only non-constructive step is the following. The reals $v_i$ are computed from the data by explicit
polynomial expressions, so the sequence $(v_i)_{i<N}$ exists in $\RCA$ and ``$v_i>0$'' is $\Sigma^0_1$
uniformly in $i$. By bounded $\Sigma^0_1$ comprehension, which is provable in $\RCA$ \cite[II.3]{Simpson2009SOSOA}, the
finite sets $\{i<N:v_i>0\}$ and $\{i<N:v_i<0\}$ exist, so $\RCA$ has the complete sign pattern $\sigma$ of
$(v_i)$ as a finite object. The simplex method can now be run symbolically on $\sigma$: each tableau is represented
by its basis, and each decision is read off $\sigma$. Because $\sigma$ is the true sign pattern, this symbolic run is
a genuine run of the simplex method on the real data. Bland's anticycling argument is a finite combinatorial argument
about the run, valid in every ordered field and formalizable with $\Sigma^0_1$ induction, so each phase stops after at
most $\binom{n+2m}{m}$ pivots. At the end of Phase~I the optimal value is $0$, since the primal is feasible, and
artificial variables that remain basic at level zero are pivoted out, which is possible because $[A\ I]$ has rank
$m$. Phase~II cannot report unboundedness, since by weak duality any dual feasible $y$ bounds the objective. So it
stops at an optimal basis $B$, where Cramer's rule gives $x^\ast$ and $y^{\ast\top}=c_B^\top B^{-1}$ as explicit
quotients of minors with non-zero denominators. Non-negative reduced costs say that $y^\ast$ is dual feasible, and
$c^\top x^\ast=c_B^\top B^{-1}b=b^\top y^\ast$ is an algebraic identity between explicitly given reals. Nothing
beyond $\Sigma^0_1$ induction and bounded $\Sigma^0_1$ comprehension is used. For the minimax theorem, shift the
payoff matrix by a rational constant that makes all entries positive and use the standard linear programming
formulation of the game; the reduction is uniform in the size.
\end{proof}

The proof makes the three calibrations of finite duality fit together. Reverse mathematics, which has classical
logic, obtains the finitely many signs it needs for free; constructive mathematics must assume them (whence
$\LPO$); and the Weihrauch degree measures how much discontinuous information about signs a uniform algorithm
needs, which is a finite parallelization of a principle strictly below $\LPO$. We expect that the same method,
applied to Lemke--Howson pivoting \cite{LemkeHowson1964} with lexicographic degeneracy resolution, shows that $\RCA$
proves the existence of Nash equilibria of bimatrix games of every size, but we have not written out the details. For
games with three or more players,
whose equilibria can be irrational algebraic numbers of high degree, \cref{prop:tarski} gives the statement for
each fixed format, the uniform statement is provable in $\WKL$ via Brouwer's theorem, and the exact strength is
open (\cref{prob:uniform-n}). Berger and Svindland note that their constructive separation theorem and fundamental
theorem of asset pricing can also be proved in $\RCA$ \cite[Remark 2]{BergerSvindland2016FTAP}.

\subsection{Separation and Hahn--Banach}\label{subsec:separation}

In infinite dimensions, certificates of optimality are continuous linear functionals, and their existence is
the Hahn--Banach theorem. Over $\RCA$, the Hahn--Banach theorem for separable Banach spaces (with
$\norm{\tilde f}\le1$, not $=\norm f$) is equivalent to $\WKL$ \cite{BrownSimpson1986}, and so are the separation of
an open convex set from a disjoint separably closed convex set and the strict separation of two disjoint open
convex sets \cite[Theorem 4.4]{HumphreysSimpson1999}. Strict separation of a compact convex set from a disjoint
separably closed convex set is equivalent to $\ACA$, already in $\R^2$ \cite[Theorem 5.1]{HumphreysSimpson1999}:
the difficulty is not the dimension but the coding: $\RCA$ cannot prove that a set given as the closure of a
sequence is closed in the coded sense, and this is where arithmetical comprehension enters. The existence of the norm of a functional, which is the value of an optimization problem, is
again $\ACA$ \cite[Theorem 13.4]{AvigadSimic2006}. In the Weihrauch lattice the Hahn--Banach theorem is equivalent to
$\WKLp$ \cite{GherardiMarcone2009,BrattkaGherardi2011JSL}, and in Bishop's mathematics it is equivalent to $\LLPO$
\cite{Ishihara1990HahnBanach}.

These results resonate with a familiar experience in convex analysis: duality theorems are cheap when a constraint
qualification provides an interior point (open sets, Slater's condition) and delicate when it does not. We
conjecture that the logical counterpart of this experience is the gap between $\WKL$ and $\ACA$ that the separation
theorems exhibit; making this precise for Lagrange and Fenchel duality is \cref{prob:duality}.

\subsection{Infinite combinatorial optimization}\label{subsec:combinatorial}

Combinatorial optimization on countable structures provides the highest calibrations of all, and the most
instructive. \Cref{tab:combinatorial} collects them.

\begin{table}[t]
\centering
\small
\begin{tabularx}{\linewidth}{@{}Xll@{}}
\toprule
Principle (countable version) & Strength over $\RCA$ & Source \\
\midrule
Matroid basis, decidable dependence (greedy algorithm) & $\RCA$ & \cite{HirstMummert2017} \\
Hall's theorem, bounded marriage problems & $\WKL$ & \cite{Hirst1990} \\
Hall's theorem, each boy knows finitely many girls & $\ACA$ & \cite{Hirst1990} \\
Hall's theorem under the $B$-bounded Hall condition & $\RCA$ (sequential: $\ACA$) & \cite{FujiwaraHiguchiKihara2014} \\
Dilworth's theorem (width $k$), Mirsky's theorem & $\WKL$ & \cite{Hirst1987,CenzerRemmel2005} \\
Stable marriage: highly bounded and effectively listed / listed / ordered & $\WKL$ / $\ACA$ / $\ATR$ & \cite{CenzerRemmel2005} \\
Shortest paths; minimum spanning trees (bounded weight) & $\ACA$ & \cite{CloteHirst1998} \\
Bases of countable vector spaces; e-matroid bases & $\ACA$ & \cite{FriedmanSimpsonSmith1983,HirstMummert2017} \\
Perfect matchings (Steffens), locally finite / bounded & $\ACA$ / $\WKL$ & \cite{FloodJuraLevinMarkkanen2022} \\
K\H{o}nig's duality theorem (bipartite graphs) & $\ATR$ & \cite{AharoniMagidorShore1992,Simpson1994} \\
Extended K\H{o}nig duality; extended Menger theorem & $\PiCA$ & \cite{AharoniMagidorShore1992,Shafer2012} \\
Menger's theorem (countable graphs) & between $\ATR$ and $\mathsf{TLPP}_0$ & \cite{Shafer2012,Towsner2013} \\
\bottomrule
\end{tabularx}
\caption{Reverse mathematics of combinatorial optimization on countable structures.}
\label{tab:combinatorial}
\end{table}

Three features of the table deserve comment. First, the role of a \emph{bounding function} (a function bounding
the neighbours of each vertex, or the preferences of each agent) is exactly the role of compactness in analysis:
with it, existence is $\WKL$; without it, $\ACA$. Second, for matchings the step from $\ACA$ to $\ATR$ happens at
\emph{duality}: Hall's theorem asserts only a matching, while K\H{o}nig's theorem asserts a matching and a cover that
certify each other, and Aharoni, Magidor and Shore built a computable bipartite graph all of whose K\H{o}nig covers
are above every computable iterate of the Turing jump \cite{AharoniMagidorShore1992}. In the Weihrauch lattice,
K\H{o}nig's theorem is arithmetically equivalent to the two-sided problem $\pr{ATR}_2$ \cite[Section 9]{Goh2019KDT}. A
primal--dual pair is a far more rigid object than either half. (Stable marriage reaches $\ATR$ as well, but only in
its ``ordered'' form, which encodes the comparability of well-orderings \cite{CenzerRemmel2005}.) Third,
the greedy algorithm is the combinatorial analogue of convexity: when it applies (matroids with decidable
dependence), existence costs nothing.

Several natural cells are empty: countable max-flow/min-cut \cite{AharoniBergerGeorgakopoulosPerlsteinSpruessel2011},
matroid intersection for countable matroids \cite{Joo2021}, and the exact strength of Menger's theorem, which
is open \cite{Shafer2012,Towsner2013}. Each of them generalizes K\H{o}nig's theorem, so any formalization strong
enough to imply it is at least $\ATR$.