Decision-procedures for invariant properties of short algorithms

For a class of algorithms R satisfying sufficiently general conditions and an enumeration of the algorithms of this class, it is proved that if the algorithm from R with code m in this enumeration algorithmically decides a property, nontrivial to N₁ and invariant (with respect to extensional equality) up to N, then for N max (t²(c)t⁵(N₁, t²(a)) one has m t^–3(N), where the constantsa, c and the function t are indicated in the text of the paper, t^–3(N) is used instead of t^–1(t^–1(t^–1(N))), and finally, t^–1(x)=yxt(y)x]. For natural enumerations the constantsa, c are not large, and the function t does not grow too rapidly. From the result obtained also follows a generalization of a theorem of Rice in a form close to that proved in 2].Translated from Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V. A. Steklova AN SSSR, Vol. 88, pp. 73–76, 1979.In conclusion, the author thanks the participants in the Leningrad seminar on mathematical logic for valuable comments.