I have an argument of the following form:
Executive Summary:
We have a $\mathbb R$-valued function $L$ which we want to show is $\mathbb Z$-valued. We approximate it by $\mathbb Q$-valued functions $\lim_{n \to \infty} L_n = L$. Magically, when we take this limit as an ultralimit in a bigger field $\mathcal R = \prod_{\mathcal F} \mathbb R$, we still get $L$, which tells us that $L$ is $\mathbb Q$-valued. We have control over the denominators to see that $L$ is $\mathbb Z$-valued.
EDIT: Here is a pdf (2 pages) with the complete argument.
Question: Can such an argument be conceptually streamlined by more systematically employing tools / language from model theory / nonstandard analysis / forcing — or maybe just from number theory?
Here is a more detailed summary:
Theorem Sketch: Let $C$ be a set equipped with two distinguished elements $0,1$ and a ternary relation $\Delta \subseteq C^3$ satisfying certain axioms [1]. Let $L : C \to \mathbb R_{\geq 0}$ be a “gapped norm” — a function satisfying certain inequalities [2]. Then $L$ is integer-valued.
Proof Sketch:
Step 0: Choose a prime $p$.
Step 1: Construct a sequence of functions $\lceil L \rceil =L_0 \geq L_1 \geq \dotsb \geq L : C \to \mathbb N[1/p]$ which decreases pointwise from the least integer $\geq L$ down to $L$ itself. The construction is such that every “norm” inequality is satisfied by $L_n$ for all but finitely many $n$ [4], along with some other “forcing” conditions which will be useful in Step 3 [5].
Step 2: Choose a nonprincipal ultrafilter $\mathcal F$ on the finite-powerset-lattice of the set of “norm” inequalities. Let $L_\infty : C \to \mathcal R := \prod_\mathcal{F} \mathbb R$ be the “ultralimit” of the $L_n$’s, but with values in the ultrapower field $\mathcal R$ (i.e. $L_\infty(C)(n) := L_n(C)$).
Step 3: Observe that by construction, we have $L_\infty \geq L$. Argue inductively [6] using the additional “forcing” conditions from Step 1 that the reverse inequality also holds, so that $L = L_\infty$.
Step 4: Since the equation $L = L_\infty$ is independent of the choice of $\mathcal F$ from Step 2, conclude that for each $X \in \mathcal C$, the sequence $n \mapsto L_n(X)$ is eventually constant, so that $L_\infty(X) = L(X) \in \mathbb N[1/p]$.
Step 5: Since the prime $p$ from Step 0 was arbitrary, we have $L(X) \in \mathbb N$ for all $X \in \mathcal C$ as desired.
Notes:
I think this form of argument must be a “standard forcing argument” in some sense. My guess, in fact, would be that there are some fields of logic where arguments of exactly the above form are considered “routine”, as well as other fields of logic where one might not routinely make arguments of exactly the above form but nevertheless the pieces are all quite familiar and the whole thing together looks quite natural.
By contrast, in algebraic topology (where I intend to make this argument) these tools are all quite unfamiliar, so that I think I am bumbling around and not putting things very elegantly.
I also suspect that a typical number theorist would find it very straightforward to make an argument equivalent to the above one, except that they would somehow never mention ultrafilters. I would also be keen to hear about an ultrafilter-free way to think about an argument like this one.
I’m also reminded of the fact that Cohen was an analyst, and some (to-me-cryptic) quote of his indicating that when he originally introduced forcing, he was “just” adapting some sort of (well-known?) analytic techniques to logic. I say this because the above argument only occurred to me after a very long period of becoming well-acquainted with the “minimization” procedure in footnote [3] below, which I thought of as very much an “analytic” phenomenon.
Footnotes:
[1]: The axioms say that $C$ is the object set of a triangulated category with $0$ the zero object and $\Delta$ the set of triples $X,Y,Z$ such that there exists a triangle $X \to Y \to Z$. Moreover, we impose the “monogencity” requirement that $C$ be generated by $1$ in the sense that the smallest triangulated subcategory of $C$ containing $1$ is $C$ itself.
[2]: The “norm” axioms say that $L(0) = 0$, $L(1) \leq 1$, and whenever $(X,Y,Z) \in \Delta$ we have $L(Y) \leq L(X) + L(Z)$. The norm is “gapped” if $L(1) = 1$ and $L(X) \leq 1 \implies L(X) = 0 \vee L(X) = 1$. I think of this condition as a sort of “seed” of integrality which the theorem “spreads” to the rest of $C$ like a crystalizing liquid :) Technically, we also require that a “gapped” norm satisfy $L(X \oplus Y) = L(X) + L(Y)$ and $L(X[1]) = L(X)$, which I suppose can’t quite be stated without referring to the triangulated structure in footnote [1], but I don’t think that’s important to the outline of the argument.
[3]: It seems to be relevant that these “norm inequalities” are set up in such a way that if $f : C \to \mathbb R_{\geq 0}$ is an arbitrary function, then there is a unique maximal $\mathbb R_{\geq 0}$-valued norm $L \leq f$, which can be obtained from $f$ by a straightforward “greedy minimization” procedure — if some “norm” inequality is violated, then just decrease the relevant value of $f$ to “force” it to be satisfied. Rinse and repeat. At any rate, the fact that this is so allows us to conclude already in step 2 that the “standard part” of $L_\infty(X)$ is exactly $L(X)$.
[4]: Moreover, any $\mathbb R_{\geq 0}$-valued function $\leq \lceil L \rceil$ which satisfies all of the “norm” inequalities must equal $L$. In practice the construction proceeds by listing out all of the “norm” inequalities which must be satisfied, and then guaranteeing that $L_n$ satisfies the first $n$ of them. But I don’t think this point is crucial.
[5]: Although these additional conditions are in some sense the crux of the proof, I think for the current question their precise form is not so important. In case I’m wrong about this: they say that if $(X,Y,Z) \in \Delta$, and if $L(X),L(Z) < L(Y)$, then for all but finitely many $n$ we have $L_n(X) - L_n(Y) + L_n(Z) \geq L(X) - L(Y) + L(Z)$.
[6]: The induction is over the “number of cells” in $X \in \mathcal C$ (which makes sense due to the “monogenicity” requirement in footnote [1]), which feels somehow akin to inducting over the “length of the name” of $X \in \mathcal C$….