intuitionistic logic

aesthetics  →
being  →
complexity  →
database  →
enterprise  →
ethics  →
fiction  →
history  →
internet  →
knowledge  →
language  →
licensing  →
linux  →
logic  →
method  →
news  →
perception  →
philosophy  →
policy  →
purpose  →
religion  →
science  →
sociology  →
software  →
truth  →
unix  →
wiki  →
essay  →
feed  →
help  →
system  →
wiki  →
critical  →
discussion  →
forked  →
imported  →
original  →
intuitionistic logic
[ temporary import ]
please note:
- the content below is remote from Wikipedia
- it has been imported raw for GetWiki
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems of intuitionistic logic do not include the law of the excluded middle and double negation elimination, which are fundamental inference rules in classical logic.Formalized intuitionistic logic was originally developed by Arend Heyting to provide a formal basis for Brouwer's programme of intuitionism. From a proof-theoretic perspective, Heyting’s calculus is a restriction of classical logic in which the law of excluded middle and double negation elimination have been removed. Excluded middle and double negation elimination can still be proved for some propositions on a case by case basis, however, but do not hold universally as they do with classical logic.Several systems of semantics for intuitionistic logic have been studied. One of these semantics mirrors classical Boolean-valued semantics but uses Heyting algebras in place of Boolean algebras. Another semantics uses Kripke models. These, however, are technical means for studying Heyting’s deductive system rather than formalizations of Brouwer’s original informal semantic intuitions. Semantical systems claiming to capture such intuitions, due to offering meaningful concepts of “constructive truth” (rather than merely validity or provability), are Gödel’s dialectica interpretation, Kleene’s realizability, Medvedev’s logic of finite problems,Shehtman, V., "Modal Counterparts of Medvedev Logic of Finite Problems Are Not Finitely Axiomatizable," in Studia Logica: An International Journal for Symbolic Logic, vol. 49, no. 3 (1990), pp. 365-385. or Japaridze’s computability logic. Yet such semantics persistently induce logics properly stronger than Heyting’s logic. Some authors have argued that this might be an indication of inadequacy of Heyting’s calculus itself, deeming the latter incomplete as a constructive logic.G. Japaridze. "In the beginning was game semantics". In: Games: Unifying Logic, Language and Philosophy. O. Majer, A.-V. Pietarinen and T. Tulenheimo, eds. Springer 2009, pp.249-350. Preprint

Mathematical constructivism

In the semantics of classical logic, propositional formulae are assigned truth values from the two-element set {top, bot} ("true" and "false" respectively), regardless of whether we have direct evidence for either case. This is referred to as the 'law of excluded middle', because it excludes the possibility of any truth value besides 'true' or 'false'. In contrast, propositional formulae in intuitionistic logic are not assigned a definite truth value and are only considered "true" when we have direct evidence, hence proof. (We can also say, instead of the propositional formula being "true" due to direct evidence, that it is inhabited by a proof in the Curry–Howard sense.) Operations in intuitionistic logic therefore preserve justification, with respect to evidence and provability, rather than truth-valuation.Intuitionistic logic is a commonly-used tool in developing approaches to constructivism in mathematics. The use of constructivist logics in general has been a controversial topic among mathematicians and philosophers (see, for example, the Brouwer–Hilbert controversy). A common objection to their use is the above-cited lack of two central rules of classical logic, the law of excluded middle and double negation elimination. These are considered to be so important to the practice of mathematics that David Hilbert wrote of them: "Taking the principle of excluded middle from the mathematician would be the same, say, as proscribing the telescope to the astronomer or to the boxer the use of his fists. To prohibit existence statements and the principle of excluded middle is tantamount to relinquishing the science of mathematics altogether." van Heijenoort: Hilbert (1927), p.476Despite the serious challenges presented by the inability to utilize the valuable rules of excluded middle and double negation elimination, intuitionistic logic has practical use. One reason for this is that its restrictions produce proofs that have the existence property, making it also suitable for other forms of mathematical constructivism. Informally, this means that if there is a constructive proof that an object exists, that constructive proof may be used as an algorithm for generating an example of that object, a principle known as the Curry–Howard correspondence between proofs and algorithms. One reason that this particular aspect of intuitionistic logic is so valuable is that it enables practitioners to utilize a wide range of computerized tools, known as proof assistants. These tools assist their users in the verification (and generation) of large-scale proofs, whose size usually precludes the usual human-based checking that goes into publishing and reviewing a mathematical proof. As such, the use of proof assistants (such as Agda or Coq) is enabling modern mathematicians and logicians to develop and prove extremely complex systems, beyond those which are feasible to create and check solely by hand. One example of a proof which was impossible to formally verify without algorithm is the famous proof of the four color theorem. This theorem stumped mathematicians for more than a hundred years, until a proof was developed which ruled out large classes of possible counterexamples, yet still left open enough possibilities that a computer program was needed to finish the proof. That proof was controversial for some time, but, later, it was verified using Coq.


