Definability in algorithmic logic

Abstract

In this paper we consider recursive implicit definitions of functors and predicates in algorithmic logic [1], [5], [9], which may be regarded as procedures (compare A. Salwicki [10]). We examine the possibility of elimination of defined symbols from algorithmic formulas. We prove that the halting property of a procedure is not definable by means of formulas of extended algorithmic logic [1] (with classical quantifiers). As corollary we obtain that extended algorithmic logic has not Beth-property.