Higher-Order Decision Theory

Abstract

This paper investigates a surprising relationship between decision theory and proof theory. Using constructions originating in proof theory based on higher-order functions, so called quantifiers and selection functions, we show that these functionals model choice behavior of individual agents. Our framework is expressive, it captures classical theories such as utility functions and preference relations but it can also be used to faithfully model abstract goals such as coordination. It is directly implementable in functional programming languages. Lastly, modeling an agent with selection functions and quantifiers is modular and thereby allows to seamlessly combine agents bridging decision theory and game theory.