File:Rieger-Nishimura.svg|thumb|right|280px|The Rieger–Nishimura lattice. Its nodes are the propositional formulas in one variable up to intuitionistic logical equivalencelogical equivalenceThe syntax of formulas of intuitionistic logic is similar to propositional logic or first-order logic. However, intuitionistic connectives are not definable in terms of each other in the same way as in classical logic, hence their choice matters. In intuitionistic propositional logic (IPL) it is customary to use →, ∧, ∨, ⊥ as the basic connectives, treating ¬A as an abbreviation for {{nowrap|(A → ⊥)}}. In intuitionistic first-order logic both quantifiers ∃, ∀ are needed.

Weaker than Classical Logic

Intuitionistic logic can be understood as a weakening of classical logic, meaning that it is more conservative in what it allows a reasoner to infer, while not permitting any new inferences that could not be made under classical logic. Each theorem of intuitionistic logic is a theorem in classical logic, but not conversely. Many tautologies in classical logic are not theorems in intuitionistic logic - in particular, as said above one of its chief points is to not affirm the law of the excluded middle so as to vitiate the use of non-constructive proof by contradiction which can be used to furnish existence claims without providing explicit examples of the objects that it proves exist. We say "not affirm" because while it is not necessarily true that the law is upheld in any context, no counterexample can be given: such a counterexample would be an inference (inferring the negation of the law for a certain proposition) disallowed under classical logic and thus is not allowed in a strict weakening like intuitionistic logic. Indeed, the double negation of the law is retained as a tautology of the system: that is, it is a theorem that neg [neg (P vee neg P)] regardless of the proposition P.

Sequent calculus

Gentzen discovered that a simple restriction of his system LK (his sequent calculus for classical logic) results in a system which is sound and complete with respect to intuitionistic logic. He called this system LJ. In LK any number of formulas is allowed to appear on the conclusion side of a sequent; in contrast LJ allows at most one formula in this position.Other derivatives of LK are limited to intuitionistic derivations but still allow multiple conclusions in a sequent. LJ'Proof Theory by G. Takeuti, {{ISBN|0-444-10492-5}} is one example.

Hilbert-style calculus

Intuitionistic logic can be defined using the following Hilbert-style calculus. This is similar to a way of axiomatizing classical propositional logic.In propositional logic, the inference rule is modus ponens
  • MP: from phi and phi to psi infer psi
and the axioms are
  • THEN-1: phi to (chi to phi )
  • THEN-2: (phi to (chi to psi )) to ((phi to chi ) to (phi to psi ))
  • AND-1: phi land chi to phi
  • AND-2: phi land chi to chi
  • AND-3: phi to (chi to (phi land chi ))
  • OR-1: phi to phi lor chi
  • OR-2: chi to phi lor chi
  • OR-3: (phi to psi ) to ((chi to psi ) to (phi lor chi to psi ))
  • FALSE: bot to phi
To make this a system of first-order predicate logic, the generalization rules
  • forall -GEN: from psi to phi infer psi to (forall x phi ), if x is not free in psi
  • exists -GEN: from phi to psi infer (exists x phi ) to psi , if x is not free in psi
