A Complete Bounded Theory with Unbounded Types

TL;DR

This paper explores the relationship between the complexity of theories and their types, revealing that bounded theories can have unbounded types in the first-order logic setting.

Contribution

It demonstrates that, contrary to expectations, a bounded, orall_1-axiomatizable theory can possess unbounded types, challenging previous assumptions.

Findings

Bounded theories can have unbounded types in first-order logic.

The complexity of a theory's types does not necessarily match its axiomatization complexity.

Contrasts with the infinitary logic case where complexity aligns more closely.

Abstract

One measure of the complexity of a first-order theory, and similarly a type, is the complexity of the formulas required to axiomatize it. We say a theory is bounded if there is an axiomatization involving only $\forall_n$-formulas for some finite $n$, and unbounded otherwise. One might expect bounded theories to have only bounded types. In fact, an analogue holds in infinitary logic, where the complexity of a Scott sentence roughly agrees with the complexity of the most complicated automorphism orbit. Our main result, however, shows this is not the case in the first-order setting: Namely, there can be a bounded theory, in fact $\forall_1$-axiomatizable, which has unbounded types.