Logique Intuitionniste

Un système logique constructif qui interprète les connecteurs logiques en termes de provabilité ou de constructions, rejette la loi du tiers exclu non restreinte, et se formalise couramment par la déduction naturelle, les calculs de séquents, les algèbres de Heyting ou la sémantique de Kripke pour la vérité constructive.