On the Quantifier-Free Fragment of ‘Logic of Effective Definitions’

Article type: Research Article

Authors: Bergstra, Jan A.^a | Meyer, John J.Ch.

Affiliations: [a] Department of Computer Science, University of Leiden, Wassenaarseweg 80, Postbus 9512, 2300 RA Leiden, The Netherlands

Abstract: In [2] Jerzy Tiuryn has introduced Logic of Effective Definitions (LED) in which properties of effective definitional schemes are expressed. With respect to the quantifier-free part of it, he proved that each open formula is equivalent to one in a special conjunctive normal form. We prove that there is no finite bound to the number of conjuncts required for these normal forms.

Keywords: algorithmic logic, computability, algebraic structures, functional effective definitional schemes

DOI: 10.3233/FI-1981-4409

Journal: Fundamenta Informaticae, vol. 4, no. 4, pp. 935-955, 1981