LMU Munich, Theresienstr. 39, 80333 Munich,
Germanymatthias.eberl@mail.dehttps://orcid.org/0000-0002-2410-3747 Matthias
Eberl <ccs2012> <concept>
<concept_id>10003752.10003753.10003754.10003733</concept_id>
<concept_desc>Theory of computation Lambda calculus</concept_desc>
<concept_significance>500</concept_significance> </concept> <concept>
<concept_id>10003752.10003790.10003800</concept_id> <concept_desc>Theory of
computation Higher order logic</concept_desc>
<concept_significance>500</concept_significance> </concept> <concept>
<concept_id>10003752.10003790.10011740</concept_id> <concept_desc>Theory of
computation Type theory</concept_desc>
<concept_significance>500</concept_significance> </concept> <concept>
<concept_id>10003752.10010124.10010131.10010133</concept_id>
<concept_desc>Theory of computation Denotational semantics</concept_desc>
<concept_significance>500</concept_significance> </concept> </ccs2012>
[500]Theory of computation Lambda calculus [500]Theory of computation Higher
order logic [500]Theory of computation Type theory [500]Theory of computation
Denotational semantics Delia Kesner, Eduardo Hermo Reyes, and Benno van den
Berg 3 29th International Conference on Types for Proofs and Programs (TYPES
2023) TYPES 2023 TYPES 2023 June 12-16, 2023 ETSInf, Universitat Politècnica
de València, Spain 303 6

# A Reflection Principle for Potential Infinite Models of Type Theory

Matthias Eberl

###### Abstract

Denotational models of type theory, such as set-theoretic, domain-theoretic,
or category-theoretic models use (actual) infinite sets of objects in one way
or another. The potential infinite, seen as an extensible finite, requires a
dynamic understanding of the infinite sets of objects. It follows that the
type $nat$ cannot be interpreted as a set of all natural numbers,
$[\\![nat]\\!]=\mathbb{N}$, but as an increasing family of finite sets
$\mathbb{N}_{i}=\\{0,\dots,i-1\\}$. Any reference to $[\\![nat]\\!]$, either
by the formal syntax or by meta-level concepts, must be a reference to a
(sufficiently large) set $\mathbb{N}_{i}$.

We present the basic concepts for interpreting a fragment of the simply typed
$\lambda$-calculus within such a dynamic model. A type $\varrho$ is thereby
interpreted as a process, which is formally a factor system together with a
limit of it. A factor system is very similar to a direct or an inverse system,
and its limit is also defined by a universal property. It is crucial to
recognize that a limit is not necessarily an unreachable end beyond the
process. Rather, it can be regarded as an intermediate state within the factor
system, which can still be extended.

The logical type $bool$ plays an important role, which we interpret
classically as the set $\\{true,false\\}$. We provide an interpretation of
simply typed $\lambda$-terms in these factor systems and limits. The main
result is a reflection principle, which states that an element in the limit
has a “full representative” at a sufficiently large stage within the factor
system. For propositions, that is, terms of type $bool$, this implies that
statements about the limit are true if and only if they are true at that
sufficiently large stage.

###### keywords:

Indefinite extensibility, Potential infinite, Reflection principle

##  1 Introduction

In set theory, infinite sets are given by the dictum of the axiom of infinity.
There is no idea of “construction” or “approximation” involved — it is a
_static_ concept where only existence is required, without any way to get to
these sets. In contrast, consider the constructions of infinite sets as limits
of direct and inverse systems. These sets are approximated and so can be
understood from the perspective of a potential infinite. Moreover, they
possess the structure of their approximating parts. Finally, and most
importantly from a finitistic perspective, there is no necessity to “jump
over” to an absolute, actual infinite limit set if all states of the system
are finite. Instead, if one takes care of all the stages of one’s
investigation, then a sufficiently large state within the system is sufficient
and is a full substitute for an infinite limit set.

From a consequent potentialist’s point of view, it is actually a misuse of
language to call a set infinite. Since the potentialist’s view is a form of
finitism, and since sets are given by their extension, every set is finite in
this regard. Therefore, what can be considered infinite is the type, say
$nat$, whereas the set $\mathbb{N}$ would be more accurately described as
_indefinitely extensible_. Thus, the usual terminology, saying that a set is
infinite, means that its type is infinite and that the extension of the type,
i.e., the set of elements of that type, is given by some _indefinitely large_
state (or _sufficiently large_ state) in an indefinitely extensible system of
finite sets.

A system, introduced in Section 2.1, formalizes a changing totality of
objects, an “open” and potentially unending process in which both the
collection and its elements expand simultaneously. This process allows a
(relative) completion or compactification by constructing a limit, which
temporarily ends or “closes” the process.

The concept of partiality becomes relevant in extensible systems. It is a
consequence of the fact that objects can be generated, or if you prefer a less
constructive language, detected, so that they do not exist from the beginning.
Partiality first appears in direct systems, where objects do not exist at the
initial stages. In this situation, partiality is not difficult to deal with,
but it becomes demanding in the function space construction, especially in the
presence of higher types.

A few words about the notation. The term “iff” is an abbreviation for “if and
only if”. $\mathbb{N}$ refers to the set of natural numbers
$\\{0,1,2,\dots\\}$, $\mathbb{N}^{+}:=\mathbb{N}\setminus\\{0\\}$ and
$\mathbb{N}_{i}:=\\{0,\dots,i-1\\}$. We write $[A\to B]$ for the function
space of all functions with domain $A$ and codomain $B$, and
$\mathcal{P}(\mathcal{M})$ for the power set of $\mathcal{M}$.

###  1.1 Extensibility, Coinduction and Domain Theory

A fundamental concept in the context of the potential infinite is
_extensibility_. The main modes of extensibility are the creation of new
objects and the creation of new knowledge about existing objects. However, we
understand the latter as a differentiation of an object or an identification
of several objects. In the case of differentiation, there may be multiple
versions of an object at a later stage. When considering limit constructions,
this is different from the understanding of the accumulation of information.
To illustrate this point, let us consider inductive and coinductive
definitions. These are related to adding and differentiating objects
respectively, but they are not the only way.

  1. 1.

The dynamic reading of an inductive definition leads to an infinite process of
creating objects, related to direct systems.

  2. 2.

The dynamic reading of a coinductive definition leads to an infinite process
of differentiating objects, related to inverse systems.

To give an example, let $Seq$ denote finite 0-1-sequences and $Seq^{\infty}$
stand for infinite 0-1-sequences. Then the algebra with constructors
$nil:\\{\ast\\}\to Seq$ and $append:Seq\times\mathbb{N}_{2}\to Seq$
inductively defines the structure of $Seq$, whereby
$\mathbb{N}_{2}=\\{0,1\\}$. The coinductive definition of $Seq^{\infty}$ has
one destructor-pair $(head,tail):Seq^{\infty}\to\mathbb{N}_{2}\times
Seq^{\infty}$ and defines a coalgebra. To give these structural definitions a
dynamic reading requires an index set, which will be $\mathbb{N}^{+}$ and
$\mathbb{N}$.

In case of inductive definitions one starts with the element $\ast$. The
states of $Seq$ are thus $Seq_{0}=\\{\ast\\}$, $Seq_{1}=\\{()\\}$,
$Seq_{2}=\\{(),0,1\\}$, $Seq_{3}=\\{(),0,1,00,01,10,11\\}$ and so on. The
inductive definition of $Seq$ gives rise to a direct system
$(Seq_{i})_{i\in\mathbb{N}^{+}}$ with subset inclusion as embedding. A direct
system is more general than this construction by an inductive definition, as
it allows for the possibility of non-injective embeddings. This corresponds to
the addition and identification of objects in a single process and is relevant
for a construction of quotients.

For a dynamic understanding of coinductive definitions, start with a “generic”
element, say $s$, so $Seq^{\infty}_{0}=\\{s\\}$. The destructor-pair
$(head,tail)$ gives $Seq^{\infty}_{1}=\\{0s,1s\\}$,
$Seq^{\infty}_{2}=\\{00s,01s,10s,11s\\}$, and so on. The coinductive
definition of $Seq^{\infty}$ allows one to increase the knowledge about the
sequence, which we understand as a process of differentiation. The projections
$proj_{i}^{i^{\prime}}:Seq^{\infty}_{i^{\prime}}\to Seq^{\infty}_{i}$ then
remove this information gained by differentiation, e.g.,
$proj_{1}^{2}(01s)=0s$. We read $01s\in Seq^{\infty}_{2}$ and $0s\in
Seq^{\infty}_{1}$ as states of the same (infinite) object, differing only in
the amount of information that we have about that object. The inverse system
$(Seq^{\infty},proj)$ corresponds to subsets $A\subseteq\mathbb{N}$ if we take
$A=\\{i\in\mathbb{N}\mid s_{i}=1\\}$ for $(s_{i})_{i\in\mathbb{N}}\in
Seq^{\infty}$.

This idea of differentiating objects is also related to Brouwer’s concept of
(lawlike and lawless) choice sequences within a spread — the standard text on
this subject is [13]. However, our approach does not involve the constructive
reasoning that is inherent in the definition of a spread.

Differentiating infinite objects differs from domain theory [1], where the
ideal, infinite elements are ideals (being infinite sets) of their
approximating parts, which are the compact elements. In domain theory, each
approximation is seen as a different object, not as states of one object, and
the ideal completion uses the idea that sets are _actual_ infinite. In other
words, the idea of differentiating infinite objects, as formulated in
coinductive definitions and inverse systems, is not present in domain theory.
Domain theory uses inductive definitions and least fixed point constructions.

Another way to get these ideal elements in domains is to think of an infinite
domain as a bilimit of finite domains. A bilimit is a limit construction where
direct and inverse limits coincide. One could interpret this coincidence as a
reduction of inverse systems to direct systems. In the approach here, the
limit construction is, roughly speaking, between the direct and the inverse
limit, since the predecessor relation $\stackrel{{\scriptstyle p}}{{\mapsto}}$
(which will be introduced soon) is, again roughly speaking, between the
embedding $emb$ and the projection $proj$. In Section 2.1 we will introduce
such an embedding-projection pair, associated with the predecessor relation
$\stackrel{{\scriptstyle p}}{{\mapsto}}$. Direct and inverse systems can then
be seen as extreme situations of adding and differentiating objects, while the
system based on the predecessor relation $\stackrel{{\scriptstyle
p}}{{\mapsto}}$ is in general a combination of both.

###  1.2 Formalizing the Potential Infinite

A potential infinite set $\mathcal{M}$ is a dynamic, finite set. To formalize
this consequently, any reference to $\mathcal{M}$ can only be made by
reference to some finite state $\mathcal{M}_{i}$. A completed totality of all
elements or all states of this set does not exist. For example, there exist
states $\mathbb{N}_{i}$ of the set of natural numbers, but there is neither a
complete set $\mathbb{N}$ nor the complete family of all sets
$\mathbb{N}_{i}$. The latter has to do with the fact that, for a consequent
reading, this finitistic view applies to meta-level concepts as well, in
particular to the index set from which the indices $i$ are taken; see Section
1.4 for more on this.

In a first step we introduce indices $i$, given by a directed index set
$\mathcal{I}$, i.e., a set $\mathcal{I}$ of stages together with a binary,
reflexive and transitive relation $\leq$ so that any finite set of indices has
an upper bound. A potential infinite set is thus a family
$\mathcal{M}_{\mathcal{I}}$ of states $\mathcal{M}_{i}$, $i\in\mathcal{I}$,
where all sets are finite.

We want to express that two elements $a_{i}\in\mathcal{M}_{i}$ and
$a_{i^{\prime}}\in\mathcal{M}_{i^{\prime}}$ at different stages $i$ and
$i^{\prime}$ are equal. This equality is not given by an equivalence relation,
but by a family of reflexive relations $\stackrel{{\scriptstyle
p}}{{\mapsto}}_{i^{\prime},i}\,\subseteq\mathcal{M}_{i^{\prime}}\times\mathcal{M}_{i}$
for $i^{\prime}\geq i$. We write $a_{i^{\prime}}\stackrel{{\scriptstyle
p}}{{\mapsto}}a_{i}$ for $(a_{i^{\prime}},a_{i})\in\ \stackrel{{\scriptstyle
p}}{{\mapsto}}_{i^{\prime},i}$, saying that $a_{i}$ is a predecessor of
$a_{i^{\prime}}$, and we use $\stackrel{{\scriptstyle p}}{{\mapsto}}$ as an
abbreviation for $\stackrel{{\scriptstyle p}}{{\mapsto}}_{i^{\prime},i}$.
Reflexivity means that $a_{i}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}$ for
all $i\in\mathcal{I}$ and $a_{i}\in\mathcal{M}_{i}$. We do not require
$\stackrel{{\scriptstyle p}}{{\mapsto}}$ to be transitive.111The reason is
this: The index set of the function space is $\mathcal{I}\times\mathcal{J}$
with pairs written as $i\to j$ (c.f. Section 2.2). Call an extension of the
index from $i\to j$ to $i\to j^{\prime}$, $j^{\prime}\geq j$, _covariant_ and
from $i\to j$ to $i^{\prime}\to j$, $i^{\prime}\geq i$, _contravariant_. Then
a combination of two different kind of extensions may fail to be a correct
extension. For an example, see [5]. A _system_
$(\mathcal{M}_{\mathcal{I}},\stackrel{{\scriptstyle p}}{{\mapsto}})$ consists
of a family $\mathcal{M}_{\mathcal{I}}$ together with reflexive relations
$\stackrel{{\scriptstyle p}}{{\mapsto}}$. Later we will introduce further
properties in order to allow a function space construction, leading to the
notion of a _factor system_ [5].

Let types $\varrho\in{Typ}$ be given. In this paper they consist of some base
types $\iota$, including type $bool$ for propositions, which are interpreted
classically as the Boolean values $true$ and $false$, and a type constructor
$\to$. So types are $\varrho::=\iota\,\,|\,\,\varrho\to\varrho$. A (typing)
context $\Gamma$ is a list of types $(\varrho_{0},\dots,\varrho_{n-1})$. More
explicitly we can write
$(\mathsf{x_{0}}:\varrho_{0},\dots,\mathsf{x_{n-1}}:\varrho_{n-1})$ for the
context $\Gamma$, since we use a fixed list of variables
$\mathsf{x_{0}},\mathsf{x_{1}},\mathsf{x_{2}},\dots$ in Section 3. The empty
context is $()$ and $\Gamma.\varrho$ denotes the context $\Gamma$, extended by
$\varrho$. We assume that for each type $\varrho$ there is an index set
$(\mathcal{I}_{\varrho},\leq)$, so each type comes with its own set of stages.
For instance, the index set for type $nat$ is $(\mathbb{N}^{+},\leq)$ with
$\mathcal{M}_{i}=\mathbb{N}_{i}$ for $i\in\mathbb{N}^{+}$.222The use of
$\mathbb{N}^{+}$ instead of $\mathbb{N}$ as index set is done for technical
reasons: A factor system has projections between different states
$\mathbb{N}_{i}$, and there is no projection from $\mathbb{N}_{i}$, $i>0$ into
$\mathbb{N}_{0}=\emptyset$. Another example is type $bool$ with the singleton
set $(\\{bool\\},=)$ of one index $bool$ and
$\mathcal{M}_{bool}:=\mathbb{B}:=\\{true,false\\}$. For a typing context
$\Gamma=(\varrho_{0},\dots,\varrho_{n-1})$ define
$\mathcal{I}_{\Gamma}:=\mathcal{I}_{\varrho_{0}}\times\dots\times\mathcal{I}_{\varrho_{n-1}}$
and endow $\mathcal{I}_{\Gamma}$ with the product order.

