Definability in algorithmic logic

Article type: Research Article

Authors: Dańko, Wiktor

Affiliations: University of Warsaw, Division Bialystok

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.

Keywords: algorithmic logic, definability in algorithmic logic, implicit definitions, essentiality of procedures, halting property

DOI: 10.3233/FI-1978-2118

Journal: Fundamenta Informaticae, vol. 2, no. 1, pp. 277-287, 1978