  Constructive arithmetic, or the Markov arithmetic MA, is obtained from
intuitionistic arithmetic HA by adding the following two principles: the Markov
principle M which distinguishes constructivism from intuitionism, and the
so-called extended Church thesis ECT, which distinguishes constructive
semantics from classical semantics. The first principle is expressed by a
predicate formula, but ECT is formulated as a scheme in the arithmetical
language. Some earlier results of the authors make possible to replace the
scheme ECT by a pure predicate formula. This gives a predicate calculus MQC
which can serve as a logical basis for constructive arithmetic. Namely,
arithmetical theory based on MQC and Peano axioms proves all formulas deducible
in MA. Note that MQC is not an intermediate calculus between intuitionistic and
classical logics: it proves some formulas that are not deducible in the
classical predicate calculus.
  Bibliography: 12 items.
