Intuicionistická logika nebo konstruktivistická logika je systém symbolické logiky původně vyvinutý Arendem Heytingem, aby poskytl formální základ pro Brouwerův program intuicionismu. Systém zachovává spíše ospravedlnění než pravdu, a to napříč transformacemi, které přinášejí odvozené výroky. Z praktického hlediska existuje také silná motivace pro používání intuicionistické logiky, protože má vlastnost existence, což ji činí vhodnou i pro jiné formy matematického konstruktivismu.
Syntaxe formulæ intuicionistické logiky je podobná výrokové logice nebo logice prvního řádu. Zjevný rozdíl je v tom, že mnoho tautologií těchto klasických logik již nemůže být dokázáno v rámci intuicionistické logiky. Příkladem může být nejen zákon vyloučeného středního P ∨ ¬ P, ale také Peirceho zákon ((P → Q) → P) → P, a dokonce i eliminace dvojité negace. V klasické logice jsou P → ¬ P a také ¬ P → P věty. V intuicionistické logice je pouze první věta: Dvojitá negace může být zavedena, ale nemůže být odstraněna.
Pozorování, že mnoho klasicky platných tautologií nejsou věty intuicionistické logiky, vede k myšlence oslabení důkazní teorie klasické logiky.
Pravidlo odvození je modus ponens a axiomy jsou:
Aby se z toho stal systém predikátové logiky prvního řádu, přidává se pravidlo zobecnění spolu s axiomy:
Interdefinovatelnost operátorů
V klasické výrokové logice je možné brát jeden z konjunkcí, disjunkcí nebo implikací jako primitivní a definovat další dva z hlediska toho společně s negací, jako v Łukasiewiczových třech axiomech výrokové logiky. Je dokonce možné definovat všechny čtyři z hlediska jediného dostatečného operátoru, jako je Peirceho šipka nebo Shefferův tah. Podobně v klasické logice prvního řádu může být jeden z kvantifikátorů definován z hlediska druhého a negace.
To jsou v zásadě důsledky zákona bivalence, který činí všechny takové spojky pouze booleovskými funkcemi. Zákon bivalence neplatí v intuicionistické logice, platí pouze zákon neodporu. V důsledku toho se nelze obejít bez spojek a všechny výše uvedené axiomy jsou nezbytné. Většina klasických identit jsou pouze věty inuitionistické logiky v jednom směru, i když některé jsou věty v obou směrech. Jsou následující:
Konjunkce versus disjunkce:
Konjunkce versus implikace:
Rozpojení versus implikace:
Univerzální versus existenciální kvantifikace:
Takže například „a nebo b“ je silnější vyjádření než „když ne a, tak b“, zatímco tyto jsou klasicky zaměnitelné. Na druhou stranu „a ani b“ se nerovná „a ani b“.
Gentzen zjistil, že relativně jednoduchá modifikace jeho systému LK vede k systému, který je zdravý a kompletní s ohledem na intuicionistickou logiku. Tento systém nazval LJ.
Sémantika je poněkud složitější než u klasického, deterministického případu. Modelová teorie může být dána Heytingovou algebrou nebo ekvivalentně Kripkeho sémantikou.
V klasické logice často diskutujeme o pravdivostních hodnotách, které může vzorec nabývat. Hodnoty jsou obvykle vybírány jako členy booleovské algebry. Setkávací a spojovací operace v booleovské algebře jsou ztotožňovány s ∧ a ∨ logickými spojkami, takže hodnota vzorce tvaru A ∧ B je splněním hodnoty A a hodnoty B v booleovské algebře. Pak máme užitečnou větu, že vzorec je platnou větou klasické logiky tehdy a jen tehdy, je-li jeho hodnota 1 pro každé ocenění—tedy pro každé přiřazení hodnot jeho proměnným.
Odpovídající věta platí pro intuicionistickou logiku, ale místo přiřazení hodnoty každému vzorci z Booleovy algebry se používají hodnoty z Heytingovy algebry, jejímž zvláštním případem jsou Booleovy algebry.
Vzorec je v intuicionistické logice platný tehdy a jen tehdy, pokud obdrží hodnotu nejvyššího prvku pro jakékoli ocenění z jakékoli Heytingovy algebry.
Lze prokázat, že k rozpoznání platných vzorců stačí uvažovat o jediné Heytingově algebře, jejíž prvky jsou otevřenými množinami reálné roviny R2. V této algebry,
Operace ∧ a ∨ odpovídají zadanému průniku a sjednocení a hodnota přiřazená vzorci A→B je (AC ∪ B)°,
vnitřek sjednocení hodnoty B a komplementu hodnoty A. Spodní prvek ø je prázdná množina, a horní prvek je celá rovina R2. Negace je jako obvykle definována jako ¬ A = A→ø, takže hodnota ¬ A se redukuje na AC°, vnitřek doplňku hodnoty A. S těmito přiřazeními jsou intuicionisticky platné vzorce přesně ty, kterým je přiřazena hodnota celé roviny.
Například vzorec ¬ (A ∧ ¬ A) je platný, protože bez ohledu na to, jaká množina X je zvolena jako hodnota vzorce A, hodnota ¬ (A ∧ ¬ A) může být ukázána jako celá rovina:
Věta o topologii nám říká, že XC ° je podmnožinou XC, takže průsečík je prázdný, takže:
Takže ocenění tohoto vzorce je pravdivé, a skutečně vzorec je platný.
Ale zákon vyloučeného středu, A∨¬ A, může být prokázán jako neplatný tím, že hodnota A bude {y : y > 0 }. Pak hodnota ¬ A je vnitřek {y : y ≤ 0 }, což je
{y : y < 0 }, a hodnota vzorce je sjednocení
{a : y > 0 }
a
{y : y < 0 }, což je {y : y ≠ 0 }, ne celé letadlo.
Nekonečná Heytingova algebra popsaná výše dává pravdivé ocenění všem intuicionisticky platným vzorcům bez ohledu na to, jaké hodnoty jsou přiřazeny proměnným ve vzorci. Naopak pro každý neplatný vzorec existuje přiřazení hodnot z této algebry proměnným, které přináší nesprávné ocenění vzorce. Lze prokázat, že žádná konečná Heytingova algebra nemá tuto vlastnost.
Na základě své práce o sémantice modální logiky vytvořil Saul Kripke další sémantiku pro intuicionistickou logiku, známou jako Kripkeho sémantika nebo relační sémantika.