Separating the Fan Theorem and Its Weakenings

TL;DR

This paper constructs Kripke models to differentiate various versions of the Fan Theorem in reverse constructive mathematics, clarifying their logical relationships and hierarchy.

Contribution

It introduces a family of Kripke models that separate all known variants of the Fan Theorem, advancing understanding of their implications.

Findings

Separates all known variants of the Fan Theorem

Establishes strict implications and non-implications among them

Provides a unified model framework for analysis

Abstract

Varieties of the Fan Theorem have recently been developed in reverse constructive mathematics, corresponding to different continuity principles. They form a natural implicational hierarchy. Some of the implications have been shown to be strict, others strict in a weak context, and yet others not at all, using disparate techniques. Here we present a family of related Kripke models which separates all of the as yet identified fan theorems.