are added, along with the axioms
  • PRED-1: (forall x phi (x)) to phi (t), if the term t is free for substitution for the variable x in phi (i.e., if no occurrence of any variable in t becomes bound in phi (t))
  • PRED-2: phi (t) to (exists x phi (x)), with the same restriction as for PRED-1

Optional connectives


If one wishes to include a connective lnot for negation rather than consider it an abbreviation for phi to bot , it is enough to add:
  • NOT-1': (phi to bot ) to lnot phi
  • NOT-2': lnot phi to (phi to bot )
There are a number of alternatives available if one wishes to omit the connective bot (false). For example, one may replace the three axioms FALSE, NOT-1', and NOT-2' with the two axioms
  • NOT-1: (phi to chi ) to ((phi to lnot chi ) to lnot phi )
  • NOT-2: phi to (lnot phi to chi )
as at Propositional calculus#Axioms. Alternatives to NOT-1 are (phi to lnot chi ) to (chi to lnot phi ) or (phi to lnot phi ) to lnot phi .


The connective leftrightarrow for equivalence may be treated as an abbreviation, with phi leftrightarrow chi standing for (phi to chi ) land (chi to phi ). Alternatively, one may add the axioms
  • IFF-1: (phi leftrightarrow chi ) to (phi to chi )
  • IFF-2: (phi leftrightarrow chi ) to (chi to phi )
  • IFF-3: (phi to chi ) to ((chi to phi ) to (phi leftrightarrow chi ))
IFF-1 and IFF-2 can, if desired, be combined into a single axiom (phi leftrightarrow chi ) to ((phi to chi ) land (chi to phi )) using conjunction.

Relation to classical logic

