On logical parameterizations and functional representability in local set theories

TL;DR

This paper explores the relationships between local set theories and their linguistic topoi, proving isomorphisms between certain functors and analyzing logical parameterizations to enhance the representation of functions.

Contribution

It establishes the isomorphism between two functors from local set theories to their linguistic topoi and applies logical parameterization to improve function representation.

Findings

Two functors from local set theories to their linguistic topoi are isomorphic.

Logical parameterization allows syntactic functions to be self-represented in the internal language.

The study clarifies the structure of local set theories within topos-theoretic frameworks.

Abstract

There is a well-known inclusion $\iota_\mathscr{E}$ of a topos $\mathscr{E}$ in the linguistic topos $\mathscr{T}(\Sigma)$ of its internal language $\Sigma$ that proves both toposes to be equivalent. There is also a canonical translation $\eta_S$ for any local set theory $S$ into the local set theory $\Sigma$ of its linguistic topos. Starting from a local set theory, this yields two a priori distinct inclusions from $\mathscr{T}(S)$ to $\mathscr{T}(\Sigma)$. Herein, these two functors are proved to be isomorphic. Furthermore, the concept of logical parameterization is investigated and then applied to see that $\iota_{\mathscr{T}(S)}$ parameterizes $\mathscr{T}(\eta_S)$ in such a way that syntactic $S$-functions are represented by themselves in $\Sigma$.