Abstract

We consider the construction of the Baigger counter-example in constructive analysis for the Brouwer fixed-point theorem. There exists an actual (Polish school) computable function mapping the unit square to itself, all the fixed points of which are non-computable points and therefore algorithmically indeterminable. The algorithm computing the Baigger function uses the Kleene tree, a famous infinite computable tree which has no computable infinite path and giving an actual example of the tree (of which there are many equivalent) is part of the problem. We show how to do this using the exotic Fractran language, interpreted in Python. This allows definition of the Baigger function from the bottom up.

• Baigger, G.: Die Nichtkonstruktivität des Brouwerschen Fixpunktsatzes. Arch. Math. Logik Grundlag. 25(3-4) (1985) 183–188
• Brattka, V,, Le Roux, S., Miller, J.S., Pauly, A. Connected choice and the Brouwer fixed point theorem. Journal of Mathematical Logic 19 (2019).
• Pour-El, M.B., Richards, J.I.: Computability in analysis and physics. Perspectives in Mathematical Logic. Springer- Verlag, Berlin (1989)
• Tanaka, Y. On Constructive versions of the tychonoff and Schauder fixed point theorems. Applied Mathematics E-Notes 11 (2011) 125-132