A topos for continuous logic

TL;DR

This paper introduces a new ordering for predicates in continuous logic, representing its semantics as a hyperdoctrine and embedding it into a Grothendieck topos, linking logic with category theory.

Contribution

It proposes a novel predicate ordering in continuous logic and embeds its semantics into a topos framework, bridging logic and categorical structures.

Findings

Hyperdoctrine formulation of continuous logic semantics

Embedding into Grothendieck topos

Category of equivalence relations corresponds to complete metric spaces

Abstract

We suggest an ordering for the predicates in continuous logic so that the semantics of continuous logic can be formulated as a hyperdoctrine. We show that this hyperdoctrine can be embedded into the hyperdoctrine of subobjects of a suitable Grothendieck topos. For this embedding we use a simplification of the hyperdoctrine for continuous logic, whose category of equivalence relations is equivalent to the category of complete metric spaces and uniformly continuous maps.