# Reasoning about Social Choice and Games in Monadic Fixed-Point Logic

## TL;DR

This paper proposes using monadic fixed-point logic with counting as a natural language to specify and analyze properties of improvement graphs in social choice and game theory, enabling efficient model checking.

## Contribution

It introduces a novel application of monadic fixed-point logic with counting to model and verify properties of improvement graphs across social choice and game-theoretic domains.

## Key findings

- Logic can specify properties of improvement graphs
- Model checking is efficient in graph size
- Applicable to various social choice and game scenarios

## Abstract

Whether it be in normal form games, or in fair allocations, or in voter preferences in voting systems, a certain pattern of reasoning is common. From a particular profile, an agent or a group of agents may have an incentive to shift to a new one. This induces a natural graph structure that we call the improvement graph on the strategy space of these systems. We suggest that the monadic fixed-point logic with counting, an extension of monadic first-order logic on graphs with fixed-point and counting quantifiers, is a natural specification language on improvement graphs, and thus for a class of properties that can be interpreted across these domains. The logic has an efficient model checking algorithm (in the size of the improvement graph).

---
Source: https://tomesphere.com/paper/1907.09100