Since we want to consider sets, relations and functions as objects, i.e., as
elements of further potential infinite sets, we have to consider elements as
dynamic entities as well. A dynamic object $a$ of type $\varrho$ is given by
its states $a_{i}$, $i\in\mathcal{I}_{\varrho}$. As with sets, any reference
to $a$ can only be a reference to one of its states $a_{i}$.

A dynamic object needs not be defined on all stages
$i\in\mathcal{I}_{\varrho}$, so the index set $\mathcal{I}_{a}$, for which a
state $a_{i}$ of $a$ exists, is a subset of $\mathcal{I}_{\varrho}$, i.e.,
$\mathcal{I}_{a}\subseteq\mathcal{I}_{\varrho}$. One of the basic requirements
is that every object has “sufficiently many” indices $\mathcal{I}_{a}$. For
natural numbers, or more generally for base type objects, the situation is
simple: If a number $n$ occurs at stage $n+1$, i.e., $n\in\mathbb{N}_{n+1}$,
it will be there for all future stages $m>n+1$, i.e., $n\in\mathbb{N}_{m}$, so
the index set $\mathcal{I}_{n}=\\{n+1,n+2,\dots\\}$ is an up-set. By _up-set_
we mean a non-empty, upward closed subset, in this case a subset of
$\mathbb{N}^{+}$. For higher-order functions, however, the situation is less
straightforward and is one of the main challenges of this approach.

The concept of a potential infinite has two aspects, a cardinal aspect
$\mathfrak{D}$ and an ordinal aspect $\ll$. Let
$C=(i_{0},\dots,i_{n-1})\in\mathcal{I}_{\Gamma}$ be a list of indices
$i_{0}\in\mathcal{I}_{\varrho_{0}},\dots,i_{n-1}\in\mathcal{I}_{\varrho_{n-1}}$,
for $\Gamma=(\varrho_{0},\dots,\varrho_{n-1})$, called _state context_. Write
$C.i$ for the extension of $C$ by $i$.

  1. 1.

The cardinal aspect is given by a set
$\mathfrak{D}_{\Gamma}\subseteq\mathcal{P}(\mathcal{I}_{\Gamma})$ for each
context $\Gamma$. $\mathcal{H}\in\mathfrak{D}_{\Gamma}$ says that there are
_indefinitely many_ , or _sufficiently many_ contexts in $\mathcal{H}$.

  2. 2.

The ordinal aspect is given by relations
$\ll^{\Gamma.\varrho}\,\in\mathfrak{D}_{\Gamma.\varrho}$. Let $C\ll i$ stand
for $C.i\in\ll^{\Gamma.\varrho}$, meaning that a stage $i$ is _indefinitely
large_ , or _sufficiently large_ relative to the state context $C$.

The sets $\mathfrak{D}_{\Gamma}$ satisfy the following properties: Each set
$\mathcal{H}\in\mathfrak{D}_{\Gamma}$ is cofinal — recall that cofinality of
$\mathcal{H}$ means $\forall C\in\mathcal{I}_{\Gamma}\,\exists C^{\prime}\geq
C$ with $C^{\prime}\in\mathcal{H}$. This minimal requirement simply states
that we will always find a context in $\mathcal{H}$ beyond any bound.
$\mathfrak{D}_{\Gamma}$ is closed under supersets, so “more than indefinitely
many is indefinitely many”. Furthermore, an up-set on $\mathcal{I}_{\Gamma}$
always has indefinitely many indices. Finally, the main restriction is that
$\mathfrak{D}_{\Gamma}$ is closed under intersections. This is necessary in
order to guarantee that a relation between two objects can be established on
indefinitely many indices. This amounts to saying:

$\mathfrak{D}_{\Gamma}\text{ is a proper filter on
}\\{\mathcal{H}\subseteq\mathfrak{D}_{\Gamma}\mid\mathcal{H}\text{ is
cofinal}\\}\text{ and }\mathfrak{D}_{\Gamma}\text{ contains all up-sets}.$
(Filter)

We will use the locution _$\mathfrak{D}$ -many indices_, which refers to a set
in $\mathfrak{D}_{\Gamma}$, and _cofinal many indices_ , which refers to a
cofinal index set. The interpretation in a potential infinite structure, which
we introduce in Section 3, will be relative to $\mathfrak{D}$ (and later also
relative to $\ll$, when we introduce the universal quantifier in a subsequent
paper).

A basic theme of the potential infinite is _dependency_. In particular, there
are no fixed sets $\mathfrak{D}$ and $\ll$, but these are parameters that
depend on factors of the concrete mathematical investigation and the state of
it. Another way of expressing this is to say that $\mathfrak{D}$ and $\ll$ are
intensional notions whose extension depends on the context of investigation.
In the same way that $\mathfrak{D}$ and $\ll$ depend on the investigation,
some concepts, in turn, depend on $\mathfrak{D}$ and $\ll$; the notion of
continuity depends on $\mathfrak{D}$ and the interpretation of the universal
quantifier depends on $\ll$. It is possible to define continuity on limit sets
without reference to the underlying system. The basic relation is then a
family of PERs and we will explore this structure in more detail in a separate
paper. Moreover, in this paper we deal only with the cardinal aspect, i.e.,
$\ll$ is not considered here.

###  1.3 Relation to Constructive Approaches

We are only investigating the idea of a potential infinite, not that of
constructivity, decidability, complexity or knowledge about existence, which
are important concepts in intuitionism [14] and in theories about
computability [8]. The common models of intuitionistic logic, such as Kripke
models, or more generally topos-theoretic models [9], use unbounded universal
quantification. For instance, in a Kripke model, the validity of a universal
quantified formula uses a reference to all “future” nodes — there could be
infinitely many of them and at each such node the carrier set could be an
infinite set as well. In our approach, only finite sets are used, and in a
consequent finitistic view only finitely many of them.

We use classical logic. This is because it has a simpler model than
constructive models and is more widely used. Furthermore, the results
presented here rely on the fact that classical logic has a finite number of
truth values. This is an important difference from intuitionistic logic, which
has, if truth values are used at all, infinitely many of them.

The novel aspect of this potential infinite model is the introduction of
_state judgements_ , which are refinements of typing judgements. If
$\Gamma\vdash\mathsf{r}:\varrho$ is such a typing judgement, then a state
judgement has the form $C\mid\mathsf{r}:i$, where $C$ is a stage of the
context $\Gamma$ and $i$ is a stage of the type $\varrho$. The idea that we
can only refer to infinite objects via a specific state is reflected in the
fact that the primary object of interpretations is a state judgement
$C\mid\mathsf{r}:i$. It is interpreted in a family of factor systems, which
have only “local” application functions given as

$App_{i,j}:[\mathcal{M}_{i}\to\mathcal{N}_{j}]\times\mathcal{M}_{i}\to\mathcal{N}_{j},\
(f_{i\to j},a_{i})\mapsto f_{i\to j}(a_{i}).$

Additionally, the typing judgement $\Gamma\vdash\mathsf{r}:\varrho$ has an
interpretation in the limit set. However, the notion of a limit of a factor
system depends on the notion of “indefinitely many stages”, which we formalize
as sets $\mathfrak{D}_{\varrho}$. This is in particular relevant for the
function space and the possibility to define a “global” application function
$App:[\mathcal{M}\to\mathcal{N}]\times\mathcal{M}\to\mathcal{N},(f,a)\mapsto
f(a)$ on limit sets, leading to a common _extensional type structure_ [2]. The
question which higher-order functions exist and whether all local applications
together yield a global application depends on the properties of
$\mathfrak{D}_{\varrho}$. A global application function is available for all
first-order functions, however, this may not be the case for higher-order
functions. In contrast, in a type structure, also referred to as _(typed)
applicative structure_ , a global application is available for all types. This
holds analogously for _Kripke applicative structures_ [10].

###  1.4 The Meta-Theory

The meta-theory in which the concepts are developed is classical higher-order
logic, as formalized in Church’s simple type theory [3]. This theory will also
serve as the investigated theory. At the object-level, we develop a potential
infinite model in order to interpret typed $\lambda$-terms. At the meta-level
these two views of infinity are relevant:

  1. 1.

One accepts actual infinity at the meta-level. In this case, a limit can be
seen as the usual actual infinite set beyond the system. This view allows a
comparison of an actual infinite model, given as limit structure, with the
potential infinite part, i.e., the system.

  2. 2.

One uses the view that infinity is an extensible finite. Then a limit is an
intermediate state of the system. This is the consistent realization of the
finitistic approach.

The reflection principle, which is the main theorem of this paper, states in
the first case that all objects in the limit, including propositions, have a
counterpart in the factor system. So it says something like this: Whatever
exists and holds under the assumption that actual infinite sets exist, already
exists and holds at a sufficiently large stage in the system. For infinite
objects, these can be seen as approximations. For type $bool$, which is
interpreted in classical logic as a finite set of truth values
$\\{true,false\\}$, the values are the same in the actual infinite limit set
and at a finite stage of the system. This is because these values are not
approximated.

In the second case, the reflection principle is only a means to show the
correctness of the interpretation. However, a consistent realization requires
that an infinite set on meta-level, like the index set $\mathcal{I}$, is only
available at a stage $j$. A consequent realization in type theory moreover
uses a type in place of the index set, together with a term $\leq$, which is
then shown to be reflexive, transitive, and directed.

The use of a classical meta-theory instead of a constructive one is not
essential here. We could also take an intuitionistic type theory at meta-level
and develop most of the model theory in a pure constructive way. So we expect
that the model construction can be formalized in common proof assistants such
as Coq, Lean or Agda. We need, however, a bit of classical reasoning, at least
when introducing the universal quantifier. To prove the reflection principle
with universal quantifier as an extension of Theorem 3.9, one has to do a kind
of Löwenheim-Skolem construction. This requires that a universal quantified
formula is either true (at all stages), or it is false at some stage and is
false at all later stages, too. It is of greater significance that, for a
consequent realization, in which only potential infinities are used at meta-
level, the proof assistant must implement state judgments.

###  1.5 Structure of the Paper

We already started in Section 1.2 to formalize the potential infinite as a
dynamic concept, which replaces an actual infinite set with a _factor system_
, which is, roughly, a generalization of a direct and inverse system. The
concept of factor systems was first introduced in [5]. In Section 2 we
reiterate the definition of a factor system and add further definitions that
are necessary for an interpretation. These are primarily the notions of a
direct and inverse factor system, which are required to interpret variables.
We show the construction of the function space between two factor systems and
elucidate the notions of a target and a limit of a factor system. As with
direct and inverse systems, limits are targets that satisfy a universal
property and have a concrete construction. In Section 2.5 we demonstrate how
to introduce an application that makes limit sets a type structure.

Section 3 introduces a judgement for states, parallel to judgements for types.
These are defined on a fragment of the simply typed $\lambda$-calculus, which
we call _core fragment_. Based on these state judgements we give a first
version of an interpretation of $\lambda$-terms in the core fragment, not
including any constants. In particular, the present paper does not yet include
logic. We give an interpretation of types and terms with two parts, one is
within the system, the other is in its limit. Based on this interpretation we
show a first version of a reflection principle, which says that an element $a$
of type $\varrho$ in the limit set is reflected by an element $a_{i}$ at some
stage $i\in\mathcal{I}_{\varrho}$ in the system. This element $a_{i}$ is an
approximation of $a$, and at the same time it fully represents $a$. If logic
is included, then the representation includes all propositions about these
elements, so anything we can say about $a$ is true if and only if it is true
for $a_{i}$.

##  2 Factor Systems and their Limits

Factor systems and their limits have been introduced in [5]. In this paper, we
summarize their properties. The main concept is that of a factor system, those
of a prefactor system (with embeddings/projections) are afferent notions. In
addition to that, we introduce the notion of a _stable_ system, which is a
natural notion to prove stronger properties, although these are not necessary
here. We prove that stability is closed under both the function space
construction and the limit construction.

Relevant for the interpretation in Section 3 are the specific forms of a
_direct_ and _inverse_ factor system. A direct factor system is similar to a
direct system, it is more specific in the sense that the embedding is part of
an embedding-projection pair. On the other hand it is more general in the
sense that equations hold only up to an equivalence relation. The same holds
for inverse factor systems and inverse systems. Moreover, we introduce the
concept of a _homomorphism_ between two systems.

The subsequent Lemmata 2.11 and 2.13 are extended versions of corresponding
lemmata in [5], which use the property (Filter), not only cofinality. These
versions are necessary to prove Corollary 2.22, which states that the function
space construction commutes with the limit construction. This is a
prerequisite for the definition of a model. Proposition 2.8 and Corollary 2.17
describe how direct and inverse factor systems extend to the function space
and to the limit. Both are essential to prove the reflection principle for
variables.

###  2.1 Factor Systems

$\mathcal{I}$ will always denote a non-empty directed index set with preorder
$\leq$. A _system_ is a pair
$(\mathcal{M}_{\mathcal{I}},\stackrel{{\scriptstyle p}}{{\mapsto}})$
consisting of a family
$\mathcal{M}_{\mathcal{I}}:=(\mathcal{M}_{i})_{i\in\mathcal{I}}$ and reflexive
(for $i=i^{\prime}$) relations $\stackrel{{\scriptstyle p}}{{\mapsto}}$ on
$\mathcal{M}_{i^{\prime}}\times\mathcal{M}_{i}$ for $i^{\prime}\geq i$. Two
elements $a_{i}\in\mathcal{M}_{i}$ and $b_{j}\in\mathcal{M}_{j}$ are
_consistent_ , written as $a_{i}\asymp b_{j}$, iff there is an index
$i^{\prime}\geq i,j$ and some $a_{i^{\prime}}\in\mathcal{M}_{i^{\prime}}$ such
that $a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}$ and
$a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}b_{j}$. As a convention,
whenever we use a suffix $i\in\mathcal{I}$ for some element, this refers to
the state, e.g. $a_{i}\in\mathcal{M}_{i}$. An important special case is that
the relations $\stackrel{{\scriptstyle p}}{{\mapsto}}$ are partial functions,
which is equivalent to:

$a_{i}\asymp b_{i}\iff a_{i}\stackrel{{\scriptstyle p}}{{\mapsto}}b_{i}\iff
a_{i}=b_{i}$ (Fun)

