Difference between revisions of "Constructive propositional calculus"
From Encyclopedia of Mathematics
(Importing text file) |
(TeX) |
||
| Line 1: | Line 1: | ||
| + | {{TEX|done}} | ||
A [[Logical calculus|logical calculus]] describing a derivation method for expressions that are valid from the point of view of [[Constructive mathematics|constructive mathematics]]. The phrase "constructive propositional calculus" is usually regarded as synonymous with the term [[Intuitionistic propositional calculus|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, | A [[Logical calculus|logical calculus]] describing a derivation method for expressions that are valid from the point of view of [[Constructive mathematics|constructive mathematics]]. The phrase "constructive propositional calculus" is usually regarded as synonymous with the term [[Intuitionistic propositional calculus|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 | + | 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|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==== | ====References==== | ||
<table><TR><TD valign="top">[1]</TD> <TD valign="top"> S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top"> G.F. Rose, "Propositional calculus and realizability" ''Trans. Amer. Math. Soc.'' , '''75''' (1953) pp. 1–19</TD></TR></table> | <table><TR><TD valign="top">[1]</TD> <TD valign="top"> S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top"> G.F. Rose, "Propositional calculus and realizability" ''Trans. Amer. Math. Soc.'' , '''75''' (1953) pp. 1–19</TD></TR></table> | ||
Latest revision as of 13:34, 17 March 2014
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
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