November 3
Karel Hrbacek,
CUNY
Nonstandard methods without the Axiom of Choice
Model-theoretic frameworks for nonstandard methods entail the existence of nonprincipal ultrafilters over $\mathbb N$, a strong version of the Axiom of Choice (AC). While AC is instrumental in many abstract areas of mathematics, such as general topology or functional analysis, its use in infinitesimal calculus or number theory should not be necessary.
Mikhail Katz and I have formulated a set theory SPOT in the language that has, in addition to membership, a unary predicate “is standard.” In addition to ZF, the theory has three simple axioms, Transfer, Nontriviality and Standard Part, that reflect the insights of Leibniz. It is a subtheory of the nonstandard set theories IST and HST, but unlike them, it is a conservative extension of ZF. Arguments carried out in SPOT thus do not depend on any form of AC. Infinitesimal calculus can be developed in SPOT as far as the global version of Peano's Theorem (the usual proofs of which use ADC, the Axiom of Dependent Choice). The existence of upper Banach densities can be proved in SPOT.
The conservativity of SPOT over ZF is established by a construction that combines the methods of forcing developed by Ali Enayat for second-order arithmetic and Mitchell Spector for set theory with large cardinals.
A stronger theory SCOT is a conservative extension of ZF+ADC. It is suitable for handling such features as an infinitesimal approach to the Lebesgue measure.
I will also formulate an extension of SPOT to a theory with multiple levels of standardness SPOTS, in which Renling Jin's recent groundbreaking proof of Szemeredi's Theorem can be carried out. While it is an open question whether SPOTS is conservative over ZF, SPOTS + DC (Dependent Choice for relations definable in it) is a conservative extension of ZF + ADC.
Reference: KH and M. G. Katz, Infinitesimal analysis without the Axiom of Choice, Ann. Pure Applied Logic 172, 6 (2021). https://doi.org/10.1016/j.apal.2021.102959, https://arxiv.org/abs/2009.04980