Logic of Effective Definitions

A new logic to deal with properties of algorithmic processes in an abstract structure is proposed. This logic is based on the class of (deterministic) effective definitional schemes. A complete (infinitary) proof system is given. The paper contains among the other results, a “computation” of Hanf number of the above-mentioned logic, which turns out to he unexpectedly high.