intuitionist logic

intuitionist logic

Incorrect term for "intuitionistic logic".
This article is provided by FOLDOC - Free Online Dictionary of Computing (
The following article is from The Great Soviet Encyclopedia (1979). It might be outdated or ideologically biased.

Intuitionist Logic


the form of predicate calculus that reflects intuitionism’s view of the nature of logical laws acceptable, from its point of view, for proofs of propositions in those areas of the deductive sciences (especially mathematics) that are essentially related to the concept of mathematical infinity.

In accordance with the views of intuitionism, there is no law of the excluded middle or law of removal of double negation in intuitionist logic. A formal logical system constructed by the Dutch mathematician A. Heyting in 1930, which covers the predicate calculus, is usually viewed as intuitionist logic. Even earlier, based on nonintuitionist considerations, a system of intuitionist logic as applied to the propositional calculus, a part of predicate calculus, was constructed by the Soviet scholar V. I. Glivenko. Heyting’s intuitionist logic is distinguished in that the content of the reasoning expressed in it is acceptable from the point of view of the intuitionism of the Dutch mathematician L. E. J. Brouwer.

With the development of constructivist schools in mathematics and logic, intuitionist logic was applied in these fields and therefore was frequently called constructive logic, although certain constructivist principles recognized by many representatives of these schools are absent in intuitionist logic, for example, the principle of constructive selection, introduced by the constructivist school headed by the Soviet mathematician A. A. Markov.

The Great Soviet Encyclopedia, 3rd Edition (1970-1979). © 2010 The Gale Group, Inc. All rights reserved.
References in periodicals archive ?
This philosophical position is fleshed out in relation to a unique logic, intuitionist logic, defined in relation to mental constructions of mathematical proofs.
Similarly but importantly distinct, in intuitionist logic: "AAB" is defined as proven when A is proven and B is proven; "AvB" is defined as proven when A is proven or B is proven; "[logical not]A" is defined as proven when there exists a proof that there is no proof of A; and "A [right arrow] B" is defined as proven when there exists a construction that, provided any proof of A, may be applied to provide a proof of B (Non-classical, 100).
Using Intensional Type Theory, Gilmore covers elementary logic, type theory, recursions, choice and function terms, intuitionist logic, logic and mathematics and logic and computer science.
In his 1963 paper, entitled 'Semantical Analysis of Intuitionistic Logic I', Kripke provides a model-theoretic interpretation of intuitionist logic. Among the results presented in that paper is an illustration of how Cohen's forcing-relation is isomorphic to intuitionistic entailment so long as the forcing conditions are not generic, in which case the relation behaves classically (obeying the Law of the Excluded Middle).
I reject the idea that a move to intuitionist logic can resolve the problems of set theory.
There is also an interesting discussion of the nature of the logical connectives and intuitionist logic.
(6) As a tool for reasoning within the language with which we are concerned, intuitionist logic is reliable, in a way in which classical logic is not.
Yaroslav Shramko argues that there are logics that can presuppose deep temporal ideas even if they do not involve temporal concepts in their syntax, and illustrates this with a discussion of negation in intuitionist logic. Mogens Wegener and Peter Ohrstrom discuss logics that allow truth to emerge and offer a new tense logic, system W, which elaborates a system of A.
(The definitions of the propositional operators are the usual ones for a Heyting lattice so that, as one would expect, We "theorems" of this generalised propositional logic are those of intuitionist logic. Chapter 24 gives the natural proof.)
Perhaps that logic is already with us: intuitionist logic. One of the main reasons for the foundation of intuitionist logic was the rejection of the completed infinite: there could be no totality consisting of all the natural numbers.
To prepare the way, we must first look closely at the rule of existential elimination familiar from classical and intuitionist logics and at rules governing identity.