Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Uniform Preorders and Partial Combinatory Algebras

Jonas Frey

Abstract

Uniform preorders are a class of combinatory representations of Set-indexed preorders that generalize Pieter Hofstra's basic relational objects. An indexed preorder is representable by a uniform preorder if and only if it has as generic predicate. We study the $\exists$-completion of indexed preorders on the level of uniform preorders, and identify a combinatory condition (called 'relational completeness') which characterizes those uniform preorders with finite meets whose $\exists$-completions are triposes. The class of triposes obtained this way contains relative realizability triposes, for which we derive a characterization as a fibrational analogue of the characterization of realizability toposes given in earlier work. Besides relative partial combinatory algebras, the class of relationally complete uniform preorders contains filtered ordered partial combinatory algebras, and it is unclear if there are any others.

Uniform Preorders and Partial Combinatory Algebras

Abstract

Uniform preorders are a class of combinatory representations of Set-indexed preorders that generalize Pieter Hofstra's basic relational objects. An indexed preorder is representable by a uniform preorder if and only if it has as generic predicate. We study the -completion of indexed preorders on the level of uniform preorders, and identify a combinatory condition (called 'relational completeness') which characterizes those uniform preorders with finite meets whose -completions are triposes. The class of triposes obtained this way contains relative realizability triposes, for which we derive a characterization as a fibrational analogue of the characterization of realizability toposes given in earlier work. Besides relative partial combinatory algebras, the class of relationally complete uniform preorders contains filtered ordered partial combinatory algebras, and it is unclear if there are any others.
Paper Structure (9 sections, 12 theorems, 28 equations)

This paper contains 9 sections, 12 theorems, 28 equations.

Table of Contents

  1. The locally ordered category of uniform preorders
  2. Adjunctions of uniform preorders
  3. Cartesian uniform preorders
  4. Existential quantification
  5. Indexed frames
  6. Relational completeness
  7. Ordered partially combinatory algebras
  8. Discreteness
  9. Partial combinatory algebras

Key Result

Lemma 1.6

The $2$-functor $\mathsf{fam}:\mathsf{UOrd}\to\mathsf{IOrd}$ is a local equivalence, and its bi-essential image consists of the indexed preorders which admit a generic predicate. Concretely, if $\EuScript{H}$ is an indexed preorder with generic predicate $\iota\in\EuScript{H}(A)$, then the correspon where $p,q:r\to A$ are the first and second projections as in the diagram.

Theorems & Definitions (34)

  • Definition 1.1
  • Definition 1.2
  • Definition 1.4
  • Remark 1.5
  • Lemma 1.6
  • Lemma 2.1
  • Definition 3.1
  • Lemma 3.2
  • Remark 3.4
  • Definition 4.1
  • ...and 24 more