Brouwer's Fan Theorem (FT) is an important result in constructive mathematics, stating a continuity property. However, this statement is not true in general, particularly in a realizability setting. Realizability models satisfying FT still exist, for example in Kleene's second realizability algebra.

In 2013, Lubarsky and Rathjen gave another realizability model satisfying FT using a weaker language for its realizers. Based on this work, we construct a new model realizing FT with a lambda-calculus with oracle.

Thanks to this model and using the notion of Evidenced Frame, we give a general theorem giving a sufficient condition for any computational system to realize FT in a realizability interpretation. We advocate that this method can lead to a deeper understanding of the computational content of several axiom by giving theorems that account for a broad enough class of computational systems.

In this talk, I will describe the realizability model inspired by Lubarsky and Rathjen (after recalling the statement of FT and how realizability works) and present how we generalize it to a statement about general computational systems.

This is a joint work with Etienne Miquey.