Characterizing when certain logic theories have finite models
A characterization of the finite model property for $ω$-categorical theories
Logic in Computer Science
Summary
Some logical theories always have infinite examples, but others can be understood entirely through finite examples. This paper shows how to tell when a particular kind of logical theory, known for being well-behaved and unique in structure, guarantees that all its implied statements can be satisfied by finite models. By doing this, the authors provide a way to connect deep logical properties to patterns found in families of finite structures and their random expansions. This insight helps understand how larger and more complex finite structures might behave logically.
What this means in practice
- •For database designers: Identify when schema constraints guarantee finite data representations based on logical theory properties.
- •For developers of logic-based ai systems: Design knowledge bases ensuring all entailed facts can be grounded in finite datasets for efficient reasoning.
A theory result. No direct application yet.
Authors
Vera Koponen
Abstract
A first-order theory $T$ has the {\em finite model property} if every first-order sentence that is implied by $T$ has a finite model. We give a characterization of when a complete $ω$-categorical theory $T$ has the finite model property. The characterization makes it possible to transfer stability theoretic results in [29] to certain classes of finite structures. This approach also gives information concerning properties that a sequence of finite ``base structures'' of ever larger size must have in order for its random expansions to a larger vocabulary to have a chance to satisfy a convergence law for first-order logic.