Infinitary Logic Has No Expressive Efficiency Over Finitary Logic

TL;DR

The paper proves that infinitary logic does not yield greater quantifier-efficiency than finitary logic: any finitary formula equivalent to an infinitary formula with $n$ quantifier alternations is itself equivalent to a finitary formula with the same $n$. It introduces a forcing framework based on elementary extensions (strong and weak forcing) to analyze when infinitary formulas transfer truth across models, and shows that such formulas are definable by force expressions built from finitary components. The main theorem establishes an interpolation-like result for $L_{\omega_1,\omega}$ and $L_{\infty,\omega}$: if an infinitary $\exists_n$ (or $\forall_n$) formula is equivalent to a finitary one across all models of a countable theory, then the two are equivalent to a finitary $\exists_n$ (or $\forall_n$) formula in all models of the theory. The work connects forcing, elementary amalgamation, and Malitz interpolation to characterize which infinitary formulas preserve under extensions and how this constrains their quantifier structure, with implications for the expressiveness and definability of infinitary languages.

Abstract

We can measure the complexity of a logical formula by counting the number of alternations between existential and universal quantifiers. Suppose that an elementary first-order formula $\varphi$ (in $\mathcal{L}_{ω,ω}$) is equivalent to a formula of the infinitary language $\mathcal{L}_{\infty,ω}$ with $n$ alternations of quantifiers. We prove that $\varphi$ is equivalent to a finitary formula with $n$ alternations of quantifiers. Thus using infinitary logic does not allow us to express a finitary formula in a simpler way.

Theorems & Definitions (55)

• Theorem 1.1
• Theorem 1.2
• Theorem 1.3
• Theorem 3.1
• proof
• Lemma 3.2
• proof
• Lemma 3.3
• proof
• Example 3.4