This article is cited in 5 papers

On arithmetic complexity of certain constructive logics

V. E. Plisko

M. V. Lomonosov Moscow State University

Abstract: A constructive arithmetical theory is an arbitrary set of closed arithmetical formulas that is closed with respect to derivability in an intuitionsitic arithmetic with the Markov principle and the formal Church thesis. For each arithmetical theory $T$ there is a corresponding logic $L(T)$ consisting of closed predicate formulas in which all arithmetic instances belong to $T$. For so-called internally enumerable constructive arithmetical theories with the property of existentiality, it is proved that the logic $L(T)$ is $\Pi_1^T$-complete. This implies, for example, that the logic of traditional constructivism is $\Pi_2^0$-complete.

UDC: 510.64

Received: 10.01.1990

 English version: Mathematical Notes, 1992, 52:1, 701–709

Bibliographic databases:

• 
• 
•