Formalization of Filter-Method Construction for Real Numbers in Coq

Guowei Dou; Wensheng Yu

Home/Archive/arXiv

arXiv · 2611.09134

Formalization of Filter-Method Construction for Real Numbers in Coq

Guowei Dou·Wensheng Yu

View original source ↗Read source document ↗Export metadata ↓

Abstract

This paper presents a formalization for a theory of constructing real numbers using concepts related to filters. The formalization is implemented using the Coq proof assistant and is grounded in axiomatic set theory. The theory encompasses various notions such as filters, ultrafilters, principal ultrafilters, and arithmetical ultrafilters. A special filter, namely the non-principal arithmetical ultrafilter, whose existence requires the Continuum Hypothesis to be proven, is employed to establish several non-standard number sets: *N, *Z and *Q. The set of real numbers, R, is subsequently derived by equivalently classifying a specific subset of *Q. The entire theory is thoroughly formalized, with each detail verified to ensure rigor and precision. This work contributes a new selection of foundational materials for the formalization of mathematical theories.

Explore related subjects

math.LO

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Guowei Dou, Wensheng Yu. 2026-11-06. Formalization of Filter-Method Construction for Real Numbers in Coq. https://arxiv.org/abs/2611.09134

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

A Dubnov-Ivanov-Nagata-Higman Theorem for NIP nilrings

We prove that NIP nilrings of bounded nilexponent are nilpotent. We also deduce that NIP $ω$-categorical $n$-Engel Lie algebras of characteristic $p>n$ are nilpotent, yielding a case of the Lie algebra analogous of Wilson conjecture for $ω$-categorical groups.

math.LO↗

arXiv2026

A simplified proof of the o-minimal Whitney Extension Theorem

We give a proof of the o-minimal version of the Whitney Extension Theorem simplified as compared to the original ones. A new simplifying ingredient is a definable variant of Urysohn's lemma for class $\mathcal{C}^q$ (see Section 3).

math.LO↗

arXiv2026

Keisler Measures and Generically Stable Random Types

We introduce the notions of $rgs$ and $irgs$ for Keisler measures, motivated by the study of generically stable random types and their associated Morley sequences. We obtain characterizations of these notions in terms of averages of classical first-order formulas over suitable probabilistic partitions (Theorems 3.2 and 3.3). We compare these notions with $fim$, $fam$, and self-averaging, and show that for types the notions $fim$, $irgs$, and $rgs$ coincide. We prove that if a definable global Keisler measure$μ$ is not dependent, then every Morley sequence in its canonical random extension $r_μ$ is divergent (Theorem 4.7). Consequently, every $irgs$ measure is dependent (Corollary 4.8) and hence symmetric (Corollary 4.13). Furthermore, we show that for $irgs$ measures the model-theoretic instability events $\mathbf{O}^φ$, $\mathbf{I}^φ$, and $\mathbf{L}^φ$ have $\mathbb{P}_μ$-measure zero (Theorem 5.4). In view of the equivalence of $fim$ and $irgs$ subsequently established in [6], this provides an alternative proof of the corresponding result for $fim$ measures in [9].

math.LO↗