Namespaces
Variants
Actions

Difference between revisions of "Intuitionistic propositional calculus"

From Encyclopedia of Mathematics
Jump to: navigation, search
(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
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/i/i052/i052170/i0521701.png" /></td> </tr></table>
+
$$A\supset(\neg A\supset B).$$
  
A common variant of intuitionistic propositional calculus is formulated as follows. Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/i/i052/i052170/i0521702.png" /> be arbitrary formulas in the logical language considered. The axioms of the calculus are the following formulas:
+
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) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/i/i052/i052170/i0521703.png" />;
+
1) $A\supset(B\supset A)$;
  
2) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/i/i052/i052170/i0521704.png" />;
+
2) $(A\supset B)\supset((A\supset(B\supset C))\supset(A\supset C))$;
  
3) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/i/i052/i052170/i0521705.png" />;
+
3) $A\supset(B\supset A\land B)$;
  
4) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/i/i052/i052170/i0521706.png" />;
+
4) $A\land B\supset A$;
  
5) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/i/i052/i052170/i0521707.png" />;
+
5) $A\land B\supset A$;
  
6) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/i/i052/i052170/i0521708.png" />;
+
6) $A\supset A\lor B$;
  
7) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/i/i052/i052170/i0521709.png" />;
+
7) $B\supset A\lor B$;
  
8) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/i/i052/i052170/i05217010.png" />;
+
8) $(A\supset C)\supset((B\supset C)\supset(A\lor B\supset C))$;
  
9) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/i/i052/i052170/i05217011.png" />;
+
9) $(A\supset B)\supset((A\supset\neg B)\supset\neg A)$;
  
10) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/i/i052/i052170/i05217012.png" />.
+
10) $A\supset(\neg A\supset B)$.
  
The only derivation rule of intuitionistic propositional calculus is the rule of modus ponens: If formulas <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/i/i052/i052170/i05217013.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/i/i052/i052170/i05217014.png" /> are derivable, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/i/i052/i052170/i05217015.png" /> 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|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.

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