DROPS

Document

DOI: 10.4230/LIPIcs.TYPES.2025.14

Functional Representability in Local Set Theories

Authors: Enrique Ruiz Hernández and Pedro Solórzano

Published in: LIPIcs, Volume 384, 31st International Conference on Types for Proofs and Programs (TYPES 2025)

Abstract

In general local set theories (LST), there is an incomplete representability as (x↦τ) for syntactic functions, i.e. those given by descriptions of the form ∀ x∃!yγ, for some formula γ. The well-known equivalence theorem establishes among other things that it is possible to produce a well-termed local set theory that extends any given LST. However, the natural translation between the corresponding languages still does not guarantee strict functional representability, but only up to isomorphisms. In this report, natural isomorphisms that are compatible with reasoning internally in the original LST are made explicit and explored in more generality. The internal translation along them is exhibited to be compatible with all logical operations; syntactic functions naturally represent themselves in a robust way as described in the main results.

Cite as

Enrique Ruiz Hernández and Pedro Solórzano. Functional Representability in Local Set Theories. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 14:1-14:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{ruizhernandez_et_al:LIPIcs.TYPES.2025.14,
  author =	{Ruiz Hern\'{a}ndez, Enrique and Sol\'{o}rzano, Pedro},
  title =	{{Functional Representability in Local Set Theories}},
  booktitle =	{31st International Conference on Types for Proofs and Programs (TYPES 2025)},
  pages =	{14:1--14:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-441-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{384},
  editor =	{Nordvall Forsberg, Fredrik and McKinna, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.14},
  URN =		{urn:nbn:de:0030-drops-270323},
  doi =		{10.4230/LIPIcs.TYPES.2025.14},
  annote =	{Keywords: local set theories, function symbols, categorical logic}
}

Search Results

Documents authored by Ruiz Hernández, Enrique

Functional Representability in Local Set Theories

Abstract

Cite as

Thanks for your feedback!

Could not send message