Show Summary Details

Page of

PRINTED FROM OXFORD REFERENCE ( (c) Copyright Oxford University Press, 2013. All Rights Reserved. Under the terms of the licence agreement, an individual user may print out a PDF of a single entry from a reference work in OR for personal use.

date: 19 November 2017

intuitionistic logic

A Dictionary of Logic

Thomas Macaulay Ferguson,

Graham Priest

intuitionistic logic 

Describes systems of propositional and first-order logic developed by Arend Heyting (1898–1980) as a formal axiomatization of the reasoning central to L. E. J. Brouwer’s (1881–1966) programme of intuitionism.

Given the Gödel-McKinsey-Tarski embedding of intuitionistic logic into intuitionistic logic, one can read intuitionistic logic as a scheme of reasoning in which assertion of a sentence intuitionistic logic is the assertion of the provability of intuitionistic logic. This makes many of the formal distinctions between intuitionistic and classical logic salient. For example, the double negation law:

  • intuitionistic logic

is rejected in intuitionistic logic. But to accept this scheme as a theorem is equivalent to the statement:

  • If one can prove that the rejection of intuitionistic logic leads to absurdity, then one can prove intuitionistic logic.

To assert, for example, that intuitionistic logic holds, i.e., that intuitionistic logic, would entail that one could disprove both intuitionistic logic and intuitionistic logic. But this is absurd from an intuitionistic perspective, hence intuitionistic logic leads to absurdity, or intuitionistic logic. But the scheme:

  • intuitionistic logic

is also rejected, as it would entail that for any formula intuitionistic logic, one has the means to either prove or disprove intuitionistic logic.

This interpretation explains the failure of instances of one of De Morgan’s laws, i.e.:

  • intuitionistic logic

Should this scheme count as an axiom or theorem, then as an instance, one could infer in general that:

  • intuitionistic logic

Intuitionistic logic is not paraconsistent and one in general has a proof of the antecedent intuitionistic logic of this formula; if intuitionistic logic is defined as the proof that intuitionistic logic entails a contradiction, then as intuitionistic logic trivially follows. Accepting the consequent of this formula—known as weak excluded middle—as an axiom scheme would be to state that for any formula intuitionistic logic, one has either a proof that intuitionistic logic entails a contradiction or a proof that intuitionistic logic can never entail a contradiction. But this is not true if intuitionistic logic is, e.g., the Riemann Hypothesis.

Intuitionistic logic is a proper subsystem of classical logic and the addition of either the law of excluded middle (intuitionistic logic) or Peirce’s law intuitionistic logic as axiom schema generates classical logic.

Was This Useful?