Constructive propositional calculus

A logical calculus describing a derivation method for expressions that are valid from the point of view of constructive mathematics. The phrase "constructive propositional calculus" is usually regarded as synonymous with the term intuitionistic propositional calculus. However, under certain special interpretations of constructivism, intuitionistic propositional calculus proves to be incomplete. For example, the well-known formula of Rose,

$$((\neg\neg A\supset A)\supset(\neg\neg A\lor\neg A))\supset(\neg\neg A\lor\neg A),$$

where $A$ is the formula $\neg p\lor\neg q$ and $p,q$ are propositional variables, is not derivable in intuitionistic propositional calculus, and at the same time is identically true in the Kleene interpretation of recursive realizability, at least if the constructive selection principle (or Markov's principle) is accepted. A real problem is the study of the completeness of constructive propositional calculus for different versions of the semantics of constructive mathematics.

References

[1]	S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)
[2]	G.F. Rose, "Propositional calculus and realizability" Trans. Amer. Math. Soc. , 75 (1953) pp. 1–19