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 on this topic

BFI Working Paper·Jun 18, 2025

Innovator Networks Within the Firm and the Quality of Innovation

Michael Gibbs, Friederike Mengel, and Christoph Siemroth
Topics: Uncategorized
BFI Working Paper·Jun 17, 2025

The Social Desirability Atlas

Leonardo Bursztyn, Ingar K. Haaland, Nicolas Röver, and Christopher Roth
Topics: Uncategorized
BFI Working Paper·Jun 10, 2025

Measuring Markets for Network Goods

Leonardo Bursztyn, Matthew Gentzkow, Rafael Jiménez-Durán, Aaron Leonard, Filip Milojević, and Christopher Roth
Topics: Uncategorized