Difference between revisions of "Intuitionistic propositional calculus"
(Importing text file) |
(TeX) |
||
| Line 1: | Line 1: | ||
| + | {{TEX|done}} | ||
A [[Logical calculus|logical calculus]] describing rules for the derivation of propositions that are valid from the point of view of [[Intuitionism|intuitionism]]. The generally accepted formulation of intuitionistic propositional calculus was proposed by A. Heyting in 1930. Its fundamental difference from classical propositional calculus is in the replacement of the [[Law of the excluded middle|law of the excluded middle]] (or the law of double negation) by the weaker contradiction principle | A [[Logical calculus|logical calculus]] describing rules for the derivation of propositions that are valid from the point of view of [[Intuitionism|intuitionism]]. The generally accepted formulation of intuitionistic propositional calculus was proposed by A. Heyting in 1930. Its fundamental difference from classical propositional calculus is in the replacement of the [[Law of the excluded middle|law of the excluded middle]] (or the law of double negation) by the weaker contradiction principle | ||
| − | + | $$A\supset(\neg A\supset B).$$ | |
| − | A common variant of intuitionistic propositional calculus is formulated as follows. Let | + | A common variant of intuitionistic propositional calculus is formulated as follows. Let $A,B,C$ be arbitrary formulas in the logical language considered. The axioms of the calculus are the following formulas: |
| − | 1) | + | 1) $A\supset(B\supset A)$; |
| − | 2) | + | 2) $(A\supset B)\supset((A\supset(B\supset C))\supset(A\supset C))$; |
| − | 3) | + | 3) $A\supset(B\supset A\land B)$; |
| − | 4) | + | 4) $A\land B\supset A$; |
| − | 5) | + | 5) $A\land B\supset A$; |
| − | 6) | + | 6) $A\supset A\lor B$; |
| − | 7) | + | 7) $B\supset A\lor B$; |
| − | 8) | + | 8) $(A\supset C)\supset((B\supset C)\supset(A\lor B\supset C))$; |
| − | 9) | + | 9) $(A\supset B)\supset((A\supset\neg B)\supset\neg A)$; |
| − | 10) | + | 10) $A\supset(\neg A\supset B)$. |
| − | The only derivation rule of intuitionistic propositional calculus is the rule of modus ponens: If formulas | + | The only derivation rule of intuitionistic propositional calculus is the rule of modus ponens: If formulas $A$ and $A\supset B$ are derivable, then $B$ is derivable. |
Every derivable formula of this calculus is valid from the intuitionistic point of view; the problem of completeness of the calculus described is more subtle. Intuitionistic propositional calculus is complete, e.g., with respect to algebraic semantics, the Kripke and Beth models, but it is incomplete with respect to the [[Recursive realizability|recursive realizability]] interpretation of Kleene; see also [[Constructive propositional calculus|Constructive propositional calculus]]. | Every derivable formula of this calculus is valid from the intuitionistic point of view; the problem of completeness of the calculus described is more subtle. Intuitionistic propositional calculus is complete, e.g., with respect to algebraic semantics, the Kripke and Beth models, but it is incomplete with respect to the [[Recursive realizability|recursive realizability]] interpretation of Kleene; see also [[Constructive propositional calculus|Constructive propositional calculus]]. | ||
For references, see [[Intuitionism|Intuitionism]]. | For references, see [[Intuitionism|Intuitionism]]. | ||
Revision as of 13:31, 17 March 2014
A logical calculus describing rules for the derivation of propositions that are valid from the point of view of intuitionism. The generally accepted formulation of intuitionistic propositional calculus was proposed by A. Heyting in 1930. Its fundamental difference from classical propositional calculus is in the replacement of the law of the excluded middle (or the law of double negation) by the weaker contradiction principle
$$A\supset(\neg A\supset B).$$
A common variant of intuitionistic propositional calculus is formulated as follows. Let $A,B,C$ be arbitrary formulas in the logical language considered. The axioms of the calculus are the following formulas:
1) $A\supset(B\supset A)$;
2) $(A\supset B)\supset((A\supset(B\supset C))\supset(A\supset C))$;
3) $A\supset(B\supset A\land B)$;
4) $A\land B\supset A$;
5) $A\land B\supset A$;
6) $A\supset A\lor B$;
7) $B\supset A\lor B$;
8) $(A\supset C)\supset((B\supset C)\supset(A\lor B\supset C))$;
9) $(A\supset B)\supset((A\supset\neg B)\supset\neg A)$;
10) $A\supset(\neg A\supset B)$.
The only derivation rule of intuitionistic propositional calculus is the rule of modus ponens: If formulas $A$ and $A\supset B$ are derivable, then $B$ is derivable.
Every derivable formula of this calculus is valid from the intuitionistic point of view; the problem of completeness of the calculus described is more subtle. Intuitionistic propositional calculus is complete, e.g., with respect to algebraic semantics, the Kripke and Beth models, but it is incomplete with respect to the recursive realizability interpretation of Kleene; see also Constructive propositional calculus.
For references, see Intuitionism.
Intuitionistic propositional calculus. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Intuitionistic_propositional_calculus&oldid=31387