Formalization of the Filter Extension Principle (FEP) in Coq

TL;DR

This paper formalizes and verifies the Filter Extension Principle within the Coq proof assistant, providing a rigorous foundation for ultrafilters and their applications in logic and set theory.

Contribution

It offers the first formal proof of the Filter Extension Principle in Coq, enabling further formalization of non-standard analysis and related mathematical theories.

Findings

Formal verification of the Filter Extension Principle in Coq

Rigorous formal descriptions of filters and ultrafilters

Foundation for formalizing non-standard analysis

Abstract

The Filter Extension Principle (FEP) asserts that every filter can be extended to an ultrafilter, which plays a crucial role in the quest for non-principal ultrafilters. Non-principal ultrafilters find widespread applications in logic, set theory, topology, model theory, and especially non-standard extensions of algebraic structures. Since non-principal ultrafilters are challenging to construct directly, the Filter Extension Principle, stemming from the Axiom of Choice, holds significant value in obtaining them. This paper presents the formal verification of the Filter Extension Principle, implemented using the Coq proof assistant and grounded in axiomatic set theory. It offers formal descriptions for the concepts related to filter base, filter, ultrafilter and more. All relevant theorems, propositions, and the Filter Extension Principle itself are rigorously and formally verified. This work sets the stage for the formalization of non-standard analysis and a specific real number theory.