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.
