The Small-Is-Very-Small Principle

TL;DR

This paper establishes the small-is-very-small principle for restricted sequential theories, showing that small witnesses imply very small witnesses, with various consequences for theory extensions, models, and interpretability.

Contribution

It introduces the small-is-very-small principle for restricted sequential theories and explores its implications for theory extensions, models, and interpretability.

Findings

Every restricted, recursively enumerable sequential theory has a finitely axiomatized conservative extension.

Every sequential model has an extension where the intersection of all definable cuts is the natural numbers.

Reflection holds for $\

Abstract

The central result of this paper is the small-is-very-small principle for restricted sequential theories. The principle says roughly that whenever the given theory shows that a property has a small witness, i.e. a witness in every definable cut, then it shows that the property has a very small witness: i.e. a witness below a given standard number. We draw various consequences from the central result. For example (in rough formulations): (i) Every restricted, recursively enumerable sequential theory has a finitely axiomatized extension that is conservative w.r.t. formulas of complexity $\leq n$. (ii) Every sequential model has, for any $n$, an extension that is elementary for formulas of complexity $\leq n$, in which the intersection of all definable cuts is the natural numbers. (iii) We have reflection for $\Sigma^0_2$-sentences with sufficiently small witness in any consistent restricted theory $U$. (iv) Suppose $U$ is recursively enumerable and sequential. Suppose further that every recursively enumerable and sequential $V$ that locally inteprets $U$, globally interprets $U$. Then, $U$ is mutually globally interpretable with a finitely axiomatized sequential theory. The paper contains some careful groundwork developing partial satisfaction predicates in sequential theories for the complexity measure depth of quantifier alternations.