Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Note on Los's Theorem for Kripke-Joyal Semantics

Marc Aiguier, Romain Pascual

TL;DR

This article uses the categorical version of Los's theorem to obtain a proof of the compactness theorem for Kripke-Joyal semantics and shows that the extension entails its set-theoretic version.

Abstract

Los's theorem, also known as the fundamental result of ultraproducts, states that the ultraproduct over a family of structures for the same language satisfies a first-order formula if and only if the set of indices for which the structures satisfy the formula belongs to the underlying ultrafilter. The associated notion of satisfaction is the Tarskian one via the elements of the set-theoretic structure that allow interpreting the formula. In the context of topoi, Kripke-Joyal semantics extends Tarski's notion to categorical logic. In this article, we propose to extend Los's theorem to first-order structures on elementary topoi for Kripke-Joyal semantics. We also show that the extension entails its set-theoretic version. As is customary, we use the categorical version of Los's theorem to obtain a proof of the compactness theorem for Kripke-Joyal semantics.

A Note on Los's Theorem for Kripke-Joyal Semantics

TL;DR

This article uses the categorical version of Los's theorem to obtain a proof of the compactness theorem for Kripke-Joyal semantics and shows that the extension entails its set-theoretic version.

Abstract

Los's theorem, also known as the fundamental result of ultraproducts, states that the ultraproduct over a family of structures for the same language satisfies a first-order formula if and only if the set of indices for which the structures satisfy the formula belongs to the underlying ultrafilter. The associated notion of satisfaction is the Tarskian one via the elements of the set-theoretic structure that allow interpreting the formula. In the context of topoi, Kripke-Joyal semantics extends Tarski's notion to categorical logic. In this article, we propose to extend Los's theorem to first-order structures on elementary topoi for Kripke-Joyal semantics. We also show that the extension entails its set-theoretic version. As is customary, we use the categorical version of Los's theorem to obtain a proof of the compactness theorem for Kripke-Joyal semantics.

Paper Structure

This paper contains 19 sections, 17 theorems, 9 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Notations
  4. Subobjects and Heyting Algebras
  5. Elementary Topoi
  6. Filters, Filtered Products, and Filtered Colimits
  7. Set-theoretic Filters and Ultrafilters
  8. Filtered Products in Categories
  9. Locally Finitely Presentable Category
  10. Noetherian Objects
  11. Categorical Semantics for First-Order Logic (FOL)
  12. The Category of Sigma-Structures
  13. Kripke-Joyal Semantics
  14. Internal Logic of a Topos
  15. Filtered Products in Sigma-Structures and Łoś's Theorem
  16. ...and 4 more sections

Key Result

Theorem 1.1

Let $(\mathcal{M}_i)_{i\in I}$ be an $I$-indexed family of nonempty $\Sigma$-structures, and let $F$ be an ultrafilter on $I$. Let $\prod_F \mathcal{M}$ be the ultraproduct of $(\mathcal{M}_i)_{i\in I}$ with respect to $F$. Since each $\mathcal{M}_i$ is nonempty, the ultraproduct $\prod_F \mathcal{M

Theorems & Definitions (40)

  • Theorem 1.1: Łoś's Theorem los_quelques_1955
  • Definition 2.1: Filtered product
  • Definition 2.2: Filtered category
  • Definition 2.3: Filtered colimit
  • Definition 2.4: Finitely presentable object
  • Definition 2.5: Locally finitely presentable category adamek_locally_1994
  • Definition 2.6: Noetherian object
  • Proposition 2.7
  • proof
  • Definition 3.1: $\Sigma$-structure
  • ...and 30 more