I cannot imagine that I shall ever return to the creed of the true Platonist, who sees the world of the actual infinite spread out before him and believes that he can comprehend the incomprehensible.

Abraham Robinson,

From A Formalist's Point of View

Systems

A dynamic object $a$ is mathematically a function from an index set $\mathcal{I}$ to possible states $a_i$ of $a$ , that is, $a$ is the family $(a_i)_{i \in \mathcal{I}}$ . Similarly, a dynamic set $\mathcal{M}$ is a family of sets varying over $\mathcal{I}$ , i.e., $\mathcal{M}$ is $(\mathcal{M}_i)_{i \in \mathcal{I}}$ . The finitistic approach requires that $\mathcal{M}_i$ is finite, but the technical treatment makes no use of this property ― we could work with other small versus large distinctions as well. But from our perspective we gain nothing by doing so. More relevant is the fact that we do not need any notion of finiteness of the sets $\mathcal{M}_i$ . The set $\mathcal{I}$ is equipped with a preorder $\leq$ indicating that if $i' \geq i$ , then $i'$ refers to a "later" state. We also require that $\mathcal{I}$ is directed with the idea that the different states converge towards "one limit" (without reaching it if the set is infinite).

The objects in the different states $\mathcal{M}_{i'}$ and $\mathcal{M}_i$ for $i' \geq i$ are connected by a relation $a_i \mapsto \! \! \! \! \! \! \! \! \ {s \above 0pt \ } \ \, a_{i'}$ if $a_i \in \mathcal{M}_i$ and $a_{i'} \in \mathcal{M}_{i'}$ . The intention is that $a_{i'}$ is a successor of $a_i$ . The simplest case for first-order logic is that $\mapsto \! \! \! \! \! \! \! \! \ {s \above 0pt \ } \$ is an embedding of $\mathcal{M}_i$ into $\mathcal{M}_{i'}$ . In that situation we can identify an element with its embedding, so $\mathcal{M}_i \subseteq \mathcal{M}_{i'}$ for $i \leq i'$ . For instance, we have $\mathbb{N}_i \subseteq \mathbb{N}_{i'}$ with $\mathbb{N}_i := \{0, 1, \dots, i-1\}$ and $\mathbb{N}_i \ni n \mapsto \! \! \! \! \! \! \! \! \ {s \above 0pt \ } \ \, n \in \mathbb{N}_{i'}$ for $n < i \leq i'$ , which is a special case of a direct system. In the sequel we simply speak of a system if we refer to $((\mathcal{M}_i)_{i \in \mathcal{I}}, \mapsto \! \! \! \! \! \! \! \! \ {s \above 0pt \ } \ )$ . We consider extensible models, so we require that for all $a_i \in \mathcal{M}_i$ and all $i' \geq i$ there is some $a_{i'} \in \mathcal{M}_{i'}$ with $a_i \mapsto \! \! \! \! \! \! \! \! \ {s \above 0pt \ } \ \, a_{i'}$ (i.e., $\mapsto \! \! \! \! \! \! \! \! \ {s \above 0pt \ } \$ is left-total). Of course, the relation $\mapsto \! \! \! \! \! \! \! \! \ {s \above 0pt \ } \$ has to satisfy further properties, but it would be too lengthy to state them in this overview.

First-Order Theory

In a first-order logic the only subject that could be infinite is the domain of discourse and the functions and relations on it, not the objects themselves. We call an object infinite, if it needs infinitely many properties in order to define it.

Classical Logic