for all $a_{i},b_{i}\in\mathcal{M}_{i}$ and all $i\in\mathcal{I}$. A system
that satisfies (Fun) is called _standard_.
$(\mathcal{M}_{\mathcal{I}},\stackrel{{\scriptstyle p}}{{\mapsto}})$ is a
_prefactor system_ iff it is a system satisfying

$a_{i^{\prime}}\asymp a_{i}\iff a_{i^{\prime}}\stackrel{{\scriptstyle
p}}{{\mapsto}}a_{i}$ (Factor)

for all $a_{i}\in\mathcal{M}_{i}$ and
$a_{i^{\prime}}\in\mathcal{M}_{i^{\prime}}$ with $i\leq i^{\prime}$. The
relation $\asymp$ is then an equivalence relation on a single set
$\mathcal{M}_{i}$ with $a_{i}\asymp b_{i}\iff a_{i}\stackrel{{\scriptstyle
p}}{{\mapsto}}b_{i}\iff b_{i}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}\
\text{ for }a_{i},b_{i}\in\mathcal{M}_{i}$. In a prefactor system
$b_{i^{\prime}}\asymp a_{i^{\prime}}\stackrel{{\scriptstyle
p}}{{\mapsto}}a_{i}$ implies $b_{i^{\prime}}\stackrel{{\scriptstyle
p}}{{\mapsto}}a_{i}$, but sometimes we want to have the “dual” property as
well, which we call _stability_. Although we can do without stability for most
properties, it is an obvious requirement, and all natural examples satisfy
this property. Note that a system that satisfies (Fun) is automatically
stable.

######  Definition 2.1.

A system $(\mathcal{M}_{\mathcal{I}},\stackrel{{\scriptstyle p}}{{\mapsto}})$,
and in particular the relation $\stackrel{{\scriptstyle p}}{{\mapsto}}$, is
called _stable_ iff for all $i^{\prime}\geq i$, all
$a_{i^{\prime}}\in\mathcal{M}_{i^{\prime}}$ and
$a_{i},b_{i}\in\mathcal{M}_{i}$

$a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}\asymp b_{i}\
\Rightarrow\ a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}b_{i}.$
(Stab)

A family $emb=(emb_{i}^{i^{\prime}})_{i\leq i^{\prime}}$ of
$\asymp$-embeddings consists of $\asymp$-preserving maps
$emb_{i}^{i^{\prime}}:\mathcal{M}_{i}\to\mathcal{M}_{i^{\prime}}$ satisfying
$emb_{i}^{i}(a_{i})\asymp a_{i}$ and
$emb_{i^{\prime}}^{i^{\prime\prime}}(emb_{i}^{i^{\prime}}(a_{i}))\asymp
emb_{i}^{i^{\prime\prime}}(a_{i})$. The requirement $\asymp$-preserving means
that $emb_{i}^{i^{\prime}}(a_{i})\asymp emb_{i}^{i^{\prime}}(b_{i})$ holds for
$a_{i}\asymp b_{i}$, for all $a_{i},b_{i}\in\mathcal{M}_{i}$. Similar to a
family of $\asymp$-embeddings, $\asymp$-projections
$proj=(proj_{i}^{i^{\prime}})_{i\leq i^{\prime}}$ consist of
$\asymp$-preserving maps
$proj_{i}^{i^{\prime}}:\mathcal{M}_{i^{\prime}}\to\mathcal{M}_{i}$ satisfying
$proj_{i}^{i}(a_{i})\asymp a_{i}$ and
$proj_{i}^{i^{\prime}}(proj_{i^{\prime}}^{i^{\prime\prime}}(a_{i^{\prime\prime}}))\asymp
proj_{i}^{i^{\prime\prime}}(a_{i^{\prime\prime}})$. Moreover,
$\asymp$-embeddings $emb$ together with $\asymp$-projections $proj$ form an
_$\asymp$ -embedding-projection pair_ iff
$proj_{i}^{i^{\prime}}(emb_{i}^{i^{\prime}}(a_{i}))\asymp a_{i}$ holds for all
$a_{i}\in\mathcal{M}_{i}$ and all $i\leq i^{\prime}$.

The $\asymp$-embeddings $emb$ and $\asymp$-projections $proj$ are _coherent_
if they satisfy for all indices $i\leq i^{\prime}\leq i^{\prime\prime}$

$\displaystyle a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}\ $
$\displaystyle\Rightarrow\
emb_{i^{\prime}}^{i^{\prime\prime}}(a_{i^{\prime}})\stackrel{{\scriptstyle
p}}{{\mapsto}}a_{i}\text{ and}$ (Emb) $\displaystyle
a_{i^{\prime\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}\ $
$\displaystyle\Rightarrow\
proj_{i^{\prime}}^{i^{\prime\prime}}(a_{i^{\prime\prime}})\stackrel{{\scriptstyle
p}}{{\mapsto}}a_{i}\text{ resp.}$ (Proj)

A $\asymp$-embedding-projection pair $(emb,proj)$ is coherent if $emb$ and
$proj$ are both coherent. Property (Emb) implies that
$emb_{i}^{i^{\prime}}(a_{i})\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}$ holds
for all $a_{i}\in\mathcal{M}_{i}$, and in case that Property (Fun) holds,
$\stackrel{{\scriptstyle p}}{{\mapsto}}$ is a _partial surjection_.

######  Definition 2.2.

A _prefactor system with embeddings_ is a prefactor system
$(\mathcal{M}_{\mathcal{I}},\stackrel{{\scriptstyle p}}{{\mapsto}})$ with
coherent $\asymp$-embeddings $emb$. A _prefactor system with projections_ is a
prefactor system $(\mathcal{M}_{\mathcal{I}},\stackrel{{\scriptstyle
p}}{{\mapsto}})$ with coherent $\asymp$-projections $proj$. A _factor system_
is a prefactor system $(\mathcal{M}_{\mathcal{I}},\stackrel{{\scriptstyle
p}}{{\mapsto}})$ with a coherent $\asymp$-embedding-projection pair
$(emb,proj)$. A prefactor system is _direct_ iff it has coherent
$\asymp$-embeddings which satisfy

$a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}\iff
a_{i^{\prime}}\asymp emb_{i}^{i^{\prime}}(a_{i}).$ (Dir)

A prefactor system is _inverse_ iff it has coherent $\asymp$-projections which
satisfy

$a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}\iff
proj_{i}^{i^{\prime}}(a_{i^{\prime}})\asymp a_{i}.$ (Inv)

If $\stackrel{{\scriptstyle p}}{{\mapsto}}$, $emb$ and $proj$ are known, we
often call $\mathcal{M}_{\mathcal{I}}$ a factor system (and likewise with
prefactor systems with embeddings/projections).

######  Example 2.3.

The embeddings $emb$ in a direct system $(\mathcal{M}_{\mathcal{I}},emb)$,
with $a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}:\\!\iff
emb_{i}^{i^{\prime\prime}}(a_{i})=emb_{i^{\prime}}^{i^{\prime\prime}}(a_{i^{\prime}})$
for some $i^{\prime\prime}\geq i,i^{\prime}$, are automatically
$\asymp$-embeddings, since they preserve $\asymp$. If there are
$\asymp$-projections $proj$, such that $emb$ and $proj$ form a
$\asymp$-embedding-projection pair, then
$(\mathcal{M}_{\mathcal{I}},\stackrel{{\scriptstyle p}}{{\mapsto}},emb,proj)$
is a direct factor system.

An inverse system $(\mathcal{M}_{\mathcal{I}},proj)$ satisfies (Fun), so the
projections $proj$ are automatically $\asymp$-projections. If there are
$\asymp$-embeddings $emb$, such that $emb$ and $proj$ form a
$\asymp$-embedding-projection pair, then
$(\mathcal{M}_{\mathcal{I}},\stackrel{{\scriptstyle p}}{{\mapsto}},emb,proj)$,
with $a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}:\\!\iff
proj_{i}^{i^{\prime}}(a_{i^{\prime}})=a_{i}$, is an inverse factor system.

######  Example 2.4.

Consider $(\mathbb{N}_{i})_{i\in\mathbb{N}^{+}}$ with the embedding-projection
pair $emb_{i}^{i^{\prime}}:\mathbb{N}_{i}\to\mathbb{N}_{i^{\prime}}$,
$n\mapsto n$ and
$proj_{i}^{i^{\prime}}:\mathbb{N}_{i^{\prime}}\to\mathbb{N}_{i}$ with
$n\mapsto\min(n,i-1)$. In all three cases for $\stackrel{{\scriptstyle
p}}{{\mapsto}}$ they form an $\asymp$-embedding-projection pair and
$((\mathbb{N}_{i})_{i\in\mathbb{N}^{+}},\stackrel{{\scriptstyle
p}}{{\mapsto}},emb,proj)$ is a factor system:

  1. 1.

The standard model of the natural numbers has $\mathbb{N}_{i^{\prime}}\ni
n\stackrel{{\scriptstyle p}}{{\mapsto}}n\in\mathbb{N}_{i}$ for all $n<i$,
which is a direct factor system.

  2. 2.

The definition $n^{\prime}\stackrel{{\scriptstyle p}}{{\mapsto}}n:\\!\iff
proj_{i}^{i^{\prime}}(n^{\prime})=n$ makes it an inverse factor system.

  3. 3.

With $n^{\prime}\stackrel{{\scriptstyle p}}{{\mapsto}}n$ for all
$n^{\prime}\in\mathbb{N}_{i^{\prime}}$ and $n\in\mathbb{N}_{i}$, the factor
system $(\mathbb{N}_{i})_{i\in\mathbb{N}^{+}}$ is direct and inverse.

The second example basically adds an infinite number to $\mathbb{N}$, while
the last example is artificial, but shows the difference to direct an inverse
limits when we pick up this factor system again in Example 2.10. One can
easily check that $(\mathbb{N}_{i})_{i\in\mathbb{N}^{+}}$ is stable in all
three cases, and in the first two cases Property (Fun) is also satisfied.

######  Lemma 2.5.

Let $\mathcal{M}_{\mathcal{I}}$ be a prefactor system and given indices
$i^{\prime\prime}\geq i^{\prime}\geq i$.

  1. 1.

