Linked from

The 41 pages that link to Intuitionistic logic, each with the reason it gives.

• Propositional logicCompared with: Its propositional calculus rejects some classical principles, including unrestricted excluded middle.

• Classical logicCompared with: It rejects unrestricted excluded middle, distinguishing it from classical logic.

• Natural deductionRelated: Natural deduction gives intuitionistic logic a direct interpretation of connectives through their proof rules.

• NegationCompared with: Its negation does not generally make double negation equivalent to the original proposition.

• Sequent calculusRelated: Its sequent calculus restricts conclusions to capture constructive reasoning.

• Paraconsistent logicCompared with: It departs from classical logic for a different reason and is not generally paraconsistent.

• Mathematical logicCompared with: It rejects unrestricted use of classical principles that intuitionists regard as nonconstructive.

• Modus ponensRelated: Modus ponens remains valid even though some classical inference principles do not.

• Logical connectiveCompared with: Its connective meanings are tied to constructive proof rather than classical truth tables.

• Proof by contradictionCompared with: Its standards limit classical contradiction proofs, especially for existence claims.

• Curry–Howard correspondenceRelated: The standard proposition–type interpretation captures intuitionistic rather than unrestricted classical reasoning.

• Modal logicCompared with: It alters the underlying propositional logic, unlike standard modal extensions of classical logic.

• Truth valueCompared with: Its treatment of propositions differs from classical truth-value assignments.

• Formal systemCompared with: It changes which inferences and theorems are accepted compared with classical systems.

• IntuitionismBroader topic: It formalizes the logical consequences of intuitionistic standards of proof.

• ContradictionCompared with: It revises classical inference principles while retaining a strong role for consistency.

• Constructive proofRelated: Its interpretation of existence connects proving a claim with constructing evidence for it.

• Formal logicCompared with: It rejects an inference principle accepted in classical logic.

• Law of Excluded MiddleCompared with: It rejects the law as a universal principle when no proof of either alternative is available.

• Constructive mathematicsRelated: Its proof rules formalize a major logical foundation for constructive mathematics.

• DisjunctionCompared with: Its disjunction property requires a proof of a disjunction to establish one side.

• L. E. J. BrouwerRelated: It formalizes the proof principles associated with Brouwer’s intuitionism.

• LogicCompared with: It does not accept the law of excluded middle for every proposition.

• Relevant logicCompared with: It rejects classical principles for constructive reasons, not primarily to enforce premise-conclusion relevance.

• Reductio ad absurdumCompared with: Its treatment of negation limits what some classical reductio arguments can establish.

• Heyting algebraRelated: Heyting algebras interpret its connectives while preserving intuitionistic validity.

• Principle of explosionCompared with: Unlike classical logic, it does not validate explosion in its usual formulation.

• History of logicCompared with: Its standards of proof challenge assumptions built into classical logic.

• Symbolic logicCompared with: It shows that classical symbolic rules are not the only viable formal choices.

• ConstructivismRelated: It supplies a formal logic commonly used to express constructivist standards.

• Disjunction eliminationRelated: Disjunction elimination remains valid constructively, with evidence handled by cases.

• Disjunction introductionCompared with: It permits disjunction introduction, while interpreting disjunction through constructive proof.

• Law of noncontradictionCompared with: It rejects excluded middle in general while retaining noncontradiction.

• Cut-elimination theoremRelated: Gentzen proved cut elimination for intuitionistic as well as classical sequent calculus.

• Peirce's lawCompared with: It cannot derive Peirce's law without adding classical principles.

• Principle of bivalenceCompared with: Its rejection of unrestricted excluded middle separates it from classical reasoning, though it need not posit a third truth value.

• De Morgan's lawsCompared with: It validates only one direction of the familiar De Morgan equivalence in general.

• Deduction theoremRelated: The theorem holds in standard intuitionistic systems, but does not grant classical reasoning.

• Cartesian closed categoryRelated: The internal logic of a cartesian closed category interprets implication intuitionistically.

• Consequentia mirabilisCompared with: The classical derivation does not automatically establish the principle intuitionistically.

• Philosophical logicCompared with: It challenges a classical principle whose validity has philosophical consequences for truth and proof.