Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Continuity in Potential Infinite Models

Matthias Eberl

TL;DR

This work develops a topology-free, potential-infinite semantic framework for simple type theory by introducing factor systems and their targets as internally extensible structures. It then models continuity via partial equivalence relations (PERs) and their internal/internal-pointed systems, culminating in a robust function-space construction for PER-sets that preserves limits and embeddings. The key contributions include formal definitions of factor systems, targets/limits, PER-sets, pointed PERs, and a D-continuous function-space theory, along with a demonstration that function-space PER-sets and PER-set function spaces are structurally equivalent. This approach enables a coherent interpretation of infinite processes as indefinitely extensible finite stages, with potential applications to higher-order logic and a non-punctual view of the continuum that integrates with simple type theory.

Abstract

We introduce a model of simple type theory with potential infinite carrier sets. The functions in this model are automatically continuous, as defined in this paper. This notion of continuity does not rely on topological concepts, including domain theoretic concepts, which essentially use actual infinite sets. The model is based on the concept of a factor system, which generalizes direct and inverse systems. A factor system is basically an extensible set indexed over a directed set of stages, together with a predecessor relation between object states at different stages. The function space, when considered as a factor system, expands simultaneously with its elements. On the one hand, the space is subdivided more and more, on the other hand, the elements increase and are defined more and more precisely. In addition, a factor system allows the construction of limits that are part of its expansion process and not outside of it. At these limits, elements are indefinitely large or small, which is a contextual notion and a substitute for elements that are infinitely large or small (points). This dynamic and contextual view is consistent with an understanding of infinity as a potential infinite.

Continuity in Potential Infinite Models

TL;DR

This work develops a topology-free, potential-infinite semantic framework for simple type theory by introducing factor systems and their targets as internally extensible structures. It then models continuity via partial equivalence relations (PERs) and their internal/internal-pointed systems, culminating in a robust function-space construction for PER-sets that preserves limits and embeddings. The key contributions include formal definitions of factor systems, targets/limits, PER-sets, pointed PERs, and a D-continuous function-space theory, along with a demonstration that function-space PER-sets and PER-set function spaces are structurally equivalent. This approach enables a coherent interpretation of infinite processes as indefinitely extensible finite stages, with potential applications to higher-order logic and a non-punctual view of the continuum that integrates with simple type theory.

Abstract

We introduce a model of simple type theory with potential infinite carrier sets. The functions in this model are automatically continuous, as defined in this paper. This notion of continuity does not rely on topological concepts, including domain theoretic concepts, which essentially use actual infinite sets. The model is based on the concept of a factor system, which generalizes direct and inverse systems. A factor system is basically an extensible set indexed over a directed set of stages, together with a predecessor relation between object states at different stages. The function space, when considered as a factor system, expands simultaneously with its elements. On the one hand, the space is subdivided more and more, on the other hand, the elements increase and are defined more and more precisely. In addition, a factor system allows the construction of limits that are part of its expansion process and not outside of it. At these limits, elements are indefinitely large or small, which is a contextual notion and a substitute for elements that are infinitely large or small (points). This dynamic and contextual view is consistent with an understanding of infinity as a potential infinite.
Paper Structure (22 sections, 20 theorems, 45 equations, 2 figures)

This paper contains 22 sections, 20 theorems, 45 equations, 2 figures.

Table of Contents

  1. Introduction
  2. A Motivating Example
  3. Some Observations
  4. Structure of the Paper
  5. Factor Systems and their Limits
  6. Factor Systems
  7. Targets and Limits
  8. Stronger Properties for $\mathfrak{D}$
  9. Sets with Families of PERs
  10. Approximating Equality and the Internal System
  11. Pointed Families of PERs
  12. The Internal System for Pointed Families of PERs
  13. Convergence and Completeness
  14. Total Equivalence Relations and PER-Sets
  15. The Function Space of PER-Sets
  16. ...and 7 more sections

Key Result

Lemma 3.2

Let $(\mathcal{M},\stackrel{p}{\longmapsto})$ be a target for a prefactor system $(\mathcal{M}_\mathcal{I},\stackrel{p}{\mapsto})$, then $(\mathcal{M},\approx_\mathcal{I})$, with $\approx_\mathcal{I}$ as defined in (perpmap), is a $\mathfrak{D}$-set.

Figures (2)

  • Figure 1: Overview over the structures.
  • Figure 2: Convergent sequences in systems and limits.

Theorems & Definitions (49)

  • Example 2.1
  • Definition 3.1: $\mathfrak{D}$-set
  • Lemma 3.2: Target structure of a prefactor system
  • proof
  • Example 3.3
  • Definition 3.4
  • Example 3.5
  • Definition 3.6: Internal system
  • Lemma 3.7: Internal system of a $\mathfrak{D}$-set
  • proof
  • ...and 39 more