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.