We introduce, in a general setting, an ‘‘analytic’’ version of standard equational calculi of combinatory logic. Analyticity lies on the one side in the fact that these calculi are characterized by the presence of combinatory introduction rules in place of combinatory axioms, and on the other side in that the transitivity rule proves to be eliminable. Apart from consistency, which follows immediately, we discuss other almost direct consequences of analyticity and the main transitivity elimination theorem; in particular the Church−Rosser and (...) the leftmostreduction theorems for the associated notions of reduction. The last two sections deal with analytic combinatory calculi with the extensionality rule added. Here, as far as the elimination of transitivity is concerned, we have only partial results, which unfortunately do not cover, at present, full CL + Ext. Yet, they are sufficient to prove the decidability of weaker combinatory calculi with extensionality, including e.g. BCK + Ext. (shrink)

Extended algorithmic logic (EAL) as introduced in [18] is a modified version of extended +-valued algorithmic logic. Only two-valued predicates and two-valued propositional variables occur in EAL. The role of the +-valued logic is restricted to construct control systems (stacks) of pushdown algorithms whereas their actions are described by means of the two-valued logic. Thus EAL formalizes a programming theory with recursive procedures but without the instruction CASE.The aim of this paper is to discuss EAL and prove the completeness theorem. (...) A complete formalization of EAL was announced in [20] but no proof of the completeness theorem was given. (shrink)