On logical parameterizations and functional representability in local set theories

Abstract

There is a well-known inclusion ${\iota }_{\mathcal{E}}$ of a topos $\mathcal{E}$ in the linguistic topos $\mathcal{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 $\mathcal{T}(S)$ to $\mathcal{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 }_{\mathcal{T}(S)}$ parameterizes $\mathcal{T}({\eta }_S)$ in such a way that syntactic $S$-functions are represented by themselves in $\Sigma$.

arXiv comment28 pages. New Introductory text