Take as starting point for classical first-order logic the usual Tarskian model theory, i.e., model theory of classical first-order logic. The variable assignment $\vec{a} = (a_0, \dots, a_{n-1})$ , instantiating the free variables $\mathsf{x_0}, \dots, \mathsf{x_{n-1}}$ in a formula $\mathsf{\Phi}$ , are taken from $\mathcal{M}_C := \mathcal{M}_{i_0} \times \dots \times \mathcal{M}_{i_{n-1}}$ ― we assume that each formula $\mathsf{\Phi}$ is given together with a list of variables $\mathsf{x_0}, \dots, \mathsf{x_{n-1}}$ . Relation $R$ , the interpretation of an n-ary relation symbol $\mathsf{R}$ in the signature, is a family $(R_C)_{C \in \mathcal{I}^n}$ with $R_C \subseteq \mathcal{M}_C$ . It satisfies $R_C \subseteq R_{C'}$ for $C \leq C'$ with a pointwise order, so relations are increasing, too. It is also possible to add function symbols and functions.

The main concept in model theory is the notion of a validity (also called satisfaction) of a formula $\mathsf{\Phi}$ in a model $\mathcal{M}$ under a variable assignment $\vec{a}$ , written as $\mathcal{M} \models \mathsf{\Phi}[\vec{a}]$ . In our approach, the notion of validity becomes $(\mathcal{M}_i)_{i \in \mathcal{I}} \models_{\ll} \mathsf{\Phi}[\vec{a} : C]$ with $\ll$ as an additional parameter. The interpretation of the logical connectives is as usual. The universal quantifier is interpreted by

(\mathcal{M}_i)_{i \in \mathcal{I}} \models_{\ll} \forall \mathsf{x_n} \mathsf{\Phi} [\vec{a} : C]

\ :\!\iff

(\mathcal{M}_i)_{i \in \mathcal{I}} \models_{\ll} \mathsf{\Phi} [\vec{a}b : Ci]

for all

b \in \mathcal{M}_i

with an indefinitely large set $\mathcal{M}_i$ , i.e., $i \gg C$ . Therein, $\vec{a} b$ is the extension of the variable assignment $\vec{a}$ by $b$ , and $Ci$ the extension of the context $C$ by index $i$ . The existential quantifier $\exists \mathsf{x}$ can be reduced to $\neg \forall \mathsf{x} \neg$ .

Figure 3: Relations between Language and Model.

This interpretation uses a semantic reflection principle: An assertion about all infinitely many elements in $(\mathcal{M}_i)_{i \in \mathcal{I}}$ is true if and only if it is true about a part $\mathcal{M}_i$ that reflects the whole infinite set in the current context $C$ . In order to show that this interpretation is sound (relative to a usual inference system for classical first-order logic) and that the validity is independent of the chosen index $i \gg C$ , one has to restrict the set of relations $\ll$ to those, which contain all witnesses of valid existential assertions. We call these relations $\ll$ adequate. The definition of these is similar to the proof of the Löwenheim-Skolem theorem and Mycielski's original work. The interpretation $\models_{\ll}$ is also complete for these relations $\ll$ . Moreover it is locally finite in the sense that a finite set of expressions requires a finite model only.

A characteristic in Tarskian semantics is the interpretation of open formulas. The interpretation is relative to a variable assignment $\vec{a}$ and an open formula is valid if it is valid relative to all variable assignments $\vec{a}$ . Additionally, the interpretation with reflection principle is relative to a notion of being indefinitely large, i.e. $\ll$ , and a formula is valid, if it is valid relative to all adequate relations $\ll$ . Adequacy is a relative notion as well, it depends on a set of formulas. For a (possibly infinite) set of formulas $\mathcal{T}$ we choose some stage $k$ and for the finite set $\mathcal{T}_{\!k}$ there is an adequate relation $\ll$ ; moreover, there is also some stage $j$ in the model which interprets all formulas in $\mathcal{T}_{\!k}$ correctly, expressed by the formulation " $(\mathcal{M}_i)_{i \leq j}$ is sufficiently large for $\mathcal{T}_{\!k}$ ". Locally finiteness follows from this dependency of the (size of the) model from the (number of) syntactical expressions. There could be other, conflicting dependencies, for instance the requirement that there is a constant $\mathsf{c}_a$ in the language for each element $a$ in the model, being an embedding $\mathcal{M}_j \hookrightarrow \mathcal{L}_k$ , see Figure 3. In other words, the claim that for each element in the model there is a constant in the language is not an innocuous requirement.

Intuitionistic Logic

This interpretation with reflection principle is also applicable to intuitionistic logic with Kripke models, or alternatively Beth models. Kripke models are based on a frame $(\mathcal{K},\leq)$ , being a preorder of epistemic states or nodes. Deviating from the index set $\mathcal{I}$ , these frames are typically not directed ― different branches generate alternatives, which may not "meet later".

There is however a more important difference between the index sets $\mathcal{K}$ and $\mathcal{I}$ : The set $\mathcal{K}$ represents epistemic states or states of information, whereas the index set $\mathcal{I}$ is related to the ontological side of the semantics. So we may ask whether an element $a$ exists in $\mathcal{M}_i$ , but if it exists there, it has already all of its properties (nothing new can be added to $a$ in $\mathcal{M}_{i'}$ for $i' \geq i$ ). Technically this is the requirement that $R_C$ is the restriction of $R_{C'}$ for $C \leq C'$ . In comparison, if $a$ exists at $k$ , it has the properties known at $k$ , but we may discover at $k' > k$ additional properties, even if the same objects exist at $k$ and $k'$ . Similar as for classical logic, one can define a forcing relation (denoting validity in this case) with a reflection principle and show soundness and completeness as well as local finiteness.

Higher-Order Theory

A finitistic point of view can deal with infinite objects, such as $\omega$ (the object representing the set of natural numbers in set theory), in two ways:

The object, say $\omega$ , may be regarded as a single abstract object. First-order logic can deal with these kind of objects only.
Or infinite objects are indefinitely extensible objects, analogously as sets are indefinitely extensible. Then there is no single object $\omega$ , only approximations of it, e.g. finite sets $\omega_i$ . Higher-order logic formalizes this concept as well.

Differentiation of Objects

Higher-order logic extends first-order logic in that it handles infinite objects. In set theory, as in any other first-order theory, the universe is in our approach a system $(\mathcal{M}_i)_{i \in \mathcal{I}}$ with finite carrier sets $\mathcal{M}_i$ . The abstract "set-objects" $a \in \mathcal{M}_i$ become concrete in the background model due to the indefinitely increasing membership relation $\epsilon$ , which is a family with states $\epsilon_i \subseteq \mathcal{M}_i \times \mathcal{M}_i$ . An object such as $\omega$ represents an increasing family $\omega_i := \{a \in \mathcal{M}_i \mid a \ \epsilon_i \ \omega\}$ for all $i \in \mathcal{I}$ with $\omega \in \mathcal{M}_i$ . Thereby $\omega_i$ is a "real" set, i.e., a (finite) set in the background model, that increases if we enlarge $i \in \mathcal{I}$ . There is no explicit concept in first-order logic that sees all of these $\omega_i$ as approximations of $\omega$ . The successor relation $\mapsto \! \! \! \! \! \! \! \! \ {s \above 0pt \ } \$ in a first-order model is always a function, that is, an object is not differentiated if the model increases. To put it another way, if a (first-order) object occurs at some stage, it is already "complete" and is not an approximation that needs further differentiation.

Higher-order logic explicitly introduces approximations which are placed in relation by $\mapsto \! \! \! \! \! \! \! \! \ {s \above 0pt \ } \$ . Infinite objects are only handled by their approximations, e.g. $\omega$ is the family of finite von Neumann ordinals $n$ and $n \mapsto \! \! \! \! \! \! \! \! \ {s \above 0pt \ } \ \, n'$ if $n \ \epsilon \ n'$ . Then $\omega$ exists only as this family, not as an abstract limit object ― but in higher-order logic there might be both, abstract objects and families of approximations. The axiom of infinity expresses the existence of an abstract limit object for each increasing system. Additionally, each sufficiently large $n$ plays the role of $\omega$ , whereby its size depends on the current context.

Similarly, a real number, for instance $\sqrt{2}$ , can be given as an indefinitely extensible Cauchy sequence of rational numbers. Then a sufficiently good approximation by a rational number is a substitute for the real number. Additionally the real number may be given as abstract object of some base type, which is an element of a complete ordered field (defined axiomatically). But $\sqrt{2}$ is not the infinite Cauchy sequence, being an element of this field of real numbers.

Simple Type Theory

Figure 4: Extensible Function Space.

An elegant way to formulate classical higher-order logic is within the framework of simple type theory. A prerequisite for a dynamic model is an indefinitely extensible system with a limit construction in the style of a direct and inverse limit. This allows an interpretation of the universal quantifier similar as for first-order logic. In simple type theory all infinite objects are (higher-order) functions.

In order to see how simple type theory handles them by approximations, consider functions on natural numbers. Instead of first building an actual infinite set $\mathbb{N}$ and then defining the function space $[\mathbb{N} \to \mathbb{N}]$ as consisting of "all" functions, $[\mathbb{N} \to \mathbb{N}]$ is approximated by finite function spaces $\mathbb{N}_{i \to j} := [\mathbb{N}_{i} \to \mathbb{N}_{j}]$ , with $i, j \in \mathbb{N}^+ :=\{1,2,\dots\}$ ― we suggestively write $i \to j$ for such a pair of indices. These function spaces form a system $(\mathbb{N}_{i \to j})_{i,j > 0}$ with $f \mapsto \! \! \! \! \! \! \! \! \ {s \above 0pt \ } \ \, f'$ , whereby a function $f : \mathbb{N}_{i} \to \mathbb{N}_{j}$ is related to $f' : \mathbb{N}_{i'} \to \mathbb{N}_{j'}$ for $i \leq i'$ and $j \leq j'$ if $f$ is the restriction of $f'$ to $\mathbb{N}_i$ , see Figure 4. A function is itself an indefinitely extensible family $(f_{i \to j})_{(i,j) \in \mathcal{H}}$ with $f_{i \to j} : \mathbb{N}_i \to \mathbb{N}_j$ and a suitable index set $\mathcal{H} \subseteq \mathbb{N}^+ \times \mathbb{N}^+$ . A suitable index set must have "enough" indices, however, the definition of such an index set is a challenge for functionals of type 2 and higher.

All other constructions to handle infinite objects in a finitistic way use, to our knowledge, completed infinities. A wide spread approach to handle infinite objects very generally is domain theory. A domain $\mathcal{D}$ is directed complete, which is a property that requires actual infinite sets in order to be non-trivial, since each finite directed set has automatically a greatest element. There is another, less well known approach, the hyperfinite type structure. It is based on a Fréchet product (i.e., a product reduced by the Fréchet filter). In a Fréchet product two elements $(a_i)_{i \in \mathbb{N}}$ and $(b_i)_{i \in \mathbb{N}}$ are identified if they differ only w.r.t. finitely many indices $i$ . This is obviously trivial if $\mathbb{N}$ is regarded as potential infinite, since all elements are identified then.

A Dynamic Type Theory

The long-term aim is to present this dynamic model theory within a fully developed framework of type theory, according to the slogan that a logic is always a logic over a type theory. This type theory has a dynamic component which is essential for its model. It consists of stages as well as of types for these stages, which we call approximation types. A stage is simply a closed term of an approximation type, and an approximation type is a type together with a directed relation $\leq$ (which is a constant or a closed term).

The most important difference to ordinary type theory is the fact that types are not interpreted directly. Types are intensional (i.e., they do not have a fixed extension of elements) and their main role is to classify elements. What is interpreted instead as (de)finite sets of elements are types in specific states, i.e., the stages. For instance, the square function $\mathsf{sqr} : nat \to nat$ , interpreted at stage $(\mathsf{3},\mathsf{8}) : nat^+ \times nat^+$ (whereby type $nat^+$ corresponds to $\mathbb{N}^+$ ), is in a state given by the finite set of assignments $\{0 \mapsto 0, 1 \mapsto 1, 2 \mapsto 4\}$ .

For a dynamic type theory the basic distinction is between terms $\mathsf{r},\mathsf{s},\dots$ and types $\varrho, \sigma, \dots$ , whereby types are build up as usual by type constructors such as $\to$ (building the function space). To each type $\varrho$ there is an approximation type $\varrho^*$ assigned to it. A closed term of type $\varrho^*$ is an approximation stage for objects of type $\varrho$ , so the type declaration $\mathsf{i} : \varrho^*$ corresponds to the requirement $i \in \mathcal{I}_{\varrho}$ , with $\mathcal{I}_\varrho$ the set of indices of type $\varrho$ . For instance, the approximation type for $nat \to nat$ is type $nat^+ \times nat^+$ with product order, i.e., $(nat \to nat)^* = nat^+ \times nat^+$ . The term $(\mathsf{3},\mathsf{8}) : nat^+ \times nat^+$ defines a stage of the potential infinite set $[\mathbb{N} \to \mathbb{N}]$ of functions on natural numbers, in this case the finite function space $[\mathbb{N}_3 \to \mathbb{N}_8]$ , which is the state of set $[\mathbb{N} \to \mathbb{N}]$ at stage $(\mathsf{3},\mathsf{8})$ .

Similar as a type declaration $\Gamma \vdash \mathsf{r} : \varrho$ , that is, term $\mathsf{r}$ has type $\varrho$ in type context $\Gamma = (\varrho_0, \dots, \varrho_{n-1})$ one has additionally a state declaration $C \vdash \mathsf{r} : \mathsf{i}$ , meaning, term $\mathsf{r}$ has an approximation at stage $\mathsf{i}$ for the state context $C = (\mathsf{i_0}, \dots, \mathsf{i_{n-1}})$ . The context $C$ corresponds to input bounds and $\mathsf{i}$ to an output bound. The declaration $C \vdash \mathsf{r} : \mathsf{i}$ thus guarantees that the interpretation of term $\mathsf{r}$ satisfies the principle of finite support. One may also see the state declaration as a refinement of a type declaration and combine both declarations into one.

One of the advantages is that the hierarchy of universes, which are hard to handle in the usual type theories, is naturally formalized in a dynamic type theory, since all types have these stages (except perhaps types with finitely many elements). Another advantage is that the principle of finite support and continuity principles hold "by design" and there is no need to require them explicitely in the language. On the other hand, the challenging question for a dynamic type theory is the application of a higher order functional, given by a term of higher type, for instance $(nat \to nat) \to nat$ , to an argument. Since there is no completed function of type $nat \to nat$ , application is only defined at the stages $i \to j$ . The challenge is to find "enough" stages in order to define a total application globally. It seems, however, that it is not possible to define such a total function application in general. So it requires a justification, which depends on the circumstances and the context in which the functional is applied to the function. This could also be seen as a positive effect instead of a restriction, following from a consistent view on such principles as that of finite support or continuity. Note that it is always possible to replace higher-order objects by abstract first-order objects, as stated in the beginning of Section Higher-Order Theory.

Meta-Mathematics

We shortly look at meta-mathematical properties, in particular to non-standard models. Some meta-mathematical properties change and some become trivial with this new interpretation.

The Language

Let $\mathcal{L}$ denote the set of our expressions, such as terms and formulas. If $\mathcal{L}$ is infinite, it is consequently seen as indefinitely extensible. This is the case for the usual first- and higher-order languages. In all of these languages $\mathcal{L}$ one can exhaust its expressions by some measure of complexity, whereby the set $\mathbb{N}$ as index set suffices. So $\mathcal{L} = (\mathcal{L}_k)_{k \in \mathbb{N}}$ with finite sets $\mathcal{L}_k$ and $\mathcal{L}_k \subseteq \mathcal{L}_{k'}$ for $k \leq k'$ . The understanding of the language as increasing is important for meta-mathematical properties. With this understanding some notions collapse, for instance consistent is the same as finitely consistent ( $\mathcal{T}$ is finitely consistent if any finite subset of $\mathcal{T}$ has a model). As a consequence, all models are saturated. Interestingly, the compactness theorem for first-order logic does not become trivial, but uniformity: If we find a model at each stage of an increasing set of formulas (i.e. a set $\mathcal{T}$ with states $\mathcal{T}_k \subseteq \mathcal{L}_{k}$ ), then there is a common model for all stages. This follows from the construction of the Henkin-model in a first-order completeness proof.

Non-Standard Models

Figure 5: Differentiation and Identification

We will shortly discuss the presence of non-standard elements in first-order logic. What is new in our approach is that relation $\mapsto \! \! \! \! \! \! \! \! \ {s \above 0pt \ } \$ allows a distinction between standard and non-standard models. Systems for which the inverse of $\mapsto \! \! \! \! \! \! \! \! \ {s \above 0pt \ } \$ (which is the predecessor relation) is a partial surjection, are called standard, all others non-standard. That is, in a standard model objects are not identified at later states whereas non-standard models allow an identification of objects when the domain of elements increase, i.e., $a_0 \mapsto \! \! \! \! \! \! \! \! \ {s \above 0pt \ } \ \, a'$ and $a_1 \mapsto \! \! \! \! \! \! \! \! \ {s \above 0pt \ } \ \, a'$ for $a_0 \not= a_1$ both in $\mathcal{M}_i$ . And as already mentioned, higher-order logic allows a differentiation in contrast to first-order logic, i.e., $a \mapsto \! \! \! \! \! \! \! \! \ {s \above 0pt \ } \ \, a_0$ and $a \mapsto \! \! \! \! \! \! \! \! \ {s \above 0pt \ } \ \, a_1$ for $a_0 \not= a_1$ both in $\mathcal{M}_i$ , see Figure 5.

Let us consider Peano arithmetic. The non-standard elements arising in Henkin's completeness construction are not infinitely large numbers. They are terms for natural numbers that cannot be seen as a number, or for which we do not know, at the current stage of the model construction, to which number it is provable equal. These non-standard elements are usually considered to be beyond all natural numbers $n \in \mathbb{N}$ . A reading of infinite as potential infinite at best shows that the number is larger than all finitely many numbers in the current context, which is easily satisfied by a (standard) natural number due to the indefinite extensibility.

Moreover, Peano arithmetic is a theory with equality, so = is interpreted by the identity. In order to satisfy this condition in the common Henkin-construction, a switch to equivalence classes is done after all elements have been introduced to the model. The two processes ― adding elements to the model on the one side and identifying them if an equality can be proven on the other ― are seen as independently increasing. One is able to complete the first task (adding elements) before starting the second one (identifying them).

With a dynamic reading these processes must be done simultaneously in a direct limit construction with non-injective embeddings. So at each stage of the construction there are typically elements (closed terms) that are known to be provably equal to some $\mathsf{n}$ (i.e., the closed term $\mathsf{S} \dots \mathsf{S}\mathsf{0}$ with n successor symbols $\mathsf{S}$ ). However, at each stage there will always be "unknown" elements due to open terms and also due to Gödel's first incompleteness theorem. In contrast, the usual iterative construction $(\mathbb{N}_i)_{i \in \mathbb{N}}$ of a standard model does not introduce non-standard numbers nor identify elements in further steps. Remind that completeness holds with respect to non-standard models (incl. the standard model), whereas categoricity holds w.r.t. the standard model only. This holds for first- and higher-order logic.

Self Application

The here presented model theory is applicable to its own background model if we apply the idea of indefinitely extensible sets to its meta theory and model. That is, the implicit background model of the here presented model theory makes use of extensible totalities, too. In particular, the index set $\mathcal{I}$ is seen as indefinitely extensible (note that $\mathcal{I}$ does not contain objects of the investigated model $(\mathcal{M}_i)_{i \in \mathcal{I}}$ , but indices are part of the background model). This does not lead to an infinite regress. One might think that, since we replaced $\mathbb{N}$ by $(\mathbb{N}_i)_{i \in \mathbb{N}}$ , the index set must then be replaced in the same way leading to $((\mathbb{N}_i)_{i \in \mathbb{N}_j})_{j \in \mathbb{N}}$ and so on. But we do not have to perpetually replace $\mathbb{N}$ by $(\mathbb{N}_i)_{i \in \mathbb{N}}$ since there never was a completed set $\mathbb{N}$ that had to be replaced. From the very beginning there were only indefinitely extensible sets with states $\mathbb{N}_j$ , and this model theory made this explicit.

In a first reading, the reader may nevertheless regard an index set $\mathbb{N}$ as actual infinite. If she accepts the new interpretation, the reader can go through the definitions, but now with the new understanding of set $\mathbb{N}$ . Then, if we mention set $(\mathbb{N}_i)_{i \in \mathbb{N}}$ , the index set $\mathbb{N}$ refers to some stage $\mathbb{N}_j$ of the background model, i.e., $(\mathbb{N}_i)_{i \in \mathbb{N}}$ is $(\mathbb{N}_i)_{i < j}$ . The requirement w.r.t. the index $j$ is that it must be sufficiently large to describe all investigated models (again, the locution "all" has to be read as "all indefinitely many" as defined previously).

In a type theoretic framework (as explained in Section A Dynamic Type Theory) the situation is slightly different, since there is no index set, but an approximation type. For that reason one should better write $(\mathbb{N}_i)_{i : nat}$ for this a family of sets instead of $(\mathbb{N}_i)_{i \in \mathbb{N}}$ . These function spaces and families of sets are treated in the theory itself. So it is immediately clear that all concepts have a finitistic reading.