Unavoidable sequences in constructive analysis

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 Π¹₁ formula is unavoidable (cannot fail to exist) and that no sequence can fail to be classically Δ¹₁. 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)