# [FOM] Symmetry and Infinity

matthias matthias.eberl at mail.de
Thu Dec 20 15:58:41 EST 2018

```Dmytro Taranovsky wrote
<--
[...] we have a sufficiently fast-growing n+1-tuple, x_0 << x_1 << ...
<< x_n, then a Sigma-0-n statement with size <x_0 is equivalent to
thereis y_1 < x_1 forall y_2 < x_2 thereis y_3 < x_3 ..., [...]
-->

There could be a connection of your notion "sufficiently fast-growing"
to the idea of the indefinitely large finite of Lavine based on a paper
of Mycielski. Let me shortly describe this idea in model theoretic terms
(actually, Mycileski’s original presentation uses a translation and
explicit bounds in the language):

Each set is seen as indefinitely increasing, formally it is a family of
finite sets M_i. So we can introduce the notion "index i is
sufficiently/indefinitely large relative to other indices i_1,...,i_n",
let us write i_1,...,i_n << i for that. The model theoretic notion of |=
A[a_1,...,a_n] (formula A is valid under assignment a_1,...,a_n) becomes
|= A[a_1,...,a_n : i_1,...,i_n] (requiring that each a_k lies within
M_k) and then the quantifier range over a finite set M_i whereby i
satisfies i_1,...,i_n << i. So one needs only finite sets to interpret
formulas and the interpretation is sound and complete w.r.t. classical
first order theories (a similar construction applies to intuitionistic
logic and Kripke models).

In this approach there is no restriction on the complexity of the
formulas (Sigma-0-n, ...). But a key observation is that the concrete
relation << may depend on "outer" factors, as e.g. some bound to the
number of formulas in scope. The length of i_1,...,i_n << i (in fact,
also the indices in i_1,...,i_n are related by <<) is the maximal number
of nested bound variables in a formula. And the "distance" between
i_1,...,i_n and i depends on where the witnesses of existential
quantified formulas in scope lie.

Kind regards,
Matthias
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20181220/22e3bdb4/attachment.html>
```