# intuitionistic 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.