Unavoidable sequences in constructive analysis
Joan Rand Moschovakis · Mathematical logic quarterly · 2010
Five recursively axiomatizable theories extending Kleene's intuitionistic theory FIM of numbers and numbertheoretic (choice) sequences are introduced and shown to be consistent, by a modified relative realizability interpretation which verifies that every sequence classically defined by a Π11 formula is unavoidable (cannot fail to exist) and that no sequence can fail to be classically Δ11. The analytical form of Markov's Principle fails under the interpretation. The notion of strongly inadmissible rule of inference is introduced, with examples (© 2010 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim)