On certain constructive predicate calculus

TL;DR

This paper introduces a new predicate calculus MQC that serves as a logical foundation for constructive arithmetic, incorporating the Markov principle and an extended Church thesis, and surpasses classical logic in some derivations.

Contribution

The authors develop MQC, a predicate calculus that replaces the ECT scheme with a predicate formula, providing a new logical basis for constructive arithmetic.

Findings

MQC can prove all formulas deducible in MA.

MQC proves some formulas not derivable in classical predicate calculus.

The calculus bridges constructive and classical semantics with new logical capabilities.

Abstract

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.