On the Quantifier-Free Fragment of ‘Logic of Effective Definitions’
Jan Aldert Bergstra, J-J.Ch. Meyer · Fundamenta Informaticae · 1981
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.