I am study the book Introduction to Linear Optimization by Bertsimas and Tsitsiklis. The proof of strong duality (Theorem 4.4)
Theorem 4.4 (Strong duality) If a linear programming problem has an optimal solution, so does its dual, and the respective optimal costs are equal.
uses the fact that the simplex method has finite termination using the lexicographic pivoting rule, takes an optimal BFS $x$, and constructs a dual feasible solution $p'=c_B'B^{-1}$ that has the same cost as the primal optimal solution.
I wonder why the simplex method is used in this proof. Why not just use the fact that a standard form LP which has an optimal solution must have an optimal BFS? Is it because the reduced costs are not guaranteed to be nonnegative?
The issue of nonnegative reduced cost is likely the reason, yes.
It does not take too much work to show (without the simplex method) that if a linear program has an optimal solution, then it has an optimal basic feasible solution. This is still a nontrivial proof, and using the simplex method to prove strong duality sidesteps it.
However, once we have the optimal basic feasible solution, there are two challenges with the reduced costs:
This is not to say that strong duality cannot be proven without the simplex method. The usual alternate route is to use Farkas's lemma: if a system of linear inequalities has no solution, then some linear combination of those inequalities (with nonnegative coefficients, so that the inequalities are preserved) yields a contradiction.
To prove Farkas's lemma, we can use Fourier-Motzkin elimination to try to solve the system of linear inequalities: this is a much slower algorithm than the simplex method, but it is also easier to handle theoretically.