Abstract:
A variety of constructive mathematics, known as Russian Recursive Constructive Mathematics (RRCM), has been considered to be characterized by two axioms: the semi-classical principle called Markov's principle (MP) and Church's Thesis (CT) or its extended variant (ECT). The latter basically asserts that any function has a recursive index, and is known to be inconsistent with Brouwer's principle, namely the continuity of all functions on Baire space. I modify Church's Thesis with negative or classical existence (NCT), and show, by a realizability model, that it is consistent with Brouwer's principle as well as with many important consequences of the original CT or ECT. Intuitively, CT requires that if a function is given then its code is also given, whereas NCT does not require it but only that any function is recursive (without index being given). I would like to know the opinions especially from today's Russian logicians about this new principle with respect to RRCM, a Russian tradition from Markov.