If $\mathcal{M}_{\mathcal{I}}$ is direct, then
$a_{i^{\prime\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}$ implies
$a_{i^{\prime\prime}}\stackrel{{\scriptstyle
p}}{{\mapsto}}emb_{i}^{i^{\prime}}(a_{i})$.

  2. 2.

If $\mathcal{M}_{\mathcal{I}}$ is inverse, then
$a_{i^{\prime\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i^{\prime}}$
implies $a_{i^{\prime\prime}}\stackrel{{\scriptstyle
p}}{{\mapsto}}proj_{i}^{i^{\prime}}(a_{i^{\prime}})$.

######  Proof 2.6.

First, $a_{i^{\prime\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}$
implies
$emb_{i^{\prime}}^{i^{\prime\prime}}(emb_{i}^{i^{\prime}}(a_{i}))\asymp
emb_{i}^{i^{\prime\prime}}(a_{i})\asymp a_{i^{\prime\prime}}$ by (Dir), hence
$emb_{i^{\prime}}^{i^{\prime\prime}}(emb_{i}^{i^{\prime}}(a_{i}))\stackrel{{\scriptstyle
p}}{{\mapsto}}a_{i^{\prime\prime}}$. From (Emb) we deduce
$emb_{i^{\prime}}^{i^{\prime\prime}}(emb_{i}^{i^{\prime}}(a_{i}))\stackrel{{\scriptstyle
p}}{{\mapsto}}emb_{i}^{i^{\prime}}(a_{i})$ and thus
$a_{i^{\prime\prime}}\stackrel{{\scriptstyle
p}}{{\mapsto}}emb_{i}^{i^{\prime}}(a_{i})$ by (Factor). For the second clause
let $a_{i^{\prime\prime}}\stackrel{{\scriptstyle
p}}{{\mapsto}}a_{i^{\prime}}$, then
$proj_{i^{\prime}}^{i^{\prime\prime}}(a_{i^{\prime\prime}})\asymp
a_{i^{\prime}}$ by (Inv), hence
$proj_{i}^{i^{\prime\prime}}(a_{i^{\prime\prime}})\asymp
proj_{i}^{i^{\prime}}(proj_{i^{\prime}}^{i^{\prime\prime}}(a_{i^{\prime\prime}}))\asymp
proj_{i}^{i^{\prime}}(a_{i^{\prime}})$. Consequently
$a_{i^{\prime\prime}}\stackrel{{\scriptstyle
p}}{{\mapsto}}proj_{i}^{i^{\prime}}(a_{i^{\prime}})$ by (Inv) again, as
claimed.

Compare these properties with (Emb) and (Proj), which hold in any prefactor
system with embeddings/projections.

######  Definition 2.7.

A _homomorphism_ $\Phi=(\Phi_{0},(\Phi^{i})_{i\in\mathcal{I}})$ between two
systems $(\mathcal{M}_{\mathcal{I}},\stackrel{{\scriptstyle p}}{{\mapsto}})$
and $(\mathcal{N}_{\mathcal{J}},\stackrel{{\scriptstyle p}}{{\mapsto}})$
consists of maps $\Phi_{0}:\mathcal{I}\to\mathcal{J}$ and
$\Phi^{i}:\mathcal{M}_{i}\to\mathcal{N}_{\Phi_{0}(i)}$ such that $\Phi_{0}$ is
monotone and for all $i\leq i^{\prime}$

$a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}\ \Rightarrow\
\Phi^{i^{\prime}}(a_{i^{\prime}})\stackrel{{\scriptstyle
p}}{{\mapsto}}\Phi^{i}(a_{i}).$ (1)

If (1) is an equivalence, then $\Phi$ is said to be _strong_. A homomorphism
between two prefactor systems with embeddings
$(\mathcal{M}_{\mathcal{I}},\stackrel{{\scriptstyle p}}{{\mapsto}},emb)$
additionally satisfies
$\Phi^{i^{\prime}}(emb_{i}^{i^{\prime}}(a_{i}))=emb_{j}^{j^{\prime}}(\Phi^{i}(a_{i}))$,
$j:=\Phi_{0}(i)$, $j^{\prime}:=\Phi_{0}(i^{\prime})$, a homomorphism between
two prefactor systems with projections
$(\mathcal{M}_{\mathcal{I}},\stackrel{{\scriptstyle p}}{{\mapsto}},proj)$
satisfies
$\Phi^{i}(proj_{i}^{i^{\prime}}(a_{i^{\prime}}))=proj_{j}^{j^{\prime}}(\Phi^{i^{\prime}}(a_{i^{\prime}}))$,
and a homomorphism between two factor systems satisfies both equations.

We call $\Phi$ injective (surjective) iff every map in $\Phi$ is injective
(surjective resp.). An _isomorphism_ $\Phi$ between two systems (prefactor
systems with embeddings/projections, factor systems) is a homomorphism with a
further homomorphism $\Psi$ as its inverse, i.e., each part of $\Psi$ is
inverse to that of $\Phi$. So an isomorphism is automatically strong. We write
$\mathcal{M}_{\mathcal{I}}\simeq\mathcal{N}_{\mathcal{J}}$ if an isomorphism
between $\mathcal{M}_{\mathcal{I}}$ and $\mathcal{N}_{\mathcal{J}}$ exists.

In the following we will use homomorphisms $\Phi$ only for the special
situation that $\mathcal{I}=\mathcal{J}$ and $\Phi_{0}$ is the identity map.
In that case we do not mention $\Phi_{0}$.

###  2.2 The Function Space

The function space of two factor systems $\mathcal{M}_{\mathcal{I}}$ and
$\mathcal{N}_{\mathcal{J}}$, denoted as
$[\mathcal{M}_{\mathcal{I}}\to\mathcal{N}_{\mathcal{J}}]$, is a family of
(finite) sets $[\mathcal{M}_{i}\to\mathcal{N}_{j}]$ indexed by pairs
$(i,j)\in\mathcal{I}\times\mathcal{J}$ with product order, whereby we write
$i\to j$ for such an index in $\mathcal{I}\times\mathcal{J}$. The set
$[\mathcal{M}_{i}\to\mathcal{N}_{j}]$ consists of all (total) functions
$f:\mathcal{M}_{i}\to\mathcal{N}_{j}$ which preserve $\asymp$, i.e., which
satisfy $f(a_{i})\asymp f(b_{i})$ for $a_{i}\asymp b_{i}$. If the relations
$\stackrel{{\scriptstyle p}}{{\mapsto}}$ are partial functions on
$\mathcal{M}_{\mathcal{I}}$ and $\mathcal{N}_{\mathcal{J}}$, then $\asymp$ is
the identity on $\mathcal{M}_{i}$ and $\mathcal{N}_{j}$ and
$[\mathcal{M}_{i}\to\mathcal{N}_{j}]$ simply consists of all functions from
$\mathcal{M}_{i}$ to $\mathcal{N}_{j}$.

Let $f\in[\mathcal{M}_{i}\to\mathcal{N}_{j}]$,
$f^{\prime}\in[\mathcal{M}_{i^{\prime}}\to\mathcal{N}_{j^{\prime}}]$ and $i\to
j\leq i^{\prime}\to j^{\prime}$, i.e., $i\leq i^{\prime}$ and $j\leq
j^{\prime}$. The basic relation $\stackrel{{\scriptstyle p}}{{\mapsto}}$ on
the function space is a logical relation [12]. It is thus defined as

$f^{\prime}\stackrel{{\scriptstyle p}}{{\mapsto}}f\ :\\!\iff\
a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}\text{ implies
}f^{\prime}(a_{i^{\prime}})\stackrel{{\scriptstyle p}}{{\mapsto}}f(a_{i})$

for all $a_{i^{\prime}}\in\mathcal{M}_{i^{\prime}}$ and
$a_{i}\in\mathcal{M}_{i}$. The embedding-projection pair for the function
space is defined in the usual way:

$\displaystyle emb_{i\to j}^{i^{\prime}\to
j^{\prime}}:[\mathcal{M}_{i}\to\mathcal{N}_{j}]\to[\mathcal{M}_{i^{\prime}}\to\mathcal{N}_{j^{\prime}}]$
$\displaystyle\quad f\mapsto emb_{j}^{j^{\prime}}\circ f\circ
proj_{i}^{i^{\prime}},$ $\displaystyle proj_{i\to j}^{i^{\prime}\to
j^{\prime}}:[\mathcal{M}_{i^{\prime}}\to\mathcal{N}_{j^{\prime}}]\to[\mathcal{M}_{i}\to\mathcal{N}_{j}]$
$\displaystyle\quad f^{\prime}\mapsto proj_{j}^{j^{\prime}}\circ
f^{\prime}\circ emb_{i}^{i^{\prime}}.$

######  Proposition 2.8.

If $\mathcal{M}_{\mathcal{I}}$ and $\mathcal{N}_{\mathcal{J}}$ are both factor
systems, so is their function space. Moreover,

  1. 1.

If $\stackrel{{\scriptstyle p}}{{\mapsto}}$ satisfies (Fun) or (Stab) on
$\mathcal{N}_{\mathcal{J}}$, so does $\stackrel{{\scriptstyle p}}{{\mapsto}}$
on $[\mathcal{M}_{\mathcal{I}}\to\mathcal{N}_{\mathcal{J}}]$.

  2. 2.

If $\mathcal{M}_{\mathcal{I}}$ is inverse and $\mathcal{N}_{\mathcal{J}}$
direct, then $[\mathcal{M}_{\mathcal{I}}\to\mathcal{N}_{\mathcal{J}}]$ is
direct.

  3. 3.

If $\mathcal{M}_{\mathcal{I}}$ is direct and $\mathcal{N}_{\mathcal{J}}$
inverse, then $[\mathcal{M}_{\mathcal{I}}\to\mathcal{N}_{\mathcal{J}}]$ is
inverse.

######  Proof 2.9.

This has been proven in [5], except for the statements about (Stab) and about
direct and inverse factor systems. Assume $f^{\prime}\stackrel{{\scriptstyle
p}}{{\mapsto}}f\asymp g$ for
$f^{\prime}\in[\mathcal{M}_{i^{\prime}}\to\mathcal{N}_{j^{\prime}}]$ and
$f,g\in[\mathcal{M}_{i}\to\mathcal{N}_{j}]$, $i\to j\leq i^{\prime}\to
j^{\prime}$, so that we have to show $f^{\prime}\stackrel{{\scriptstyle
p}}{{\mapsto}}g$. Let $a_{i^{\prime}}\stackrel{{\scriptstyle
p}}{{\mapsto}}a_{i}$, and to confirm that
$f^{\prime}(a_{i^{\prime}})\stackrel{{\scriptstyle p}}{{\mapsto}}g(a_{i})$,
use the stability condition on $\mathcal{N}_{\mathcal{J}}$ applied to
$f^{\prime}(a_{i^{\prime}})\stackrel{{\scriptstyle
p}}{{\mapsto}}f(a_{i})\asymp g(a_{i})$.

Next, let $\mathcal{M}_{\mathcal{I}}$ be inverse and
$\mathcal{N}_{\mathcal{J}}$ direct. Assume first that
$f^{\prime}\stackrel{{\scriptstyle p}}{{\mapsto}}f$ with
$f^{\prime}\in[\mathcal{M}_{i^{\prime}}\to\mathcal{N}_{j^{\prime}}]$,
$f\in[\mathcal{M}_{i}\to\mathcal{N}_{j}]$ and $i\to j\leq i^{\prime}\to
j^{\prime}$. We wish to show that $f^{\prime}\asymp emb_{i\to
j}^{i^{\prime}\to j^{\prime}}(f)$, which is the same as $f^{\prime}\asymp
emb_{j}^{j^{\prime}}\circ f\circ proj_{i}^{i^{\prime}}$. Let
$a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}b_{i^{\prime}}$ and
define $b_{i}:=proj_{i}^{i^{\prime}}(b_{i^{\prime}})$. Then
$proj_{i}^{i^{\prime}}(a_{i^{\prime}})\asymp b_{i}$ since projections preserve
$\asymp$. It follows that $a_{i^{\prime}}\stackrel{{\scriptstyle
p}}{{\mapsto}}b_{i}$ since $\mathcal{M}_{\mathcal{I}}$ is inverse, and thus
$f^{\prime}(a_{i^{\prime}})\stackrel{{\scriptstyle p}}{{\mapsto}}f(b_{i})$.
Consequently, $f^{\prime}(a_{i^{\prime}})\asymp
emb_{j}^{j^{\prime}}(f(b_{i}))=emb_{j}^{j^{\prime}}\circ f\circ
proj_{i}^{i^{\prime}}(b_{i^{\prime}})$, since $\mathcal{N}_{\mathcal{J}}$ is
direct.

For the other direction assume $f^{\prime}\asymp emb_{j}^{j^{\prime}}\circ
f\circ proj_{i}^{i^{\prime}}$ and let $a_{i^{\prime}}\stackrel{{\scriptstyle
p}}{{\mapsto}}a_{i}$. We shall prove that
$f^{\prime}(a_{i^{\prime}})\stackrel{{\scriptstyle p}}{{\mapsto}}f(a_{i})$.
Then $a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}$ implies
$proj_{i}^{i^{\prime}}(a_{i^{\prime}})\asymp a_{i}$ since
$\mathcal{M}_{\mathcal{I}}$ is inverse. Now $f$ and the embeddings preserve
$\asymp$, so
$emb_{j}^{j^{\prime}}(f(proj_{i}^{i^{\prime}}(a_{i^{\prime}})))\asymp
emb_{j}^{j^{\prime}}(f(a_{i}))$. Certainly $f^{\prime}(a_{i^{\prime}})\asymp
emb_{j}^{j^{\prime}}(f(a_{i}))$. This shows
$f^{\prime}(a_{i^{\prime}})\stackrel{{\scriptstyle p}}{{\mapsto}}f(a_{i})$,
since $\mathcal{N}_{\mathcal{J}}$ is direct, as claimed. The proof of the last
statement is verified in a similar way.

###  2.3 Targets and Limits

The subsequent concepts require sets $\mathfrak{D}(\mathcal{I})$ from Section
1.2 with Property (Filter), whereby we write $\mathfrak{D}_{\varrho}$ for
$\mathfrak{D}(\mathcal{I}_{\varrho})$ and $\mathfrak{D}_{\Gamma}$ for
$\mathfrak{D}(\mathcal{I}_{\Gamma})$. A _target_
$(\mathcal{M},\stackrel{{\scriptstyle p}}{{\longmapsto}})$ for a system
$\mathcal{M}_{\mathcal{I}}$ extends the system “at the top”, i.e., the
extension leads to a system $\mathcal{M}_{\bar{\mathcal{I}}}$, called
_compactification_ of $\mathcal{M}_{\mathcal{I}}$, with index set
$\bar{\mathcal{I}}:=\mathcal{I}\cup\\{top\\}$, $top$ as greatest index, and
$\mathcal{M}_{top}=\mathcal{M}$. Let $a\stackrel{{\scriptstyle
p}}{{\longmapsto}}a_{i}$ denote $a\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}$
provided that $a\in\mathcal{M}$, and we also write $Emb_{i}$ for
$emb_{i}^{top}$ and $Proj_{i}$ for $proj_{i}^{top}$. Relation
$\stackrel{{\scriptstyle p}}{{\mapsto}}$ on a target $\mathcal{M}$, and
consequently relation $\asymp$ on $\mathcal{M}$ as well, is by definition the
identity. The _extension_ of an element $a\in\mathcal{M}$ is
$Ext(a):=\\{a_{i}\in\bigcup_{i\in\mathcal{I}}\mathcal{M}_{i}\mid
a\stackrel{{\scriptstyle p}}{{\longmapsto}}a_{i}\\}$. A target $\mathcal{M}$
for a system $\mathcal{M}_{\mathcal{I}}$ satisfies by definition

$\mathcal{I}_{a}:=\\{i\in\mathcal{I}\mid\exists a_{i}\in\mathcal{M}_{i}\
a\stackrel{{\scriptstyle
p}}{{\longmapsto}}a_{i}\\}\in\mathfrak{D}(\mathcal{I})$

for all objects $a\in\mathcal{M}$. Moreover, if the system is a prefactor
system, a prefactor system with embeddings/projections or a factor system,
then the compactification $\mathcal{M}_{\bar{\mathcal{I}}}$ must have this
additional structure with its properties as well. Whereas the compactification
of a system is automatically a system, the compactification of a _prefactor
system_ requires for all $a\in\mathcal{M}$, $a_{i}\in\mathcal{M}_{i}$,
$a_{i^{\prime}}\in\mathcal{M}_{i^{\prime}}$ and $i\leq i^{\prime}$

$a\stackrel{{\scriptstyle
p}}{{\longmapsto}}a_{i^{\prime}},\,a\stackrel{{\scriptstyle
p}}{{\longmapsto}}a_{i}\ \Rightarrow\ a_{i^{\prime}}\stackrel{{\scriptstyle
p}}{{\mapsto}}a_{i}.$ (2)

If $\mathcal{M}$ is a target for a _prefactor system with embeddings_
$\mathcal{M}_{\mathcal{I}}$, then this implies the existence of
$\asymp$-embeddings $Emb_{i}:\mathcal{M}_{i}\to\mathcal{M}$, satisfying
$Emb_{i^{\prime}}(emb_{i}^{i^{\prime}}(a_{i}))=Emb_{i}(a_{i})$ and

$a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}\ \Rightarrow\
Emb_{i^{\prime}}(a_{i^{\prime}})\stackrel{{\scriptstyle
p}}{{\longmapsto}}a_{i}\text{ for all }i\leq i^{\prime},$ (3)

$a_{i}\in\mathcal{M}_{i}$, $a_{i^{\prime}}\in\mathcal{M}_{i^{\prime}}$ and
$a\in\mathcal{M}$. If $\mathcal{M}$ is a target for a _prefactor system with
projections_ $\mathcal{M}_{\mathcal{I}}$, then there are moreover
$\asymp$-projections $Proj_{i}:\mathcal{M}\to\mathcal{M}_{i}$ such that
$proj_{i}^{i^{\prime}}(Proj_{i^{\prime}}(a))\asymp Proj_{i}(a)$ and

$a\stackrel{{\scriptstyle p}}{{\longmapsto}}a_{i}\ \Rightarrow\
Proj_{i^{\prime}}(a)\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}\text{ for all
}i\leq i^{\prime}.$ (4)

If $\mathcal{M}$ is a target for a _factor system_ , then $Emb$ and $Proj$
with these properties exist and both form a $\asymp$-embedding-projection
pair. We write $(\mathcal{M},\stackrel{{\scriptstyle p}}{{\longmapsto}})$,
$(\mathcal{M},\stackrel{{\scriptstyle p}}{{\longmapsto}},Emb)$,
$(\mathcal{M},\stackrel{{\scriptstyle p}}{{\longmapsto}},Proj)$ and
$(\mathcal{M},\stackrel{{\scriptstyle p}}{{\longmapsto}},Emb,Proj)$,
respectively, for these targets. If $\mathcal{M}$ is a target for a prefactor
system with projections $\mathcal{M}_{\mathcal{I}}$, then the projections
$Proj_{i}$ can be defined by

$Proj_{i}(a):=proj_{i}^{i^{\prime}}(a_{i^{\prime}})\text{ for some
}i^{\prime}\geq i\text{ with }a\stackrel{{\scriptstyle
p}}{{\longmapsto}}a_{i^{\prime}}$ (5)

for $a\in\mathcal{M}$. It follows from the properties of a prefactor system
that $Proj_{i}(a)$ is unique modulo $\asymp$. Since
$Emb_{i^{\prime}}(a_{i^{\prime}})\stackrel{{\scriptstyle
p}}{{\longmapsto}}a_{i^{\prime}}$ for
$a_{i^{\prime}}\in\mathcal{M}_{i^{\prime}}$ by (3), we have for $i\leq
i^{\prime}$

