Revision #827 → #1324 · back to history
addedIntuitionistic logic4ed9ef65b730
addedBHK interpretation as standard explanation06153d0ef14a
addedSemantics induce logics stronger than Heyting's7f8e7bf17892
addedLaw of excluded middle (classical semantics)8f5122dac73a
addedInhabitation by a proof (Curry–Howard)0ca2aa204c48
addedDisjunction and existence propertiesae2827b5cc0d
addedFour color theorem verification8a6192432928
addedIPL basic connectivesb9721c4c0da4
addedHilbert-style calculus for intuitionistic logic443e36686662
addedModus ponens inference ruleaba66433082c
addedGeneralization rules for predicate logic5b5c09056c7d
addedNegation axioms NOT-1' and NOT-2'483a20ffe34c
addedAlternative negation axioms without false89ba4a372a12
addedEquivalence connective as abbreviation05c10e56f65e
addedGentzen's sequent calculus LJbdd6b926adcf
addedLJ' multiple-conclusion variantb11fb0a99b52
addedIntuitionistic theorems are classical theorems2f12a232ab21
addedDouble negation of excluded middle in minimal logic055bce54f6f9
addedStable proposition5b2162a65374
addedStability of negated propositions6832eb00422f
addedGödel–Gentzen double-negation translationf7c9b38d52db
addedConjunction/disjunction relate to implication via negation64d9886e885b
addedNon-reversibility of negation-distribution implications580e548edc04
addedExistential implies negated universal542ecb4ec103
addedStronger quantifier negation theorem85cf1671e98d
addedDisjointness characterizations equivalenced3418e401ff2
addedFinite De Morgan-type variants for two propositionsb30b46b03ad8
addedConstant domain principle invalidityf56329ced37d
addedImport-export equivalenceb9ce542c4dfb
addedConjunction of unrejectable propositions unrejectabled204059c9564
addedExcluded middle equivalent to consequentia mirabilisce62e02f7e2a
addedStrengthened disjunctive syllogismb3d7dab881c2
addedEquivalence as conjunction of implicationse72218c8f577
addedKuznetsov functionally complete connectives436e908e6954
addedConstable's Tarski-like completenessf91226bff8de
addedGlivenko: no third truth value3ddfeea0343a
addedHeyting algebra validity characterization9a2bc657e6fc
addedOpen sets of the real line sufficec609d98adbc1
addedValidity of ¬(A ∧ ¬A)46f88686871d
addedInvalidity of excluded middle via positive reals5ed925da8630
addedNo finite Heyting algebra suffices24e152977d5b
addedKripke semantics for intuitionistic logic94474a8a8ae7
addedConstable's weaker Tarski-like completenessb91e4b6b23d2
addedAdmissible rulec2e00c2c01ef
addedDisjunction property of IPC5739c726b5f7
addedBrazilian/dual-intuitionistic logic1f0a456a0e27
addedMinimal logic3abfa6d39707
addedIntermediate logics from finite Heyting algebrasea1b0f1e5ef4
addedGödel–Dummett logic6473599ae0d6
addedClassical logic axiom additions6f7691329007
addedGödel: intuitionistic logic not finite-valued414ea6b1961b
addedGödel–McKinsey–Tarski translation into S4790c12b11189
addedCurry–Howard with simply typed lambda calculus3bbdafe1ac73