Title: Linear Logical Economics: Proof-Theoretic Foundations of Resource Consumption Abstract: This paper reconstructs the foundations of neoclassical microeconomics using Jean-Yves Girard's Linear Logic (1987), addressing the fundamental mismatch between classical logic—where knowledge is non-consumable via structural rules of contraction and weakening—and economic reality, where resources are consumed. By adopting a resource-sensitive logical framework, we provide a unified proof-theoretic formulation for consumer theory, producer theory, general equilibrium, and game theory. Key economic concepts are reinterpreted as logical connectives: the multiplicative tensor () as asset portfolios, linear implication () as market transactions, additive internal choice (\&) as opportunity costs, and additive external choice () as uncertainty. We demonstrate that utility maximization and cost minimization correspond to proof search algorithms, and that market equilibrium is equivalent to the normalization of proof nets (Cut-Elimination). This approach establishes "resource consumption" not as an external assumption, but as a syntactic necessity of the economic logic itself.
Takayuki Shoji (Mon,) studied this question.