Mathematics with the potential infinite

[Matthias]

Dear James,

regarding the word "translation" for the modal approach, I simply took 
it from the authors (Linnebo and Shapiro). Of course, there is no hard 
borderline between an interpretation and a translation (e.g. one may 
regard an interpretation as a translation in the meta-language...).

There is a difference between a modal logic interpretation and my 
interpretation regarding the reading of the quantifier. In modal logic 
the modal operators in combination with the quantifier leads to 
"possibly exists", "possibly for all",.... In my approach one reads the 
usual quantifiers slightly different, more like "finally exists" and 
"finally for all". To this aim I use a relation "i << j" between stages 
i and j, saying that j is sufficiently large relative to i --- more 
precisely, i is in general a context (i_0, ..., i_{n-1}). Then E.x 
phi(x,y) is interpreted as "if y is taken at stage i and j >> i, then 
there exists an element x at stage j such that phi(x,y)". The relation j 
 >> i is such that any j' >> i would result in the same truth value 
(thanks to the Löwenhein-Skolem construction).

Regarding the identity/equality between worlds. This is indeed the 
crucial part of the system, e.g. the embeddings in a direct system. This 
embedding allows the selection of an "identical" element in a larger 
world (at a later stage). But in an inverse system, used for 
sets/properties, one has different possible successors. For instance, a 
subset M of the natural numbers N at stage i is M_i, a subset of N_i 
={0, ..., i-1}. This set could be M_i or M_i union {i} at stage i+1. In 
my second paper I define systems to model sets of base type objects, 
sets of properties/sets and function spaces.

The induction principle that you stated has already a slight 
translation, the assumption that a successor exists (besides the notions 
"possibly" after the universal quantifier). This is not necessary in my 
approach. However, the interpretation regarding "bigger wolds" that you 
stated is indeed the same as in my approach.

You said "if Wi embeds in Wj, and p1, ..., pn in Wi, then R(p1, ... , 
pn) in Wi iff R(p1, ..., pn) in Wj". This indeed holds in my approach as 
well, but often (as in Kripke semantics) a weaker version is used, 
namely "... then R(p1, ..., pn) in Wj if R(p1, ... , pn) in Wi". This 
weaker version allows an increase of knowledge about objects in a former 
stage.

There is also an issue of function vs. relation in my approach (see my 
remark at the end of my post). But only in case of higher-order 
functions. It might be necessary to replace a function f : N -> N by a 
relation (or a function f* : N -> N -> B with B ={true,false}) and show 
that it is the graph of a function. It is a future work to figure out 
what situations these are exactly and what impact they have.

I also thought about a non-directed index set, but things become more 
complex and unwieldy. So far, this is out of my scope.

Regards,
Matthias

------ Originalnachricht ------
Von "James Moody" <jmsmdy at gmail.com>
An "Matthias" <matthias.eberl at mail.de>
Cc fom at cs.nyu.edu
Datum 25.01.2023 08:45:43
Betreff Re: Mathematics with the potential infinite

