Namespaces
Variants
Actions

Difference between revisions of "Intuitionistic propositional calculus"

From Encyclopedia of Mathematics
Jump to: navigation, search
(TeX)
(MSC 03B20)
 
Line 1: Line 1:
{{TEX|done}}
+
{{TEX|done}}{{MSC|03B20}}
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]] 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\supset(\neg A\supset B).$$
Line 28: Line 29:
 
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.
 
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]] interpretation of Kleene; see also [[Constructive propositional calculus]].
  
For references, see [[Intuitionism|Intuitionism]].
+
For references, see [[Intuitionism]].

Latest revision as of 21:33, 15 December 2015

2020 Mathematics Subject Classification: Primary: 03B20 [MSN][ZBL]

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.

How to Cite This Entry:
Intuitionistic propositional calculus. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Intuitionistic_propositional_calculus&oldid=36947
This article was adapted from an original article by A.G. Dragalin (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article