Ultraproducts in abstract categorical logic

TL;DR

This work extends abstract categorical logic to encompass ultraproducts and Łoś's theorem in a quantifier-agnostic manner, enabling model-theoretic methods to operate inside a broad class of logics defined by prop-categories and internal toposes. It introduces filtered semantical systems with sup-generation, coverage, and finiteness conditions, and defines filterable quantifiers and pullbacks to carry ultraproduct constructions through to the abstract setting. The main result is an abstract Łoś's theorem, together with a compactness corollary, proven under the stated structural hypotheses. The framework unifies first-order, higher-order, modal, and coalgebraic logics, and points toward applying abstract model-theoretic tools across diverse categorical logics while keeping the quantifier choice flexible and independent.

Abstract

In a previous publication, we introduced an abstract logic via an abstract notion of quantifier. Drawing upon concepts from categorical logic, this abstract logic interprets formulas from context as subobjects in a specific category, e.g., Cartesian, regular, or coherent categories, Grothendieck, or elementary toposes. We proposed an entailment system formulated as a sequent calculus which we proved complete. Building on this foundation, our current work explores model theory within abstract logic. More precisely, we generalize one of the most important and powerful classical model theory methods, namely the ultraproduct method, and show its fundamental theorem, i.e., Los's theorem. The result is shown as independently as possible of a given quantifier.

Theorems & Definitions (79)

• Definition 2.1: Prop-category
• Remark 2.2
• Definition 2.3: Filtered product
• Proposition 2.4
• proof
• Proposition 2.5
• proof
• Definition 2.6: Filtered category
• Definition 2.7: Filtered colimit
• Definition 2.8: Finitely presentable object