>Matthias, I started reading [1] (have not started [2]), but I am 
>wondering about this section where you contrast your interpretation 
>with other interpretations of potential infinite:
>
> > Recently Linnebo and Shapiro [5] suggested to formalize the potential 
>infinite using a modal reading of this notion. They rely on an analysis 
>of the potential infinite worked out by Niebergall [10].
> > All of the mentioned approaches use some translation, restriction or 
>adoptions of the original axioms. Our approach is new, to our 
>knowledge, insofar as it formalizes the notion of an indefinitely large 
>finite as a relation, being part of the interpretation. As a 
>consequence, no manipulation of the axioms is necessary.
>
>From my perspective, your approach sounds similar to a modal approach 
>with transworld identity where the existential quantifier E.x is 
>interpreted as "possibly exists x", and the universal quantifier A.x is 
>interpreted as "forall x possibly".*** The usual semantic duality NOT 
>E.x ~ A.x NOT does not work the same way as in classical logic, since 
>"not possibly exists x phi(x)" entails but is not entailed by "forall x 
>possibly not phi(x)". In the degenerate case where there is only one 
>possible world containing the intended infinite model, however, the 
>duality does hold (so it's a limit phenomenon).
>
>The notion of transworld identity would be just be given by implicit 
>embeddings of finite partial models in the directed system, and we also 
>assume all primitive relations between elements hold iff they hold 
>necessarily: if Wi embeds in Wj, and p1, ..., pn in Wi, then R(p1, ... 
>, pn) in Wi iff R(p1, ..., pn) in Wj. Or expressed more modally, we add 
>the axiom "A iff necessarily A" for A atomic (atomic relations 
>represent "essential" properties / attributes which cannot vary across 
>worlds).
>
>There is obviously the subtle issue of functions, but assuming we are 
>OK representing them as relations with axioms saying "I am the graph of 
>a function", then for example the usual axiom schema for induction in 
>PA is interpreted (without any further translation required), to the 
>following:
>
>Forall y possibly (
>     if (
>         phi(0, y)
>         and forall x possibly (
>              if phi(x, y) then
>              possibly exists s (
>                  Succ(x, s) and phi(s, y)
>              )
>         )
>     then forall x possibly phi(x, y)
>)
>
>For worlds Wi := {0, 1, 2, ..., i-1} (and obvious accessibility 
>relation turning this into a directed system), and simplifying to the 
>case there are no parameters to the formula phi being inducted (for 
>simplicity), this ends up being interpreted as:
>
>if phi(0) and forall x, in some bigger world (
>     if phi(x) then in some even bigger world (
>         exists s Succ(x, s) and phi(s)
>     )
>)
>then forall x, in some bigger world phi(x)
>
>Thinking like Skolem, the "bigger world" here just needs to provide 
>witnesses to the relevant existential statements that might appear in 
>phi. It collapses to the usual interpretation of PA axioms when you 
>take the directed system of possible worlds to be the singleton {N}.
>
>For nested quantifiers, e.g. totality of successor function "A.x E.y 
>Succ(x,y)", there is a another way of reading it as potentialist 
>statement about constructing mathematical objects:  "for any natural 
>number x so far constructed, we can construct new natural numbers so 
>that there exists a successor to x". Then there are subtle issues that 
>an ultrafinitist might be concerned about like whether possible worlds 
>should be allowed to have gaps or not.
>
>Is there a difference between this modal explanation of potential 
>infinite and your presentation? I believe this modal explanation would 
>count as an "interpretation" and not just a "translation", since (aside 
>from the subtlety about functions), it just provides a new modal 
>interpretation to universal and existential quantification. I am 
>wondering if this is equivalent to your presentation, since your notion 
>of "context" sounds similar to how you might track the semantics of 
>nested modal statements that quantify over elements of other possible 
>worlds.
>
>Another somewhat related question: requiring the finite partial models 
>/ worlds to be a directed system seems to me like a condition that 
>avoids a lot of the troubles that Saul Kripke worked on with transworld 
>identity, e.g. you don't have to consider "If in some possible world I 
>had an identical twin, would I be the same as the twin on the left or 
>the twin on the right?", since there is a unique way to embed you (or 
>any particular element of your current world) into any world visible 
>from your world. You could also weaken this condition, however, and end 
>up with a kind of multiverse, with multiple possible completions to an 
>infinite model. In that case, I would guess that the "true" sentences 
>would be those that are true in all of the possible infinite 
>completions that could be obtained from choosing a particular directed 
>subsystem? Have you explored this?
>
>Best,
>James Moody
>
>N.B. (***) For a universe U of (finite) worlds, phi is true in U if phi 
>is true at every world in U. This (together with the worlds forming a 
>directed system) explains why we don't use "necessarily" modality to 
>describe universal quantification.
>
>On Tue, Jan 24, 2023, 5:59 PM Matthias <matthias.eberl at mail.de> wrote:
>>Dear FOM members,
>>
>>for several years I have been engaged in developing mathematics solely 
>>with the concept of the potential infinity. Two publications of mine 
>>are now available.
>>
>>The main idea is to see infinity as an indefinitely extensible finite 
>>and to develop a model theory that uses no (actual) infinite 
>>sets/objects at all. Nevertheless, the usual (classical, 
>>intuitionistic...) reasoning should be allowed. This is possible for 
>>first-order logic, for higher-order logic there are some 
>>particularities (see below).
>>
>>A consequence of using the potential infinite in this way is, for 
>>instance, that the completed set N of all natural numbers does not 
>>exist. On a syntactic level, notations such as "n \in N" can be easily 
>>replaced by a type theoretic notion "n : nat". For the semantic side 
>>the main idea is that it suffices to have indefinitely large initial 
>>parts N_i := {0,...,i-1} of N, such that there is always a part N_i (= 
>>set N at stage i) that behaves exactly as N in the current context of 
>>investigation. So infinite sets are given by indefinitely (or 
>>sufficiently) large finite sets, and what "sufficiently large" means, 
>>depends on the context of the investigation. The context thereby 
>>includes stages of the syntax as well as stages of the model.
>>
>>Developing this approach for first-order logic is possible, provided 
>>one interprets the universal quantifier with an implicit reflection 
>>principle, see [1]. Such an interpretation is necessary, since a naive 
>>interpretation of the universal quantifier by "for all ..." is 
>>equivalent to assume an (actual) infinite domain of objects. This 
>>approach goes back to Jan Mycielski and uses the technique of the 
>>Löwenheim-Skolem theorem (or Levy-Montague reflection principle). 
>>There are no technical difficulties for first-order logic. But since 
>>one cannot use set theory with actual infinite sets, one has to use 
>>higher-order logic in order to talk about objects such as functions, 
>>function spaces or the power set. The main idea here is to consider 
>>systems, i.e., direct systems, inverse systems and generalizations 
>>thereof, see [2].
>>
>>For higher-order logic there are some challenges and differences to 
>>common practice. A difference is that one cannot equate first-order 
>>objects with higher-order objects, even if they are structurally 
>>isomorphic. So the set of abstractly defined real numbers R are not 
>>the same as (equivalence classes of) Cauchy sequences, or Dedekind 
>>cuts etc. An abstractly defined real number, e.g. Euler's number e, is 
>>a single object, whereas the Cauchy sequence with limit e is an 
>>unending process, not a single entity. One needs some mapping in order 
>>to relate them, e.g. lim(s) for a Cauchy sequence s.
>>
>>Each function f : R -> R or f : CS -> CS (CS for Cauchy sequences) is 
>>allowed, also discontinuous functions such as f(x)=0 if x<0 and f(x)=1 
>>otherwise. Nevertheless, in the model all functions are continuous 
>>since an infinite sequence is treated as a potential infinite sequence 
>>and the function space is extensible as well. W.r.t. a function f : CS 
>>-> CS one might say that Brouwer's continuity principle is satisfied 
>>in the model theory, but it is not necessary to formulate this in the 
>>language, allow only continuous functions or use intuitionistic logic.
>>
>>The difference of the set theoretic and this approach become also 
>>visible in the power set construction P(_), e.g. on the set of natural 
>>numbers N. If we understand infinite as potential infinite, the set N 
>>is seen as a direct system, P(N) as an inverse system, and P(P(N)) as 
>>a direct system again. This follows from the construction in [2]. A 
>>direct system is "finitary" in the sense that each element therein 
>>occurs at some stage (and then remains more or less the same), whereas 
>>an inverse system has "infinite elements" --- an element a is given 
>>only by approximations via the projections of a. So different to the 
>>power set construction in a set universe V, where P(P(N)) is "even 
>>more infinite" than P(N), the construction P(P(N)) based on the 
>>potential infinite is finitary again. The reason is (very roughly and 
>>informal) that if a subset A of N is given only by some state A_i and 
>>never as a completed set, then a property/set on A has always to deal 
>>with an unknown part at the end (the "open future development") of A, 
>>so it cannot itself develop arbitrarily, but must be defined by this 
>>very part A_i.
>>
>>One of the main restrictions compared to mathematics with actual 
>>infinite sets is that totality of applying a higher-order functional 
>>to some function does not hold *in general* in the model. Assume that 
>>a functional F : (N -> N) -> N and a function f : N -> N are given. 
>>Then F(f) is not defined in general, only if one can show that this is 
>>the case, e.g., by proving that for all f there exists a value n such 
>>that F(f)=n. Technically, the reason has to do with the existence of 
>>filters on index sets in the model (see [2]).
>>
>>Any feedback is warmly welcome.
>>
>>
>>[1] A Model Theory for the Potential Infinite. Reports on Mathematical 
>>Logic 57, 3-30, 2022.
>>https://rml.tcs.uj.edu.pl/rml-57/01-eberl.pdf
>>
>>[2] Higher-Order Concepts for the Potential Infinite. Theoretical 
>>Computer Science, Volume 945, 2023.
>>https://authors.elsevier.com/a/1gMxJ15DaIAtMa
>>
>>
>>Kind regards,
>>Matthias
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20230125/b25df3ab/attachment-0001.html>