Automated Economic Reasoning
with Mathematica

Casey B. Mulligan, University of Chicago
help.economicreasoning.com

ABSTRACT
(please describe your presentation in 250 words or less)

The Mathematica package TheoryGuru	 lower the costs of applying automated quantifier elimination to economics and statistics.  Many suggested theorems in economics can either be proven, disproven, or even have their hypotheses shown to be inconsistent, automatically via QE.  These theorems may involve symbolic functions, integrals, or vectors.

TheoryGuru accepts the expression of reasoning in the format traditional to the field: as a conclusion to be possibly deduced from a set of assumptions.  It then automatically: checks for errors, parses input, adds standard assumptions, recognizes the theorem as a special cases of Tarski formulas, and makes QE algorithm choices.  Mathematica’s Resolve function eliminates the quantifiers and then TheoryGuru interprets the output and indicates to the user possible next steps.

This presentation demostrates TheoryGuru’s capabilities, which are documented more fully by Mulligan, Davenport, and England (2018) and at help.economicreasoning.com.

Introduction

Load package

Today we will also use some of the “Extras.”

Example browser

The examples are for user convenience, and to illustrate the range of possible applications.  The economicreasoning package reaches conclusions “from scratch” without reference to any pre-programmed example.

Introduction

Template; interpreting output

TheoryGuru[{assume1,assume2,...},hypothesis]

TheoryGuru assembles and, with Resolve, decides 2 nonlinear SAT/SMT problems: existence of examples and existence of counterexamples.

Econometrics example:
Omitted variable bias

Query about the bias of OLS

y, x1, x2, and ϵ are automatically recognized as vectors (from context).
SymbolicRegression is part of the economicreasoning package (extras).

y=x1 β1+x2 β2+ϵ;

olsslopes=Simplify@SymbolicRegression[y,x1,x2]

TheoryGuru[{x1.x1>0,x1.ϵ==0},
First@olsslopes== β1]

Show the variables that were detected

Econometrics example:
Omitted variable bias

Follow up

What else could be assumed to guarantee no bias?

TheorySufficient[]

TheoryGuru[{x1.x1>0,x1.ϵ==0,First@%},First@olsslopes== β1]

A Silver Lining to Inequality?

Below we see that women and men appeared to become more equal in terms of wages, while at the same time wages become less equal among men.  Is this a puzzle? [Source:  Mulligan and Rubinstein (2008); see also this notebook]

Define the conceptual experiment

x increases inequality σ without changing the employment rate p or the average potential wage μw.

DefineExperiment={((\[DifferentialD]p[σ,μR-μw])/(\[DifferentialD]x))==((\[DifferentialD]μw)/(\[DifferentialD]x))==0,((\[DifferentialD]σ)/(\[DifferentialD]x))>0};

SkillImpact=((\[DifferentialD]H[σ,μR-μw])/(\[DifferentialD]x));(* human capital effect of x *)

A Silver Lining to Inequality?

Definitions

f is a symbolic joint probability density function; not pre-programmed.
f is a.k.a. a partially interpreted function (as are dot products or integrals).

p[σ_,meangap_]=(∫_(-∞)^∞)(∫_(-∞)^(σ h-meangap))f[h,r]\[DifferentialD]r\[DifferentialD]h; (* female employment rate *)

H[σ_,meangap_]=(((∫_(-∞)^∞)(∫_(-∞)^(σ h-meangap))h f[h,r]\[DifferentialD]r\[DifferentialD]h)/(p[σ,meangap]));(* average human capital of working women *)

PositiveEmployment=p[σ,μR-μw]>0;

InequalityOntheMargin=(((∫_(-∞)^∞)(h^2)f[h,μw-μR+h σ]\[DifferentialD]h)/((∫_(-∞)^∞)f[h,μw-μR+h σ]\[DifferentialD]h))>((((((∫_(-∞)^∞)h f[h,μw-μR+h σ]\[DifferentialD]h)/((∫_(-∞)^∞)f[h,μw-μR+h σ]\[DifferentialD]h))))^2)∧(∫_(-∞)^∞)f[h,μw-μR+h σ]\[DifferentialD]h>0;

A Silver Lining to Inequality?

Must there be an increase in the skills of working women?

TheoryGuru[{DefineExperiment,PositiveEmployment,InequalityOntheMargin},
SkillImpact>0]

Teaching with Automated QE

Repetition rather than mechanical proof steps

Show TheoryGuru output for a theorem.

Students edit assumptions, hypothesis to examine many related theorems.

A different kind of learning.  Repetition builds intuition.

Calculus is no longer a prerequisite

A calculus prerequisite is a barrier to student participation.

In many cases, calculus is a shortcut based on local linearity.

Computer time is cheap: why take shortcuts?

TheoryBrowser’s library examples includes many nonlocal (“revealed preference”) applications.

Economics QE Bibliography

Mulligan, Casey B. “Automated Economic Reasoning with Quantifier Elimination.” NBER working paper #22922, December 2016.

Mulligan, Casey B. “Quantifier Elimination for Deduction in Econometrics.” NBER working paper #24601, May 2018.

Mulligan, Casey B., James H. Davenport, and Matthew Englamd.  “TheoryGuru: A Mathematica Package to apply Quantifier Elimination Technology to Economics.” Mathematical Software – ICMS 2018.  2018. 

Mulligan, Casey B., Russell Bradford, James H. Davenport, Matthew England and Zak Tonks.  “Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics.” Proceedings of the 3rd International Workshop on Satisfiability Checking and Symbolic Computation. 2018.