$Proj_{i}(Emb_{i^{\prime}}(a_{i^{\prime}}))\asymp
proj_{i}^{i^{\prime}}(a_{i^{\prime}}).$ (6)

A target $(\mathcal{M},\stackrel{{\scriptstyle p}}{{\longmapsto}})$ for a
system $\mathcal{M}_{\mathcal{I}}$ is a _limit_ of $\mathcal{M}_{\mathcal{I}}$
iff for every further target $(\mathcal{N},\stackrel{{\scriptstyle
q}}{{\longmapsto}})$ for $\mathcal{M}_{\mathcal{I}}$ there is a unique map
$\Phi:\mathcal{N}\to\mathcal{M}$ such that $a\stackrel{{\scriptstyle
q}}{{\longmapsto}}a_{i}$ implies $\Phi(a)\stackrel{{\scriptstyle
p}}{{\longmapsto}}a_{i}$. If the underlying system is a factor system or a
prefactor system, then we call the limit _factor limit_ and _prefactor limit_
, resp. It turns out, however, that a factor limit is the same as the
prefactor limit, and that this limit
$\underline{\textrm{lim}}(\mathcal{M}_{\mathcal{I}})$ is unique modulo
isomorphism. Therefore we simply speak of a _limit_ , or a _limit set_ , if we
want to distinguish it from a _limit element_ in this limit set.

######  Example 2.10.

Recall Example 2.3. If a direct system is also a direct factor system and
$a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}:\\!\iff
emb_{i}^{i^{\prime\prime}}(a_{i})=emb_{i^{\prime}}^{i^{\prime\prime}}(a_{i^{\prime}})$
for some $i^{\prime\prime}\geq i,i^{\prime}$, then the factor limit is the
direct limit, i.e.,
$\underline{\textrm{lim}}(\mathcal{M}_{\mathcal{I}})=\varinjlim(\mathcal{M}_{\mathcal{I}})$.
If an inverse system is additionally an inverse factor system and
$a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}:\\!\iff
proj_{i}^{i^{\prime}}(a_{i^{\prime}})=a_{i}$, then the factor limit
$\underline{\textrm{lim}}(\mathcal{M}_{\mathcal{I}})$ is the inverse limit
$\varprojlim(\mathcal{M}_{\mathcal{I}})$.

In the first case of Example 2.4 the limit is $\mathbb{N}$ (which is the
direct limit as well as the factor limit). In the second case the limit
(inverse limit and factor limit) is
$\mathbb{N}_{\infty}:=\mathbb{N}\cup\\{\infty\\}$ with $\infty=(0,1,2,\dots)$.
In the third case the factor limit is a singleton set, which is neither the
direct nor the inverse limit.

###  2.4 Consistent Sets and Dynamic Elements

It is possible to define concrete targets and limits in the form of sets of
states: A set $\alpha\subseteq\bigcup_{i\in\mathcal{I}}\mathcal{M}_{i}$ in a
system $\mathcal{M}_{\mathcal{I}}$ is called a _consistent set_ iff
$a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}$ holds for all
$a_{i^{\prime}},a_{i}\in\alpha$ with $i^{\prime}\geq i$, and
$\mathcal{I}_{\alpha}:=\\{i\in\mathcal{I}\mid\alpha\cap\mathcal{M}_{i}\not=\emptyset\\}\in\mathfrak{D}(\mathcal{I})$.
If we already have a target $\mathcal{M}$ for a prefactor system, then the set
$Ext(a)$ is such a consistent set for all $a\in\mathcal{M}$. The set of all
consistent sets in a (pre)factor system $\mathcal{M}_{\mathcal{I}}$ is itself
a target for $\mathcal{M}_{\mathcal{I}}$ with $\alpha\stackrel{{\scriptstyle
p}}{{\longmapsto}}a_{i}:\\!\iff a_{i}\in\alpha$. In other words, if
$\mathcal{M}$ denotes the set of all consistent sets, then the target is
$(\mathcal{M},\ni)$.

A _dynamic element_ is a maximal (w.r.t. subset inclusion) consistent set, and
for each consistent set $\alpha$ in a prefactor system there is exactly one
dynamic element $\alpha^{m}$ such that $\alpha\subseteq\alpha^{m}$. Let
$\mathcal{E}\mathcal{L}(\mathcal{M}_{\mathcal{I}})$ denote the set of all of
these dynamic elements, then

$(\mathcal{E}\mathcal{L}(\mathcal{M}_{\mathcal{I}}),\ni)$ (7)

is a prefactor limit of $\mathcal{M}_{\mathcal{I}}$. For the next two lemmata,
recall that it is assumed that $\mathfrak{D}(\mathcal{I})$ is a filter as
defined in (Filter).

######  Lemma 2.11.

Let $\alpha$ be a consistent set in a prefactor system
$(\mathcal{M}_{\mathcal{I}},\stackrel{{\scriptstyle p}}{{\mapsto}})$ and
$b_{i}\in\mathcal{M}_{i}$, then the following are equivalent:

  1. 1.

$b_{i}\in\alpha^{m}$.

  2. 2.

$\alpha\cup\\{b_{i}\\}$ is a consistent set.

  3. 3.

There are cofinal many $i^{\prime}\in\mathcal{I}$ with
$a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}b_{i}$ for some
$a_{i^{\prime}}\in\alpha$.

  4. 4.

$a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}b_{i}$ for all
$a_{i^{\prime}}\in\alpha$ with $i^{\prime}\geq i$.

  5. 5.

There are $\mathfrak{D}$-many $i^{\prime}\in\mathcal{I}$ with
$a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}b_{i}$ for some
$a_{i^{\prime}}\in\alpha$.

######  Proof 2.12.

This has been shown in [5], except the last clause. For its equivalence to the
other statements notice that it follows from Clause 4. since
$\mathcal{I}_{\alpha}\,\cap\\!\,\uparrow\\!i\in\mathfrak{D}(\mathcal{I})$, and
it implies Clause 3. since each set in $\mathfrak{D}(\mathcal{I})$ is cofinal.

######  Lemma 2.13.

Let $\alpha$ and $\beta$ be consistent sets in a prefactor system
$(\mathcal{M}_{\mathcal{I}},\stackrel{{\scriptstyle p}}{{\mapsto}})$, then the
following are equivalent:

  1. 1.

$\alpha^{m}=\beta^{m}$.

  2. 2.

$a_{i}\asymp b_{i}$ for all $i\in\mathcal{I}$ with $a_{i}\in\alpha$ and
$b_{i}\in\beta$.

  3. 3.

$a_{i}\asymp b_{j}$ for all $i,j\in\mathcal{I}$ with $a_{i}\in\alpha$ and
$b_{j}\in\beta$.

######  Proof 2.14.

The equivalence of 1. and 3. has been shown in [5], so it suffices to prove
that 2. implies $b_{i}\in\alpha^{m}$ for each $b_{i}\in\beta$. We wish to find
cofinal many $a_{i^{\prime}}\in\alpha$ with
$a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}b_{i}$ and apply Lemma
2.11. There are $\mathfrak{D}$-many $i^{\prime}\geq i$ with
$i^{\prime}\in\mathcal{I}_{\alpha}\cap\mathcal{I}_{\beta}$. For all
$a_{i^{\prime}}\in\alpha$, $b_{i^{\prime}}\in\beta$ we have
$a_{i^{\prime}}\asymp b_{i^{\prime}}$ by assumption, hence
$a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}b_{i}$, since
$b_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}b_{i}$.

If one, and hence all, of the conditions in Lemma 2.13 are true, then we write
$\alpha\sim\beta$. Call an element $a\in\mathcal{M}$ of a target $\mathcal{M}$
for a prefactor system $\mathcal{M}_{\mathcal{I}}$ a _limit (element)_ of a
consistent set $\alpha$ iff $\alpha\sim Ext(a)$. Obviously, $a$ is a limit of
its extension $Ext(a)$. If there is only one limit element, we denote it as
$lim(\alpha)$.

Given a factor system $\mathcal{M}_{\mathcal{I}}$. Then
$\mathcal{E}\mathcal{L}(\mathcal{M}_{\mathcal{I}})$ is, up to isomorphism, the
limit $\underline{\textrm{lim}}(\mathcal{M}_{\mathcal{I}})$, whereby
projections have been defined by (5) and embeddings are

$\displaystyle Emb_{i}(a_{i})$
$\displaystyle:=\\{emb_{i}^{i^{\prime}}(a_{i})\in\bigcup_{j\in\mathcal{I}}\mathcal{M}_{j}\mid
i^{\prime}\geq i\\}^{m}.$ (8)

Let $\mathcal{M}$ be a target for a system $\mathcal{M}_{\mathcal{I}}$, then
$\mathcal{M}$ is _maximal (over $\mathcal{M}_{\mathcal{I}}$)_ iff
$Ext(a)\in\mathcal{E}\mathcal{L}(\mathcal{M}_{\mathcal{I}})$ for all
$a\in\mathcal{M}$. $\mathcal{M}$ is _extensional (over
$\mathcal{M}_{\mathcal{I}}$)_ iff $Ext(a)\sim Ext(b)$ implies $a=b$ for all
$a,b\in\mathcal{M}$. $\mathcal{M}$ is _complete (over
$\mathcal{M}_{\mathcal{I}}$)_ iff for all consistent sets $\alpha$ there is a
limit element $a$, i.e., some $a\in\mathcal{M}$ with $Ext(a)\sim\alpha$. One
can characterize a limit $\underline{\textrm{lim}}(\mathcal{M}_{\mathcal{I}})$
also as a target that is maximal, extensional and complete over
$\mathcal{M}_{\mathcal{I}}$.

######  Proposition 2.15.

Assume a prefactor system $\mathcal{M}_{\mathcal{I}}$ has been compactified
with a target $\mathcal{M}$, yielding the extended prefactor system
$\mathcal{M}_{\bar{\mathcal{I}}}$.

  1. 1.

If $\mathcal{M}_{\mathcal{I}}$ is stable and $\mathcal{M}$ maximal over
$\mathcal{M}_{\mathcal{I}}$, then $\mathcal{M}_{\bar{\mathcal{I}}}$ is stable,
too.

  2. 2.

If $\mathcal{M}_{\mathcal{I}}$ is direct and $\mathcal{M}$ extensional over
$\mathcal{M}_{\mathcal{I}}$, then $\mathcal{M}_{\bar{\mathcal{I}}}$ is direct
and $\mathcal{I}_{a}$ contains an up-set for all $a\in\mathcal{M}$.

  3. 3.

If $\mathcal{M}_{\mathcal{I}}$ is inverse and $\mathcal{M}$ maximal over
$\mathcal{M}_{\mathcal{I}}$, then $\mathcal{M}_{\bar{\mathcal{I}}}$ is inverse
and $\mathcal{I}_{a}=\mathcal{I}$ for all $a\in\mathcal{M}$.

######  Proof 2.16.

1\. In order to show stability of $\mathcal{M}_{\bar{\mathcal{I}}}$ it
suffices to prove that $a\stackrel{{\scriptstyle p}}{{\longmapsto}}a_{i}\asymp
b_{i}$ implies $a\stackrel{{\scriptstyle p}}{{\longmapsto}}b_{i}$ for all
$a\in\mathcal{M}$. Indeed, there are cofinal many indices $i^{\prime}\geq i$
with $a\stackrel{{\scriptstyle p}}{{\longmapsto}}a_{i^{\prime}}$, and
consequently $a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}$.
Applying (Stab) yields $a_{i^{\prime}}\stackrel{{\scriptstyle
p}}{{\mapsto}}b_{i}$ for cofinal many indices $i^{\prime}\in\mathcal{I}$. By
Lemma 2.11 $a\stackrel{{\scriptstyle p}}{{\longmapsto}}b_{i}$ follows, since
$Ext(a)$ is a maximal consistent set.

2\. We claim that $a\stackrel{{\scriptstyle p}}{{\longmapsto}}a_{i}\iff
a=Emb_{i}(a_{i})$ for $a\in\mathcal{M}$. So assume $a\stackrel{{\scriptstyle
p}}{{\longmapsto}}a_{i}$ and we first establish that $a\stackrel{{\scriptstyle
p}}{{\longmapsto}}a_{j}$ implies $Emb_{i}(a_{i})\stackrel{{\scriptstyle
p}}{{\longmapsto}}a_{j}$ for all $j\in\mathcal{I}$. There are cofinal many
$i^{\prime}\geq i,j$ with $a\stackrel{{\scriptstyle
p}}{{\longmapsto}}a_{i^{\prime}}$, $a_{i^{\prime}}\stackrel{{\scriptstyle
p}}{{\mapsto}}a_{i}$ and $a_{i^{\prime}}\stackrel{{\scriptstyle
p}}{{\mapsto}}a_{j}$, hence $a_{i^{\prime}}\asymp
emb_{i}^{i^{\prime}}(a_{i})$, because $\mathcal{M}_{\mathcal{I}}$ is direct.
It follows that $emb_{i}^{i^{\prime}}(a_{i})\stackrel{{\scriptstyle
p}}{{\mapsto}}a_{j}$ for cofinal many indices $i^{\prime}\in\mathcal{I}$ and
thus $Emb_{i}(a_{i})\stackrel{{\scriptstyle p}}{{\longmapsto}}a_{j}$. This
proves $Ext(a)\sim Ext(Emb_{i}(a_{i}))$, so $a$ and $Emb_{i}(a_{i})$ are equal
since $\mathcal{M}$ is extensional over $\mathcal{M}_{\mathcal{I}}$. The
inverse implication $a=Emb_{i}(a_{i})\Rightarrow a\stackrel{{\scriptstyle
p}}{{\longmapsto}}a_{i}$ holds trivially. Moreover, $a=Emb_{i}(a_{i})$ for
$a\in\mathcal{M}$ implies that $\mathcal{I}_{a}$ contains the up-set
$\\!\,\uparrow\\!i$.

3\. We shall prove that $a\stackrel{{\scriptstyle p}}{{\longmapsto}}a_{i}\iff
Proj_{i}(a)\asymp a_{i}$. For the forward implication assume
$Proj_{i}(a)=proj_{i}^{i^{\prime}}(a_{i^{\prime}})$ for some $a_{i^{\prime}}$
with $a\stackrel{{\scriptstyle p}}{{\longmapsto}}a_{i^{\prime}}$. We establish
that $proj_{i}^{i^{\prime}}(a_{i^{\prime}})\asymp a_{i}$ for
$a\stackrel{{\scriptstyle p}}{{\longmapsto}}a_{i}$ by using the fact that
$\mathcal{M}_{\mathcal{I}}$ is inverse and that $a\stackrel{{\scriptstyle
p}}{{\longmapsto}}a_{i^{\prime}}$ and $a\stackrel{{\scriptstyle
p}}{{\longmapsto}}a_{i}$ implies $a_{i^{\prime}}\stackrel{{\scriptstyle
p}}{{\mapsto}}a_{i}$.

