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.