The size of a formula as a measure of complexity

TL;DR

This paper introduces a refined Ehrenfeucht-Fra"{sse9} game that enables more precise measurement of the size of formulas needed to express properties in propositional and first-order logic.

Contribution

It presents two versions of a new game that better distinguish formula sizes, advancing the measurement of logical complexity.

Findings

The game characterizes propositional formula size.

The game applies to first-order logic.

It allows finer distinctions in logical expressiveness.

Abstract

We introduce a refinement of the usual Ehrenfeucht-Fra\"{\i}ss\'e game. The new game will help us make finer distinctions than the traditional one. In particular, it can be used to measure the size formulas needed for expressing a given property. We will give two versions of the game: the first version characterizes the size of formulas in propositional logic, and the second version works for first-order predicate logic.