Show Summary Details

Page of

PRINTED FROM OXFORD REFERENCE (www.oxfordreference.com). (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 (for details see Privacy Policy and Legal Notice).

date: 28 February 2020

# intuitionistic logic

Source:
A Dictionary of Logic

# 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 , one can read intuitionistic logic as a scheme of reasoning in which assertion of a sentence is the assertion of the provability of . This makes many of the formal distinctions between intuitionistic and classical logic salient. For example, the double negation law:

• 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 leads to absurdity, then one can prove .

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

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

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

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

• Intuitionistic logic is not paraconsistent and one in general has a proof of the antecedent of this formula; if is defined as the proof that entails a contradiction, then as 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 , one has either a proof that entails a contradiction or a proof that can never entail a contradiction. But this is not true if 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 ( ) or Peirce’s law as axiom schema generates classical logic.