Namespaces
Variants
Actions

Constructive propositional calculus

From Encyclopedia of Mathematics
Jump to: navigation, search

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
How to Cite This Entry:
Constructive propositional calculus. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Constructive_propositional_calculus&oldid=31388
This article was adapted from an original article by A.G. Dragalin (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article