I have in mind something like the following:
Start with some suitable version of "finite" mathematics. Some possibilities might be maybe ZFC with a suitable anti-infinity axiom, the topos $\mathbf{FinSet}$, Peano arithmetic, Turing machines… something whose objects are suitably "finite".
Then, posit the existence of both a standard and a non-standard model.
Now, in this setting, where we have access both to a standard model and a non-standard extension, use the non-standard objects as proxies for infinite objects (e.g. maybe some sort of set theory that has a set of natural numbers), and develop ordinary mathematics this way.
Has anybody worked on such a thing? Does anyone know of references of it being done? Or suggestions that it can't work out?
(P.S. I wasn't sure how to tag this….)
Edit: After more thought and reviewing the answers thus far, I think I can state an example of the sort of thing i was imagining. Define a first-order theory with two types $T_1$ and $T_2$, two binary relation symbols $\in_1, \in_2$ (one for each sort), and a map $\tau : T_1 \to T_2$ satisfying:
- $(T_1, \in_1)$ satisfies the axioms of finite set theory
- $(T_2, \in_2)$ satisfies the axioms of finite set theory
- $\tau$ is injective
- $\tau$ is not surjective
- $\tau$ satisfies an axiom schema that says it's an elementary embedding
and the question is to what extent we can develop infinite set theory in this theory.
Best Answer
The standard system of a first-order model of Peano Arithmetic works in this way.
The standard model $\mathbb{N}$ is an initial segment of every nonstandard model $\mathcal{M}$. Pick a nonstandard element $w$ of $\mathcal{M}$. The binary expansion of numbers in $\mathcal{M}$ below $2^w$ define nonstandard binary strings of length $w$. For each such $x$, there corresponds a subset $X$ of $\mathbb{N}$ where a standard number $n$ belongs to $X$ if and only if the $n$-th bit of $x$ is $1$. The collection of all these sets $X$ is called the standard system $\mathrm{SSy}(\mathcal{M})$ of $\mathcal{M}$. This standard system is always a Scott set, so it can be used to form a standard model of second-order arithmetic where the weak König lemma is true. The structure of the first-order model $\mathcal{M}$ dictates a lot of the properties of this second-order model.
Similar constructions can be done in different contexts, but this is surely the most common one.