The system of classical logic is obtained by adding any one of the following axioms:
  • phi lor lnot phi (Law of the excluded middle. May also be formulated as (phi to chi ) to ((lnot phi to chi ) to chi ).)
  • lnot lnot phi to phi (Double negation elimination)
  • ((phi to chi ) to phi ) to phi (Peirce's law)
  • (lnot phi to lnot chi ) to (chi to phi ) (Law of contraposition)
In general, one may take as the extra axiom any classical tautology that is not valid in the two-element Kripke frame circ{longrightarrow}circ (in other words, that is not included in Smetanich's logic).Another relationship is given by the Gödel–Gentzen negative translation, which provides an embedding of classical first-order logic into intuitionistic logic: a first-order formula is provable in classical logic if and only if its Gödel–Gentzen translation is provable intuitionistically. Therefore, intuitionistic logic can instead be seen as a means of extending classical logic with constructive semantics.In 1932, Kurt Gödel defined a system of logics intermediate between classical and intuitionistic logic; Gödel logics are concomitantly known as intermediate logics.

Non-interdefinability of operators

In classical propositional logic, it is possible to take one of conjunction, disjunction, or implication as primitive, and define the other two in terms of it together with negation, such as in Łukasiewicz's three axioms of propositional logic. It is even possible to define all four in terms of a sole sufficient operator such as the Peirce arrow (NOR) or Sheffer stroke (NAND). Similarly, in classical first-order logic, one of the quantifiers can be defined in terms of the other and negation.These are fundamentally consequences of the law of bivalence, which makes all such connectives merely Boolean functions. The law of bivalence does not hold in intuitionistic logic, only the law of non-contradiction. As a result, none of the basic connectives can be dispensed with, and the above axioms are all necessary. Most of the classical identities are only theorems of intuitionistic logic in one direction, although some are theorems in both directions. They are as follows:Conjunction versus disjunction:
  • (phi wedge psi) to neg (neg phi vee neg psi)
  • (phi vee psi) to neg (neg phi wedge neg psi)
  • (neg phi vee neg psi) to neg (phi wedge psi)
  • (neg phi wedge neg psi) leftrightarrow neg (phi vee psi)
Conjunction versus implication:
  • (phi wedge psi) to neg (phi to neg psi)
  • (phi to psi) to neg (phi wedge neg psi)
  • (phi wedge neg psi) to neg (phi to psi)
  • (phi to neg psi) leftrightarrow neg (phi wedge psi)
Disjunction versus implication:
  • (phi vee psi) to (neg phi to psi)
  • (neg phi vee psi) to (phi to psi)
Universal versus existential quantification:
  • (forall x phi(x)) to neg (exists x neg phi(x))
  • (exists x phi(x)) to neg (forall x neg phi(x))
  • (exists x neg phi(x)) to neg (forall x phi(x))
  • (forall x neg phi(x)) leftrightarrow neg (exists x phi(x))
So, for example, "a or b" is a stronger propositional formula than "if not a, then b", whereas these are classically interchangeable. On the other hand, "not (a or b)" is equivalent to "not a, and also not b".If we include equivalence in the list of connectives, some of the connectives become definable from others:
  • (phileftrightarrow psi) leftrightarrow ((phi to psi)land(psitophi))
  • (phitopsi) leftrightarrow ((philorpsi) leftrightarrow psi)
  • (phitopsi) leftrightarrow ((philandpsi) leftrightarrow phi)
  • (philandpsi) leftrightarrow ((phitopsi)leftrightarrowphi)
  • (philandpsi) leftrightarrow (((philorpsi)leftrightarrowpsi)leftrightarrowphi)
In particular, {∨, ↔, ⊥} and {∨, ↔, ¬} are complete bases of intuitionistic connectives.As shown by Alexander Kuznetsov, either of the following connectives – the first one ternary, the second one quinary – is by itself functionally complete: either one can serve the role of a sole sufficient operator for intuitionistic propositional logic, thus forming an analog of the Sheffer stroke from classical propositional logic:Alexander Chagrov, Michael Zakharyaschev, Modal Logic, vol. 35 of Oxford Logic Guides, Oxford University Press, 1997, pp. 58–59. {{ISBN|0-19-853779-4}}.
  • ((plor q)landneg r)lor(neg pland(qleftrightarrow r)),
  • pto(qlandneg rland(slor t)).


The semantics are rather more complicated than for the classical case. A model theory can be given by Heyting algebras or, equivalently, by Kripke semantics. Recently, a Tarski-like model theory was proved complete by Bob Constable, but with a different notion of completeness than classically.Unproved statements in intuitionistic logic are not given an intermediate truth value (as is sometimes mistakenly asserted). One can prove that such statements have no third truth value, a result dating back to Glivenko in 1928.BOOK,weblink The Stanford Encyclopedia of Philosophy, Mark, van Atten, Edward N., Zalta, 27 December 2018, Metaphysics Research Lab, Stanford University, Stanford Encyclopedia of Philosophy, Instead they remain of unknown truth value, until they are either proved or disproved. Statements are disproved by deducing a contradiction from them.A consequence of this point of view is that intuitionistic logic has no interpretation as a two-valued logic, nor even as a finite-valued logic, in the familiar sense. Although intuitionistic logic retains the trivial propositions {top, bot} from classical logic, each proof of a propositional formula is considered a valid propositional value, thus by Heyting's notion of propositions-as-sets, propositional formulae are (potentially non-finite) sets of their proofs.

Heyting algebra semantics

In classical logic, we often discuss the truth values that a formula can take. The values are usually chosen as the members of a Boolean algebra. The meet and join operations in the Boolean algebra are identified with the ∧ and ∨ logical connectives, so that the value of a formula of the form A ∧ B is the meet of the value of A and the value of B in the Boolean algebra. Then we have the useful theorem that a formula is a valid proposition of classical logic if and only if its value is 1 for every valuation—that is, for any assignment of values to its variables.A corresponding theorem is true for intuitionistic logic, but instead of assigning each formula a value from a Boolean algebra, one uses values from an Heyting algebra, of which Boolean algebras are a special case. A formula is valid in intuitionistic logic if and only if it receives the value of the top element for any valuation on any Heyting algebra.It can be shown that to recognize valid formulas, it is sufficient to consider a single Heyting algebra whose elements are the open subsets of the real line R.BOOK, Lectures on the Curry-Howard Isomorphism, Sørensen, Morten Heine B, Paweł Urzyczyn, 2006, Elsevier, 978-0-444-52077-7, Studies in Logic and the Foundations of Mathematics, 42, In this algebra we have:
text{Value}[bot] &=emptyset text{Value}[top] &= mathbf{R} text{Value}[A land B] &= text{Value}[A] cap text{Value}[B] text{Value}[A lor B] &= text{Value}[A] cup text{Value}[B] text{Value}[A to B] &= text{int} left ( text{Value}[A]^{mathrm{C}} cup text{Value}[B] right )end{align}where int(X) is the interior of X and XC its complement.The last identity concerning A → B allows us to calculate the value of ¬A:
text{Value}[neg A] &= text{Value}[A to bot] &= text{int} left ( text{Value}[A]^{mathrm{C}} cup text{Value}[bot] right ) &= text{int} left ( text{Value}[A]^{mathrm{C}} cup emptyset right ) &= text{int} left ( text{Value}[A]^{mathrm{C}} right )end{align}With these assignments, intuitionistically valid formulas are precisely those that are assigned the value of the entire line. For example, the formula ¬(A ∧ ¬A) is valid, because no matter what set X is chosen as the value of the formula A, the value of ¬(A ∧ ¬A) can be shown to be the entire line:
text{Value}[neg(A land neg A)] &= text{int} left ( text{Value} [A land neg A]^{mathrm{C}} right ) && text{Value}[neg B] = text{int}left ( text{Value}[B]^{mathrm{C}} right) &= text{int} left ( left (text{Value}[A] cap text{Value}[neg A] right )^{mathrm{C}} right )&= text{int} left ( left (text{Value}[A] cap text{int} left (text{Value}[A]^{mathrm{C}} right ) right )^{mathrm{C}} right ) &= text{int} left ( left (X cap text{int} left (X^{mathrm{C}} right ) right )^{mathrm{C}} right ) &= text{int} left (emptyset^{mathrm{C}} right ) && text{int} left (X^{mathrm{C}} right ) subset X^{mathrm{C}} &= text{int} (mathbf{R}) &= mathbf{R}end{align}So the valuation of this formula is true, and indeed the formula is valid. But the law of the excluded middle, A ∨ ¬A, can be shown to be invalid by using a specific value of the set of positive real numbers for A:
text{Value}[A lor neg A] &= text{Value}[A] cup text{Value}[neg A] &= text{Value}[A] cup text{int} left ( text{Value}[A]^{mathrm{C}} right) && text{Value}[neg B] = text{int}left ( text{Value}[B]^{mathrm{C}} right) &= { x > 0} cup text{int} left ( {x > 0}^{mathrm{C}} right ) &= { x > 0} cup text{int} left ( {x leqslant 0 } right) &= { x > 0} cup {x < 0 } &={ x neq 0 } &neq mathbf{R}end{align}The interpretation of any intuitionistically valid formula in the infinite Heyting algebra described above results in the top element, representing true, as the valuation of the formula, regardless of what values from the algebra are assigned to the variables of the formula. Conversely, for every invalid formula, there is an assignment of values to the variables that yields a valuation that differs from the top element.Alfred Tarski, Der Aussagenkalkül und die Topologie, Fundamenta Mathematicae 31 (1938), 103–134. weblinkBOOK, The Mathematics of Metamathematics, Rasiowa, Helena, Roman Sikorski, 1963, Państwowe Wydawn. Naukowe, Warsaw, Monografie matematyczne, 385–386, No finite Heyting algebra has both these properties.

Kripke semantics

Building upon his work on semantics of modal logic, Saul Kripke created another semantics for intuitionistic logic, known as Kripke semantics or relational semantics.Intuitionistic Logic. Written by Joan Moschovakis. Published in Stanford Encyclopedia of Philosophy.

Tarski-like semantics

It was discovered that Tarski-like semantics for intuitionistic logic were not possible to prove complete. However, Robert Constable has shown that a weaker notion of completeness still holds for intuitionistic logic under a Tarski-like model. In this notion of completeness we are concerned not with all of the statements that are true of every model, but with the statements that are true in the same way in every model. That is, a single proof that the model judges a formula to be true must be valid for every model. In this case, there is not only a proof of completeness, but one that is valid according to intuitionistic logic.JOURNAL, Constable, R., Bickford, M., 2014, Intuitionistic completeness of first-order logic, Annals of Pure and Applied Logic, 165, 164–198, 10.1016/j.apal.2013.07.009, 1110.1614,

Relation to other logics

Intuitionistic logic is related by duality to a paraconsistent logic known as Brazilian, anti-intuitionistic or dual-intuitionistic logic.JOURNAL, Aoyama, Hiroshi, LK, LJ, Dual Intuitionistic Logic, and Quantum Logic, Notre Dame Journal of Formal Logic, 2004, 45, 4, 193–213, 10.1305/ndjfl/1099238445, The subsystem of intuitionistic logic with the FALSE axiom removed is known as minimal logic.

Relation to many-valued logic

Kurt Gödel's work involving many-valued logic showed in 1932 that intuitionistic logic is not a finite-valued logic.WEB, Burgess, John, Intuitions of Three Kinds in Gödel's Views on the Continuum,weblink (See the section titled Heyting algebra semantics above for an infinite-valued logic interpretation of intuitionistic logic.)

Relation to intermediate logics

Any finite Heyting algebra which is not equivalent to a Boolean algebra defines (semantically) an intermediate logic. On the other hand, validity of formulae in pure intuitionistic logic is not tied to any individual Heyting algebra but relates to any and all Heyting algebras at the same time.

Relation to modal logic

Any formula of the intuitionistic propositional logic may be translated into the normal modal logic S4 as follows:
bot^* &= bot A^* &= Box A && text{if } A text{ is prime (a positive literal)} (A wedge B)^*&= A^* wedge B^* (A vee B)^* &= A^* vee B^* (A to B)^*&= Box left (A^* to B^* right ) (neg A)^*&= Box(neg (A^*)) && neg A := A to botend{align}and it has been demonstratedLévy, Michel (2011). Logique modale propositionnelle S4 et logique intuitioniste propositionnelle, pp. 4–5. that the translated formula is valid in the propositional modal logic S4 if and only if the original formula is valid in IPC. The above set of formulae are called the Gödel–McKinsey–Tarski translation.There is also an intuitionistic version of modal logic S4 called Constructive Modal Logic CS4.Natasha Alechina, Michael Mendler, Valeria de Paiva, and Eike Ritter. Categorical and Kripke Semantics for Constructive S4 Modal Logic

Lambda calculus

There is an extended Curry–Howard isomorphism between IPC and simply-typed lambda calculus.

See also




  • van Dalen, Dirk, 2001, "Intuitionistic Logic", in Goble, Lou, ed., The Blackwell Guide to Philosophical Logic. Blackwell.
  • Morten H. Sørensen, PaweÅ‚ Urzyczyn, 2006, Lectures on the Curry-Howard Isomorphism (chapter 2: "Intuitionistic Logic"). Studies in Logic and the Foundations of Mathematics vol. 149, Elsevier.
  • W. A. Carnielli (with A. B.M. Brunner)."Anti-intuitionism and paraconsistency". Journal of Applied Logic Volume 3, Issue 1, Mar 2005, pp. 161–184.

External links

{{Non-classical logic}}{{Authority control}}

- content above as imported from Wikipedia
- "intuitionistic logic" does not exist on GetWiki (yet)
- time: 1:12am EDT - Wed, Sep 18 2019
[ this remote article is provided by Wikipedia ]
LATEST EDITS [ see all ]
Eastern Philosophy
History of Philosophy
M.R.M. Parrott