Many theorems in economics can be proven (and hypotheses shown to be false) with “quantifier elimination.” Results from real algebraic geometry such as Tarski’s quantifier elimination theorem and Collins’ cylindrical algebraic decomposition algorithm are applicable because the economic hypotheses, especially those that leave functional forms unspecified, can be represented as systems of multivariate polynomial (sic) equalities and inequalities. The symbolic proof or refutation of economic hypotheses can therefore be achieved with an automated technique that involves no approximation and requires no problem-specific information beyond the statement of the hypothesis itself. This paper also discusses the computational complexity of this kind of automated economic reasoning, its implementation with Mathematica and REDLOG software, and offers several examples familiar from economic theory.

More Research From These Scholars

BFI Working Paper May 10, 2018

TheoryGuru: A Mathematic Package to apply Quantifier Elimination Technology to Economics

Casey Mulligan, James H. Davenport, Matthew England
Topics:  Health care
BFI Working Paper Jul 27, 2017

Wedges, Labor Market Behavior, and Health Insurance Coverage Under the Affordable Care Act

Casey Mulligan, Trevor S. Gallen
Topics:  Health care
BFI Working Paper Oct 21, 2020

An Analysis of Vice President Biden’s Economic Agenda: The Long Run Impacts of Its Regulation, Taxes, and Spending

Timothy Fitzgerald, Kevin Hassett, Cody Kallen, Casey Mulligan