TOPICS
Search

Intuitionistic Logic


The proof theories of propositional calculus and first-order logic are often referred to as classical logic.

Intuitionistic propositional logic can be described as classical propositional calculus in which the axiom schema

 ¬¬F=>F
(1)

is replaced by

 ¬F=>(F=>G).
(2)

Similarly, intuitionistic predicate logic is intuitionistic propositional logic combined with classical first-order predicate calculus.

Intuitionistic logic is a part of classical logic, that is, all formulas provable in intuitionistic logic are also provable in classical logic. Although, even some basic theorems of classical logic do not hold in intuitionistic logic. Of course, the law of the excluded middle

 F v ¬F
(3)

does not hold in intuitionistic propositional logic.

Here are some examples of propositional formulas that are not provable in intuitionistic propositional logic:

 ¬(F ^ G)=¬F v ¬G
(4)
 F v G=¬F=>G.
(5)

Here are some examples of first-order formulas that are not provable in intuitionistic predicate logic:

 F v  forall xG(x)= forall x(F v G(x))
(6)
 F=> exists xG(x)= exists x(F=>G(x)).
(7)

Truth tables for propositional connectives define the interpretation of classical propositional calculus over the domain of two elements: true and false. This interpretation is a model of classical propositional calculus, that is, tautologies and only tautologies are formal theorems. In contrast, intuitionistic propositional calculus does not have a finite model but it has countable models.

Proofs by contradiction are not permissible in intuitionistic logic. All intuitionistic proofs are constructive, which is justified by the following properties. Intuitionistic propositional logic has the disjunction property: If F v G is provable in intuitionistic propositional calculus, then either F or G is provable in intuitionistic propositional calculus. Intuitionistic predicate logic has the existence property: If  exists xF(x) is a formula without free variables, and it is provable in intuitionistic predicate logic, then there is term t without free variables such that F(t) is provable in intuitionistic predicate logic.

The deduction theorem holds in intuitionistic propositional and predicate logics. The following theorem by Glivenko captures the essence of relation between intuitionistic and classical logics: If F is provable in classical propositional calculus, then ¬¬F is provable in intuitionistic propositional calculus. Note that this theorem cannot be extended onto intuitionistic predicate logic.


See also

First-Order Logic, Logic, Propositional Calculus

This entry contributed by Alex Sakharov (author's link)

Explore with Wolfram|Alpha

References

Kleene, S. C. Introduction to Metamathematics. Princeton, NJ: Van Nostrand, p. 39, 1964.Kleene, S. C. Mathematical Logic. New York: Dover, 2002.Mints, G. A Short Introduction to Intuitionistic Logic. Amsterdam, Netherlands: Kluwer, 2000.Novikov, P. S. Constructive Mathematical Logic from the Viewpoint of the Classical One. Moscow: Nauka, 1977.

Referenced on Wolfram|Alpha

Intuitionistic Logic

Cite this as:

Sakharov, Alex. "Intuitionistic Logic." From MathWorld--A Wolfram Web Resource, created by Eric W. Weisstein. https://mathworld.wolfram.com/IntuitionisticLogic.html

Subject classifications