For the backward implication assume
$Proj_{i}(a)=proj_{i}^{i^{\prime}}(a_{i^{\prime}})\asymp a_{i}$. To show
$a\stackrel{{\scriptstyle p}}{{\longmapsto}}a_{i}$ it suffices to find cofinal
many indices $i^{\prime\prime}\geq i^{\prime}$ with $a\stackrel{{\scriptstyle
p}}{{\longmapsto}}a_{i^{\prime\prime}}$ and
$a_{i^{\prime\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}$. To this
aim, we use maximality of $\mathcal{M}$. Indeed, there are cofinal many
indices $i^{\prime\prime}\geq i^{\prime}$ with $a\stackrel{{\scriptstyle
p}}{{\longmapsto}}a_{i^{\prime\prime}}$, and to confirm that
$a_{i^{\prime\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}$ it suffices
to prove $proj_{i}^{i^{\prime\prime}}(a_{i^{\prime\prime}})\asymp a_{i}$. Now
$a_{i^{\prime\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i^{\prime}}$ is
a consequence of $a\stackrel{{\scriptstyle
p}}{{\longmapsto}}a_{i^{\prime\prime}}$ and $a\stackrel{{\scriptstyle
p}}{{\longmapsto}}a_{i^{\prime}}$, hence
$proj_{i^{\prime}}^{i^{\prime\prime}}(a_{i^{\prime\prime}})\asymp
a_{i^{\prime}}$. Because $\asymp$-projections preserve $\asymp$, we deduce
$proj_{i}^{i^{\prime\prime}}(a_{i^{\prime\prime}})\asymp
proj_{i}^{i^{\prime}}(proj_{i^{\prime}}^{i^{\prime\prime}}(a_{i^{\prime\prime}}))\asymp
proj_{i}^{i^{\prime}}(a_{i^{\prime}})\asymp a_{i}$, as claimed. For all
$i\in\mathcal{I}$ there is some $a_{i}$ with $a\stackrel{{\scriptstyle
p}}{{\longmapsto}}a_{i}\asymp Proj_{i}(a)$, hence
$\mathcal{I}_{\alpha}=\mathcal{I}$.

######  Corollary 2.17.

Assume a prefactor system $\mathcal{M}_{\mathcal{I}}$ has been compactified
with a limit $\mathcal{M}$, yielding the extended prefactor system
$\mathcal{M}_{\bar{\mathcal{I}}}$. If $\mathcal{M}_{\mathcal{I}}$ is stable
(direct, inverse), then $\mathcal{M}_{\bar{\mathcal{I}}}$ is also stable
(direct, inverse resp.).

###  2.5 Targets and Limits on the Function Space

Consider two factor systems $\mathcal{M}_{\mathcal{I}}$ and
$\mathcal{N}_{\mathcal{J}}$ with limits $\mathcal{M}$ and $\mathcal{N}$ resp.
Then

$[\mathcal{M}\to_{\mathfrak{D}}\mathcal{N}]:=\\{f:\mathcal{M}\to\mathcal{N}\mid\mathcal{I}_{f}\in\mathfrak{D}(\mathcal{I}\times\mathcal{J})\\}$

is a target for $[\mathcal{M}_{\mathcal{I}}\to\mathcal{N}_{\mathcal{J}}]$, but
not necessarily a limit. We now state a condition which guarantees that
$[\mathcal{M}\to_{\mathfrak{D}}\mathcal{N}]$ is indeed a limit. So let $\zeta$
be a consistent set on the factor system
$[\mathcal{M}_{\mathcal{I}}\to\mathcal{N}_{\mathcal{J}}]$, and $\alpha$ a
consistent set on the factor system $\mathcal{M}_{\mathcal{I}}$. Define

$App(\zeta,\alpha):=\zeta(\alpha):=\\{f_{i\to j}(a_{i})\mid f_{i\to
j}\in\zeta\text{ and }a_{i}\in\alpha\\}.$ (Appl)

It is easy to see that this set satisfies
$b_{j^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}b_{j}$ for all $j\leq
j^{\prime}$ and $b_{j},b_{j^{\prime}}\in\zeta(\alpha)$. However,
$\zeta(\alpha)$ is not necessarily a consistent set. For that,
$\mathcal{I}_{f}[\mathcal{I}_{a}]\in\mathfrak{D}(\mathcal{J})$ must be the
case, whereby
$\mathcal{H}[\mathcal{I}^{\prime}]:=\\{j\in\mathcal{J}\mid\exists
i\in\mathcal{I}^{\prime}\ i\to j\in\mathcal{H}\\}$ for
$\mathcal{H}\subseteq\mathcal{I}\times\mathcal{J}$ and
$\mathcal{I}^{\prime}\subseteq\mathcal{I}$. This is ensured when the following
condition for $\mathfrak{D}$ is met for all sets $\mathcal{I}$ and
$\mathcal{J}$:

$\mathcal{H}\in\mathfrak{D}(\mathcal{I}\times\mathcal{J})\text{ and
}\mathcal{I}^{\prime}\in\mathfrak{D}(\mathcal{I})\text{ implies
}\mathcal{H}[\mathcal{I}^{\prime}]\in\mathfrak{D}(\mathcal{J}).$ (D)

We will require Condition (D) for the rest of this paper.

######  Lemma 2.18.

The application defined by (Appl) is extensional, i.e., for all
$\zeta,\zeta^{\prime}\in\mathcal{E}\mathcal{L}([\mathcal{M}_{\mathcal{I}}\to\mathcal{N}_{\mathcal{J}}])$
we have:

$\zeta(\alpha)=\zeta^{\prime}(\alpha)\text{ for all
}\alpha\in\mathcal{E}\mathcal{L}(\mathcal{M}_{\mathcal{I}})\ \text{ implies }\
\zeta=\zeta^{\prime}.$

######  Proof 2.19.

Assume $\zeta(\alpha)=\zeta^{\prime}(\alpha)$ for all
$\alpha\in\mathcal{E}\mathcal{L}(\mathcal{M}_{\mathcal{I}})$ and let $f_{i\to
j}\in\zeta$. We will show that $f_{i\to j}\in\zeta^{\prime}$, which proves the
lemma. Choose indices $i^{\prime}\to
j^{\prime}\in\mathcal{I}_{\zeta}\cap\,\mathcal{I}_{\zeta^{\prime}}\,\cap\\!\,\uparrow\\!(i\to
j)\in\mathfrak{D}(\mathcal{I}\times\mathcal{J})$ and let
$f^{\prime}_{i^{\prime}\to j^{\prime}}\in\zeta^{\prime}$. We wish to show
$f^{\prime}_{i^{\prime}\to j^{\prime}}\stackrel{{\scriptstyle
p}}{{\mapsto}}f_{i\to j}$. Since this is the case for $\mathfrak{D}$-many
indices $i^{\prime}\to j^{\prime}$, we have shown $f_{i\to
j}\in\zeta^{\prime}$ by Lemma 2.11, which suffices.

Now assume $a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}$ for
$a_{i^{\prime}}\in\mathcal{M}_{i^{\prime}}$ and $a_{i}\in\mathcal{M}_{i}$, so
that we have to prove $f^{\prime}_{i^{\prime}\to
j^{\prime}}(a_{i^{\prime}})\stackrel{{\scriptstyle p}}{{\mapsto}}f_{i\to
j}(a_{i})$. For
$\alpha:=Emb_{i^{\prime}}(a_{i^{\prime}})\in\mathcal{E}\mathcal{L}(\mathcal{M}_{\mathcal{I}})$
we know that $a_{i}\in\alpha$, by maximality and (3). Further,
$f^{\prime}_{i^{\prime}\to
j^{\prime}}(a_{i^{\prime}})\in\zeta^{\prime}(\alpha)=\zeta(\alpha)$ and
$f_{i\to j}(a_{i})\in\zeta(\alpha)$ implies $f^{\prime}_{i^{\prime}\to
j^{\prime}}(a_{i^{\prime}})\stackrel{{\scriptstyle p}}{{\mapsto}}f_{i\to
j}(a_{i})$, because $\zeta(\alpha)$ is a consistent set.

######  Proposition 2.20.

Let $\mathcal{M}$ and $\mathcal{N}$ be a targets for the factor systems
$\mathcal{M}_{\mathcal{I}}$ and $\mathcal{N}_{\mathcal{J}}$ resp. Assume
Condition (D) holds. If $\mathcal{N}$ is maximal (extensional, complete) over
$\mathcal{N}_{\mathcal{J}}$, so is
$[\mathcal{M}\to_{\mathfrak{D}}\mathcal{N}]$ over
$[\mathcal{M}_{\mathcal{I}}\to\mathcal{N}_{\mathcal{J}}]$.

######  Proof 2.21.

First we shall prove the claim about maximality, so let $g_{i\to
j}\in\mathcal{M}_{i\to j}$ and we apply Lemma 2.11. Assume there is a set
$\mathcal{H}\in\mathfrak{D}(\mathcal{I}\times\mathcal{J})$ with
$f\stackrel{{\scriptstyle p}}{{\longmapsto}}f_{i^{\prime}\to
j^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}g_{i\to j}$ for
$i^{\prime}\to j^{\prime}\in\mathcal{H}$, then it suffices to show
$f\stackrel{{\scriptstyle p}}{{\longmapsto}}g_{i\to j}$. By the definition of
$\stackrel{{\scriptstyle p}}{{\longmapsto}}$ it must be checked that

$f(a)\stackrel{{\scriptstyle p}}{{\longmapsto}}g_{i\to j}(a_{i})\ \text{ for
}\ a\stackrel{{\scriptstyle p}}{{\longmapsto}}a_{i}.$

There are $\mathfrak{D}$-many indices $i^{\prime}\geq i$ with
$a\stackrel{{\scriptstyle p}}{{\longmapsto}}a_{i^{\prime}}$, since
$\mathcal{I}_{a}\,\cap\\!\,\uparrow\\!i\in\mathfrak{D}(\mathcal{I})$. They
satisfy $a_{i^{\prime}}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}$, because
$a\stackrel{{\scriptstyle p}}{{\longmapsto}}a_{i^{\prime}}$ and
$a\stackrel{{\scriptstyle p}}{{\longmapsto}}a_{i}$. Applying Condition (D)
give us $\mathfrak{D}$-many indices
$j^{\prime}\in\mathcal{H}[\mathcal{I}_{a}\,\cap\\!\,\uparrow\\!i]$, which all
satisfy $f(a)\stackrel{{\scriptstyle p}}{{\longmapsto}}f_{i^{\prime}\to
j^{\prime}}(a_{i^{\prime}})\stackrel{{\scriptstyle p}}{{\mapsto}}g_{i\to
j}(a_{i})$. So maximality of $\mathcal{N}$ yields $f(a)\stackrel{{\scriptstyle
p}}{{\longmapsto}}g_{i\to j}(a_{i})$, showing the maximality of
$[\mathcal{M}\to_{\mathfrak{D}}\mathcal{N}]$.

For extensionality we prove that $f=g$, provided $Ext(f)\sim Ext(g)$. So let
$a\in\mathcal{M}$ and we claim that $f(a)=g(a)$. For all $i\to
j\in\mathcal{I}_{f}\cap\mathcal{I}_{g}$ and $f_{i\to j}\in Ext(f)$, $g_{i\to
j}\in Ext(g)$ we have $f_{i\to j}\asymp g_{i\to j}$ by definition. Condition
(D) shows that

$\mathcal{J}^{\prime}:=(\mathcal{I}_{f}\cap\mathcal{I}_{g})[\mathcal{I}_{a}]\in\mathfrak{D}(\mathcal{J}),$

and for all these indices $i\in\mathcal{I}_{a}$ and $j\in\mathcal{J}^{\prime}$
we have $a\stackrel{{\scriptstyle p}}{{\longmapsto}}a_{i}$ for some
$a_{i}\in\mathcal{M}_{i}$, $f(a)\stackrel{{\scriptstyle
p}}{{\longmapsto}}f_{i\to j}(a_{i})$, $g(a)\stackrel{{\scriptstyle
p}}{{\longmapsto}}g_{i\to j}(a_{i})$ and $f_{i\to j}(a_{i})\asymp g_{i\to
j}(a_{i})$. This yields $Ext(f(a))\sim Ext(g(a))$, since the elements of
$Ext(f(a))$ and $Ext(g(a))$ are consistent (i.e., in $\asymp$-relation to each
other) for cofinal many indices $j\in\mathcal{J}$. We now appeal to
extensionality of $\mathcal{N}$ to get $f(a)=f(b)$.

To show completeness of $[\mathcal{M}\to_{\mathfrak{D}}\mathcal{N}]$ over
$[\mathcal{M}_{\mathcal{I}}\to\mathcal{N}_{\mathcal{J}}]$ let $\zeta$ be a
consistent set in $[\mathcal{M}_{\mathcal{I}}\to\mathcal{N}_{\mathcal{J}}]$.
We define a limit element $f:\mathcal{M}\to\mathcal{N}$ of $\zeta$ by

$f(a):=\text{ limit element of }\beta:=\\{g_{i\to j}(a_{i})\mid g_{i\to
j}\in\zeta\cap[\mathcal{M}_{i}\to\mathcal{N}_{j}]\text{ and
}a\stackrel{{\scriptstyle p}}{{\longmapsto}}a_{i}\\}$

for all $a\in\mathcal{M}$. This function is well-defined: If
$a\stackrel{{\scriptstyle p}}{{\longmapsto}}a_{i}$, $a\stackrel{{\scriptstyle
p}}{{\longmapsto}}b_{i}$ and $f_{i\to j},g_{i\to
j}\in\zeta\cap[\mathcal{M}_{i}\to\mathcal{N}_{j}]$, then $a_{i}\asymp b_{i}$
follows and consequently $f_{i\to j}(a_{i})\asymp g_{i\to j}(b_{i})$; note
that $a_{i}\asymp b_{i}\iff a_{i}\stackrel{{\scriptstyle p}}{{\mapsto}}b_{i}$
and the same for $f_{i\to j}(a_{i})\asymp g_{i\to j}(b_{i})$. This implies
that any two elements in $\beta$ are consistent. Condition (D) guarantees that
$\mathcal{I}_{f}=\mathcal{I}_{\zeta}[\mathcal{I}_{a}]\in\mathfrak{D}(\mathcal{J})$.
The set $\beta$ is thus a consistent set and completeness of $\mathcal{N}$
ensures that a limit element of $\beta$ exists.

We claim that $f$ is a limit of $\zeta$. Let $f\stackrel{{\scriptstyle
p}}{{\longmapsto}}f_{i\to j}$ and $g_{i\to j}\in\zeta$ with $f_{i\to
j},g_{i\to j}\in\mathcal{M}_{i\to j}$ and we have to show $f_{i\to
j}\stackrel{{\scriptstyle p}}{{\mapsto}}g_{i\to j}$. Given
$b_{i}\stackrel{{\scriptstyle p}}{{\mapsto}}a_{i}$, both in $\mathcal{M}_{i}$,
so it suffices to show that $f_{i\to j}(b_{i})\stackrel{{\scriptstyle
p}}{{\mapsto}}g_{i\to j}(a_{i})$. Take $a:=Emb_{i}(a_{i})=Emb_{i}(b_{i})$,
then $a\stackrel{{\scriptstyle p}}{{\longmapsto}}a_{i}$ and
$a\stackrel{{\scriptstyle p}}{{\longmapsto}}b_{i}$, hence
$f(a)\stackrel{{\scriptstyle p}}{{\longmapsto}}f_{i\to j}(b_{i})$ and $g_{i\to
j}(a_{i})\in\beta$. Since $f(a)$ is a limit element of $\beta$, it follows
that $\beta\sim Ext(f(a))$, and thus $f_{i\to j}(b_{i})\asymp g_{i\to
j}(a_{i})$ by Lemma 2.13, so we are done.

Recall that limits are targets which are maximal, extensional and complete.
Recall also that
$\mathcal{E}\mathcal{L}([\mathcal{M}_{\mathcal{I}}\to\mathcal{N}_{\mathcal{J}}])$
is a limit of $[\mathcal{M}_{\mathcal{I}}\to\mathcal{N}_{\mathcal{J}}]$ and
that limits are unique modulo isomorphism.

######  Corollary 2.22.

Given two factor systems $\mathcal{M}_{\mathcal{I}}$ and
$\mathcal{N}_{\mathcal{J}}$ with limits $\mathcal{M}$ and $\mathcal{N}$ resp.
Assume Condition (D) holds, then $[\mathcal{M}\to_{\mathfrak{D}}\mathcal{N}]$
is a limit of $[\mathcal{M}_{\mathcal{I}}\to\mathcal{N}_{\mathcal{J}}]$.
Equivalently stated, there is an isomorphism
$[\mathcal{E}\mathcal{L}(\mathcal{M}_{\mathcal{I}})\to_{\mathfrak{D}}\mathcal{E}\mathcal{L}(\mathcal{N}_{\mathcal{J}})]\simeq\mathcal{E}\mathcal{L}([\mathcal{M}_{\mathcal{I}}\to\mathcal{N}_{\mathcal{J}}])$.

##  3 Towards Models and Interpretations

This section contains the first steps towards an interpretation of a typed
$\lambda$-term in a factor system and a limit of it. Let types
$\varrho\in{Typ}$ be given by $\varrho::=\iota\,\,|\,\,\varrho\to\varrho$ for
base types $\iota$. We assume that type is one of these base types. For each
type $\varrho$ let a non-empty, directed set $\mathcal{I}_{\varrho}$ of
indices be given and let
$\mathfrak{D}_{\Gamma}:=\mathfrak{D}(\mathcal{I}_{\Gamma})$ be a filter which
satisfies (Filter). Maps on indices, such as $Emb_{i}$, extend in an obvious
way to state contexts $C=(i_{0},\dots,i_{n-1})$ as products, e.g.
$Emb_{C}=Emb_{i_{0}}\times\dots\times Emb_{i_{n-1}}$.

Given also a basic version of a simply typed $\lambda$-calculus (without
constants) and for convenience we use a fixed list of variables
$\mathsf{x_{0}},\mathsf{x_{1}},\mathsf{x_{2}},\dots$ within the Church-style
$\lambda$-terms
$\mathsf{r}::=\mathsf{x_{k}}\,\,|\,\,\mathsf{r}\mathsf{r}\,\,|\,\,\lambda\mathsf{x}_{\mathsf{k}}^{\varrho}\mathsf{r}$.
We apply the usual conventions for $\lambda$-terms [11].

###  3.1 Judgements for Types and States

Typing judgements $\Gamma\vdash\mathsf{r}:\varrho$ with
$\Gamma=(\varrho_{0},\dots,\varrho_{n-1})$ are defined recursively as follows:

We can write more explicitly
$(\mathsf{x_{0}}:\varrho_{0},\dots,\mathsf{x_{n-1}}:\varrho_{n-1},\mathsf{x_{n}}:\varrho_{n})$
for the context $\Gamma.\varrho_{n}$, so $\lambda$-abstractions binds the last
variable of the context.333This style is basically the de Bruijn level
notation of $\lambda$-terms, see e.g. [6]. When we speak of typed terms this
refers to this typing judgement. It is well known that each term $\mathsf{r}$
in the simply typed $\lambda$-calculus has a unique type for a given context
$\Gamma$.

######  Definition 3.1.

Let $\iota$ denote a base type. The _positive_ and _negative_ types are
defined as

${Typ}^{+}\ni\varrho^{+}::=\iota\,\,|\,\,\varrho^{-}\to\varrho^{+}\quad\text{
and }\quad{Typ}^{-}\ni\varrho^{-}::=$

For an index $i\in\mathcal{I}_{\varrho}$ with $\varrho\in{Typ}^{+}$ we write
$i\in Idx^{+}$, and similar for $i\in Idx^{-}$. Moreover,
${Typ}^{c}\ni\varrho^{c}::=\iota\,\,|\,\,\varrho^{+}\to\varrho^{c}\,\,|\,\,\varrho^{-}\to\varrho^{c}$.

For example, $nat$ is a positive type, $nat\to nat\to$ is a negative type, is
both and $nat\to nat$ is neither. Obviously
${Typ}^{+}\cup{Typ}^{-}\subseteq{Typ}^{c}$ and
$\varrho\in{Typ}^{+}\cap{Typ}^{-}\iff\varrho::=$. In order to formulate the
rules for states, we use a fragment of the simply typed $\lambda$-calculus,
which we refer to as the _core fragment_. This fragment is constrained in such
a way that contexts $\Gamma=(\varrho_{0},\dots,\varrho_{n-1})$ contain only
positive or negative types, that is,

$\varrho_{k}\in{Typ}^{+}\cup{Typ}^{-}\text{ for all }\varrho_{k}\text{ in
}\Gamma.$ (9)

A more general definition would permit the use of further base types in place
of the negative type . This requires that the base type in question has a
finite set of objects and an interpretation analogous to that of type in
Definition 3.3. The primary motivation for this definition is the existence of
suitable rules for state judgements of variables and the fact that positive
types can be interpreted as direct factor systems and negative types as
inverse factor systems.

######  Lemma 3.2.

The typed term $\Gamma\vdash\mathsf{r}:\varrho$ is in the core fragment iff
$\Gamma\to\varrho\in{Typ}^{c}$.

This lemma follows easily by induction on $\Gamma\vdash\mathsf{r}:\varrho$.
Therein $\Gamma\to\sigma$ is defined by $()\to\sigma:=\sigma$ and
$\Gamma.\varrho\to\sigma:=\Gamma\to(\varrho\to\sigma)$; the index $C\to i$ is
defined in the same way as $\Gamma\to\sigma$. We now introduce judgements for
states of the form $C\mid\mathsf{r}:i$. They require a typing judgement
$\Gamma\vdash\mathsf{r}:\varrho$ such that $C\to
i\in\mathcal{I}_{\Gamma\to\varrho}$. The rules are based on the typing
rules444One may also combine both rules into one. The rules are however more
readable if one keeps them separated., whereby $C=(i_{0},\dots,i_{n-1})$.

The condition $j\geq i_{k}$ in Rule (Var$+$) is a consequence of the fact that
objects $a_{i_{k}}$ of positive type exist at all later stages $j$ as
$emb_{i_{k}}^{j}(a_{i_{k}})$. The condition $j\leq i_{k}$ in Rule (Var$-$) is
related to the fact that we find unique restrictions of a relation, but not
unique extensions. Note that for an index $i_{k}\in Idx^{+}\cap Idx^{-}$ both
of the rules for variables apply. In this case, however, there is only one
index, so both rules are the same.

A term usually has several state judgement, not only one. Indeed, we expect
that there are $\mathfrak{D}$-many of them and it seems necessary to prove
this stronger property in order to guarantee that at least one judgement
exists. However, we have not shown that all terms of the core fragment have a
state judgement. It is possible to define sets $\mathfrak{D}_{\Gamma}$,
similar as in [4], but with a reorder of the context $\Gamma$ that takes the
positive types first, and afterward the negative ones. In a subsequent paper
we will present such a definition of sets $\mathfrak{D}_{\Gamma}$ satisfying
Condition (D) and a proof that each term in the above mentioned fragment has
indeed $\mathfrak{D}$-many state judgements.

###  3.2 Interpretation of Types

An interpretation of a type $\varrho$ has a static and a dynamic part.
Although the limit is uniquely defined from a structural perspective, the
extension, i.e., the set of elements in the limit, depends on the stage of the
meta-level investigation, assuming a consequent finitistic view. In this case,
the limit is not the absolute end of the extensible system. As the
investigation progresses, both the system and the limit increase. The main
part of the interpretation is the factor system — the limit is necessary to
prove that the definition in the factor system is correct.

Let $([\\![\varrho]\\!]_{i})_{i\in\mathcal{I}_{\varrho}}$ be the factor system
that interprets type $\varrho$, which consists of finite sets
$[\\![\varrho]\\!]_{i}$. The limit, up to isomorphism, is then
$[\\![\varrho]\\!]:=\mathcal{E}\mathcal{L}(([\\![\varrho]\\!]_{i})_{i\in\mathcal{I}_{\varrho}})$,
see Section 2.4. These limit sets give rise to an extensional type structure
if we use (Appl) as application. Recall Lemma 2.18 and our assumption of
Condition (D).

######  Definition 3.3.

An interpretation $[\\![\ ]\\!]$ of types assigns to a type $\varrho$ a factor
system $([\\![\varrho]\\!]_{i})_{i\in\mathcal{I}_{\varrho}}$ and a limit
$[\\![\varrho]\\!]$ of it. So the pair
$(([\\![\varrho]\\!]_{i})_{i\in\mathcal{I}_{\varrho}},[\\![\varrho]\\!])$
interprets the type $\varrho$. This interpretation shall satisfy the following
properties:

  1. 1.

For a base type $\iota$, $([\\![\iota]\\!]_{i})_{i\in\mathcal{I}_{\iota}}$ is
a direct factor system.

  2. 2.

Type  is interpreted by the factor system $\mathbb{B}_{\\{\prop\\}}$ with
$\mathbb{B}=\mathbb{B}=\\{true,false\\}$ and limit $\mathbb{B}$.

  3. 3.

The interpretation of $\varrho\to\sigma$ is the factor system
$[([\\![\varrho]\\!]_{i})_{i\in\mathcal{I}_{\varrho}}\to([\\![\sigma]\\!]_{j})_{j\in\mathcal{I}_{\sigma}}]$
together with the limit
$[[\\![\varrho]\\!]\to_{\mathfrak{D}}[\\![\sigma]\\!]]$.

Since Condition (D) holds, it follows from Corollary 2.22 that the function
space $[[\\![\varrho]\\!]\to_{\mathfrak{D}}[\\![\sigma]\\!]]$ is indeed the
limit of the underlying factor system
$[([\\![\varrho]\\!]_{i})_{i\in\mathcal{I}_{\varrho}}\to([\\![\sigma]\\!]_{j})_{j\in\mathcal{I}_{\sigma}}]$.
Definition 3.3 extends to contexts $\Gamma$ in the usual way by taking
products.

######  Example 3.4.

The standard interpretation of the natural numbers $[\\![nat]\\!]=\mathbb{N}$
is the limit of the direct factor system
$([\\![nat]\\!]_{i})_{i\in\mathbb{N}^{+}}$ with
$[\\![nat]\\!]_{i}=\mathbb{N}_{i}$.555Here we assume that the interpretation
of type $nat$ is the set $\mathbb{N}$ of all natural numbers, which is an
actual infinite set if one accepts actual infinities at meta-level. If not,
$\mathbb{N}$ is an arbitrary large finite set, which corresponds to a set in
the implicitly given factor system at meta-level, i.e., $\mathbb{N}$ is
$\mathbb{N}_{j}$ for some sufficiently large index $j$ depending on the stages
of the meta-level investigation. Of course, there are other non-standard
models of $nat$ with non-standard natural numbers as well. These non-standard
numbers do not appear at the limit step, but at some stage within the system.

The next lemma is required for the reflection principle stated in Theorem 3.9.
Its proof proceeds by induction on Definition 3.1 and uses Proposition 2.8 and
Corollary 2.17.

######  Lemma 3.5.

Given an interpretation of types $[\\![\ ]\\!]$ and let $i\leq i^{\prime}$
with $i,i^{\prime}\in\mathcal{I}_{\varrho}$ for a type $\varrho$.

  1. 1.

If $\varrho\in{Typ}^{+}$, then the factor system
$([\\![\varrho]\\!]_{i})_{i\in\mathcal{I}_{\varrho}}$ is direct and
$a\stackrel{{\scriptstyle p}}{{\longmapsto}}a_{i}$ implies
$a\stackrel{{\scriptstyle p}}{{\longmapsto}}emb_{i}^{i^{\prime}}(a_{i})$.

  2. 2.

If $\varrho\in{Typ}^{-}$, then the factor system is inverse and
$a\stackrel{{\scriptstyle p}}{{\longmapsto}}a_{i^{\prime}}$ implies
$a\stackrel{{\scriptstyle
p}}{{\longmapsto}}proj_{i}^{i^{\prime}}(a_{i^{\prime}})$.

###  3.3 Interpretation of Terms and a First Version of the Reflection
Principle

The interpretation of terms in the type structure of the limit sets is the
common interpretation. What is new is the interpretation in the factor system.
This part of the interpretation requires a state judgement, so it is defined
only for the core fragment, defined in Section 3.1.

######  Definition 3.6.

A $\Gamma$-environment is a list of elements
$\boldsymbol{A}\in[\\![\Gamma]\\!]:=[\\![\varrho_{0}]\\!]\times\dots\times[\\![\varrho_{n-1}]\\!]$
for $\Gamma=(\varrho_{0},\dots,\varrho_{n-1})$. The value
$[\\![\mathsf{r}]\\!]_{\boldsymbol{A}}\in[\\![\varrho]\\!]$ of a typed term
$\Gamma\vdash\mathsf{r}:\varrho$ is defined recursively on the derivation of
the judgement $\Gamma\vdash\mathsf{r}:\varrho$ relative to a
$\Gamma$-environment $\boldsymbol{A}\in[\\![\Gamma]\\!]$:

$\displaystyle[\\![\mathsf{x_{k}}]\\!]_{\boldsymbol{A}}$
$\displaystyle:=A_{k}$ $\displaystyle\text{for
}\Gamma\vdash\mathsf{x_{k}}:\varrho_{k},$
$\displaystyle[\\![\mathsf{rs}]\\!]_{\boldsymbol{A}}$
$\displaystyle:=[\\![\mathsf{r}]\\!]_{\boldsymbol{A}}([\\![\mathsf{s}]\\!]_{\boldsymbol{A}})$
$\displaystyle\text{for }\Gamma\vdash\mathsf{r}:\varrho\to\sigma\text{ and
}\Gamma\vdash\mathsf{s}:\varrho,$
$\displaystyle[\\![\lambda\mathsf{x}_{\mathsf{n}}^{\varrho}\mathsf{r}]\\!]_{\boldsymbol{A}}(B)$
$\displaystyle:=[\\![\mathsf{r}]\\!]_{\boldsymbol{A}.B}$
$\displaystyle\text{for }\Gamma.\varrho\vdash\mathsf{r}:\sigma\text{ and
}B\in[\\![\varrho]\\!].$

######  Definition 3.7.

A $C$-environment is a list of elements
$\boldsymbol{a}\in[\\![\Gamma]\\!]_{C}:=[\\![\varrho_{0}]\\!]_{i_{0}}\times\dots\times[\\![\varrho_{n-1}]\\!]_{i_{n-1}}$
for $C=(i_{0},\dots,i_{n-1})$. The value
$[\\![\mathsf{r}]\\!]_{\boldsymbol{a}:C}^{i}\in[\\![\varrho]\\!]_{i}$ of a
term with $C\mid\mathsf{r}:i$ relative to a $C$-environment
$\boldsymbol{a}\in[\\![\Gamma]\\!]_{C}$ is defined recursively on the
derivation of the state judgement $C\mid\mathsf{r}:i$:

$\displaystyle[\\![\mathsf{x_{k}}]\\!]_{\boldsymbol{a}:C}^{j}$
$\displaystyle:=emb_{i_{k}}^{j}(a_{k})$ $\displaystyle\text{for
}C\mid\mathsf{x_{k}}:i_{k}\text{ and }\varrho_{k}\in{Typ}^{+},$
$\displaystyle[\\![\mathsf{x_{k}}]\\!]_{\boldsymbol{a}:C}^{j}$
$\displaystyle:=proj_{j}^{i_{k}}(a_{k})$ $\displaystyle\text{for
}C\mid\mathsf{x_{k}}:i_{k}\text{ and }\varrho_{k}\in{Typ}^{-},$
$\displaystyle[\\![\mathsf{rs}]\\!]_{\boldsymbol{a}:C}^{j}$
$\displaystyle:=[\\![\mathsf{r}]\\!]_{\boldsymbol{a}:C}^{i\to
j}([\\![\mathsf{s}]\\!]_{\boldsymbol{a}:C}^{i})$ $\displaystyle\text{for
}C\mid\mathsf{r}:i\to j\text{ and }C\mid\mathsf{s}:i,$
$\displaystyle[\\![\lambda\mathsf{x}_{\mathsf{n}}^{\varrho}\mathsf{r}]\\!]_{\boldsymbol{a}:C}^{i\to
j}(b)$ $\displaystyle:=[\\![\mathsf{r}]\\!]_{\boldsymbol{a}.b:C.i}^{j}$
$\displaystyle\text{for }C.i\mid\mathsf{r}:j\text{ and
}b\in[\\![\varrho]\\!]_{i}.$

By definition, the value $[\\![\mathsf{r}]\\!]_{\boldsymbol{a}:C}^{i}$ depends
on the way the judgement $C\mid\mathsf{r}:i$ has been derived. So different
derivations could lead to different values, making this definition incorrect.
The value $[\\![\mathsf{rs}]\\!]_{\boldsymbol{a}:C}^{j}$ seemingly depend on
the chosen index $i$ used in $[\\![\mathsf{s}]\\!]_{\boldsymbol{a}:C}^{i}$. A
consequence of the main Theorem 3.9 is that the value
$[\\![\mathsf{r}]\\!]_{\boldsymbol{a}:C}^{i}$ is indeed independent (modulo
$\asymp$) of the derivation of the state judgement $C\mid\mathsf{r}:i$.

######  Definition 3.8.

Given a pair $(\boldsymbol{A},\boldsymbol{a})$ with a $\Gamma$-environment
$\boldsymbol{A}$ and a $C$-environment $\boldsymbol{a}$ such that
$\boldsymbol{A}\stackrel{{\scriptstyle p}}{{\longmapsto}}\boldsymbol{a}$. The
interpretation of a typed term $\Gamma\vdash\mathsf{r}:\varrho$ with state
judgement $C\mid\mathsf{r}:i$ relative to $(\boldsymbol{A},\boldsymbol{a})$ is
the pair
$([\\![\mathsf{r}]\\!]_{\boldsymbol{A}},[\\![\mathsf{r}]\\!]_{\boldsymbol{a}:C}^{i})\in[\\![\varrho]\\!]\times[\\![\varrho]\\!]_{i}$.

One would expect that $\boldsymbol{A}\stackrel{{\scriptstyle
p}}{{\longmapsto}}\boldsymbol{a}$ implies
$[\\![\mathsf{r}]\\!]_{\boldsymbol{A}}\stackrel{{\scriptstyle
p}}{{\longmapsto}}[\\![\mathsf{r}]\\!]_{\boldsymbol{a}:C}^{i}$. Indeed, this
is the content of the next theorem, which is also the main theorem.

######  Theorem 3.9.

Given a typed term $\Gamma\vdash\mathsf{r}:\varrho$ with $C\mid\mathsf{r}:i$.
If $\boldsymbol{A}\in[\\![\Gamma]\\!]$,
$\boldsymbol{a}\in[\\![\Gamma]\\!]_{C}$ are variable assignments with
$\boldsymbol{A}\stackrel{{\scriptstyle p}}{{\longmapsto}}\boldsymbol{a}$, then

$[\\![\mathsf{r}]\\!]_{\boldsymbol{A}}\stackrel{{\scriptstyle
p}}{{\longmapsto}}[\\![\mathsf{r}]\\!]_{\boldsymbol{a}:C}^{i}.$

######  Proof 3.10.

The proof proceeds by induction on the derivation of $C\vdash\mathsf{r}:i$.
For a variable $\mathsf{x_{k}}$ of a positive type we apply Lemma 3.5. This
yields

$[\\![\mathsf{x_{k}}]\\!]_{\boldsymbol{A}}=A_{k}\stackrel{{\scriptstyle
p}}{{\longmapsto}}emb_{i_{k}}^{j}(a_{k})=[\\![\mathsf{x_{k}}]\\!]_{\boldsymbol{a}:C}^{j},$

since $A_{k}\stackrel{{\scriptstyle p}}{{\longmapsto}}a_{k}$. A similar
consideration holds for negative types. For application and abstraction the
claim follows from the fact that $\stackrel{{\scriptstyle p}}{{\longmapsto}}$
is a logical relation.

Consider the case of a closed term $\mathsf{r}:\varrho$. Let us assume that
$\varrho$ is some data type, then the theorem states that
$[\\![\mathsf{r}]\\!]\stackrel{{\scriptstyle
p}}{{\longmapsto}}[\\![\mathsf{r}]\\!]^{i}$. Recall that the predecessor
relation $\stackrel{{\scriptstyle p}}{{\mapsto}}$ is seen as a directed
equality between two states of the same object. We can thus read
$\stackrel{{\scriptstyle p}}{{\longmapsto}}$, which is nothing more than
$\stackrel{{\scriptstyle p}}{{\mapsto}}$ applied limits, as an equality
between $[\\![\mathsf{r}]\\!]$ and $[\\![\mathsf{r}]\\!]^{i}$. As indicated in
Section 1.1, $[\\![\mathsf{r}]\\!]^{i}$ is a strong form of an approximation
of $[\\![\mathsf{r}]\\!]$.

Due to the use of logical relations on higher types, application and
$\lambda$-abstraction respect this equality. Since the type of propositions is
part of the calculus, the equality holds also for truth values. The relation
$[\\![\mathsf{r}]\\!]\stackrel{{\scriptstyle
p}}{{\longmapsto}}[\\![\mathsf{r}]\\!]^{i}$ for type , with the only values
$true$ and $false$ in classical logic, is the identity. Consequently, truth in
the limit and truth in a sufficiently large stage of the factor system
coincide. Theorem 3.9 is the main result, and at the same time this theorem is
necessary to show that the basic definition of the interpretation of a term,
as introduced in Definition 3.7, is correct.

######  Corollary 3.11.

Let $\Gamma\vdash\mathsf{r}:\varrho$ be a typed term with $i\leq i^{\prime}$,
$C\mid\mathsf{r}:i$ and $C\mid\mathsf{r}:i^{\prime}$. Then
$[\\![\mathsf{r}]\\!]_{\boldsymbol{a}:C}^{i^{\prime}}\stackrel{{\scriptstyle
p}}{{\mapsto}}[\\![\mathsf{r}]\\!]_{\boldsymbol{a}:C}^{i}$ holds for all
$C$-environments $\boldsymbol{a}\in[\\![\Gamma]\\!]_{C}$.

######  Proof 3.12.

Define $\boldsymbol{A}:=Emb_{C}(\boldsymbol{a})$. Then
$\boldsymbol{A}\stackrel{{\scriptstyle p}}{{\longmapsto}}\boldsymbol{a}$
follows from Condition (Emb), hence
$[\\![\mathsf{r}]\\!]_{\boldsymbol{A}}\stackrel{{\scriptstyle
p}}{{\longmapsto}}[\\![\mathsf{r}]\\!]_{\boldsymbol{a}:C}^{i^{\prime}}$ and
$[\\![\mathsf{r}]\\!]_{\boldsymbol{A}}\stackrel{{\scriptstyle
p}}{{\longmapsto}}[\\![\mathsf{r}]\\!]_{\boldsymbol{a}:C}^{i}$ by Theorem 3.9,
and therefore
$[\\![\mathsf{r}]\\!]_{\boldsymbol{a}:C}^{i^{\prime}}\stackrel{{\scriptstyle
p}}{{\mapsto}}[\\![\mathsf{r}]\\!]_{\boldsymbol{a}:C}^{i}$ by Condition
(Factor).

The independence of the value $[\\![\mathsf{r}]\\!]_{\boldsymbol{a}:C}^{i}$
(modulo $\asymp$) from the state judgement follows from Corollary 3.11 if we
take $i=i^{\prime}$.

##  4 Conclusion and Further Work

We presented a model that can be used to interpret a fragment of the simply
typed $\lambda$-calculus (which we called _core fragment_) based on the
assumption that infinite sets are potential infinite. We gave a formalization
of the potential infinite based on the filters $\mathfrak{D}$ and sets $\ll$
within these filters. This allows one to avoid any notion of actual infinity.
The function space in this model is a family of finite function spaces and the
model already has an interpretation of the logical type with the usual two
truth values.

We introduced an interpretation of $\lambda$-terms from the core fragment
which has a dynamic part, the factor system, and a static part, the limit of
the factor system. Nevertheless, both parts are necessary, because from a
dynamic point of view, the construction of a limit is not the end of the
process, but an intermediate state.

The next step is to extend the $\lambda$-calculus to constants, in particular
to the logical constants of implication and universal quantifier. The
challenge here is that the universal quantifier is not continuous and cannot
be interpreted as a higher-order functional. The solution is to introduce an
additional rule with a side condition $C\ll i$ on the state judgments. The
correctness of the interpretation uses the fact that propositions have “stable
truth values” in the sense that for each proposition there is a stage in the
model where the truth value of the proposition does not change anymore during
further extensions. A corresponding interpretation for first-order logic has
been given in [4].

The reflection principle from Theorem 3.9 then states that all objects and
propositions (propositions are specific terms of type ) in the limit are
reflected in a sufficiently large state in the system. The interpretation is
possible on the core fragment of simple type theory, not for all terms.
However, this fragment includes a version of a classical higher-order logic.
Unlike other models, such as domain theory [1], it does not require (actual)
infinite sets at all, and it includes logic.666The idea of a logic-enriched
type theory [7] separates propositions from the underlying type theoretic
framework. In our approach the logic is inside type theory, but the
interpretation of the universal quantifier has an extra treatment.

We do not expect that the theorem about the reflection principle can be
extended from the core fragment to all terms of simply typed
$\lambda$-calculus without some kind of further restrictions. This is because
variables of function type correspond to arbitrary functions, which can also
be used to define higher-order functions by $\lambda$-abstraction. From the
perspective of extensibility, this necessitates the consideration of both
covariant (with respect to the codomain) and contravariant (with respect to
the domain) extensions simultaneously. For instance, the totality of higher-
order functions requires that, for each argument, which could be a function
$f$ of type $nat\to nat$, there must be a value. However, $f$ is not given as
a single entity. So one must identify a property that guarantees totality and
conditions that ensure invariance, that is, existing properties must be
preserved by future extensions of $f$. This is a significant challenge for
higher-order functions and it is related to properties of the filter
$\mathfrak{D}$. It is also the reason that for arbitrary functions, there are
no simple state judgements as formulated in the rules (Var$+$) and (Var$-$). A
future task will be to identify conditions under which the core fragment can
be extended to include function variables.

## References

  * [1] Samson Abramsky and Achim Jung.  Domain theory.  In Handbook of logic in computer science. Oxford University Press, 1994.
  * [2] Hendrik Pieter Barendregt.  The lambda calculus - its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics.  North-Holland, Amsterdam, 1985.
  * [3] Alonzo Church.  A formulation of the simple theory of types.  The Journal of Symbolic Logic, 5(2):56–68, 1940.  doi:10.2307/2266170.
  * [4] Matthias Eberl.  A model theory for the potential infinite.  Reports on Mathematical Logic, 57:3–30, 2022.  doi:10.4467/20842589rm.22.001.16658.
  * [5] Matthias Eberl.  Higher-order concepts for the potential infinite.  Theoretical Computer Science, 945:113667, 2023.  doi:10.1016/j.tcs.2022.12.017.
  * [6] Marcelo P. Fiore, Gordon D. Plotkin, and Daniele Turi.  Abstract syntax and variable binding.  In Proc. 14th LICS Conf., pages 193–202. IEEE, Computer Society Press, 1999.  doi:10.1109/LICS.1999.782615.
  * [7] Nicola Gambino and Peter Aczel.  The generalised type-theoretic interpretation of constructive set theory.  The Journal of Symbolic Logic, 71(1):67–103, 2006.  doi:10.2178/jsl/1140641163.
  * [8] John Longley and Dag Normann.  Higher-order computability, volume 100.  Springer, 2015.  doi:10.1007/978-3-662-47992-6.
  * [9] Saunders MacLane and Ieke Moerdijk.  Sheaves in geometry and logic: A first introduction to topos theory.  Springer Science & Business Media, 2012.  doi:10.1007/978-1-4612-0927-0.
  * [10] John C. Mitchell and Eugenio Moggi.  Kripke-style models for typed lambda calculus.  Annals of Pure and Applied Logic, 51(1-2):99–124, 1991.  doi:10.1016/0168-0072(91)90067-V.
  * [11] Rob Nederpelt and Herman Geuvers.  Type theory and formal proof: an introduction.  Cambridge University Press, 2014.
  * [12] Gordon Plotkin.  Lambda-definability and logical relations.  Edinburgh University, 1973.
  * [13] Anne S. Troelstra.  Choice sequences. A chapter of intuitionistic mathematics. Oxford logic guides, volume 44.  Clarendon Press, 1979.
  * [14] Anne S. Troelstra and Dirk van Dalen.  Constructivism in mathematics. vol. i, volume 121 of.  Studies in Logic and the Foundations of Mathematics, 26, 1988.