Un retículo acotado (con 0 y 1) provisto de una operación binaria de implicación → que satisface la adjunción a ∧ b ≤ c si y solo si a ≤ (b → c); proporciona una semántica algebraica para la lógica proposicional intuicionista donde no necesariamente se cumple el principio del tercero excluido.

Principio

La idea organizadora es la residuación: la implicación es el adjunto derecho del encuentro (∧) con antecedente fijado, codificando una condicional constructiva que puede prescindir de la negación clásica y del tercero excluido.

Demostración

El retículo de abiertos de un espacio topológico, ordenado por inclusión, con implicación U → V como el mayor abierto W tal que W ∧ U ≤ V (o usando el interior de ((X ar{U}) ∪ V)), forma una álgebra de Heyting y modela verdades intuicionistas en topología.

Aplicación incorrecta

Confundir la implicación de Heyting con la implicación material (¬a ∨ b) o suponer que cada elemento tiene un complemento booleano conduce a inferencias clásicas incorrectas, como el tercero excluido o la eliminación de la doble negación.

Consecuencia

Si la estructura es una álgebra de Heyting, admite principios de razonamiento constructivo, internaliza la implicación algebraicamente y puede actuar como objeto de valores de verdad en contextos tipo topos; las transformaciones de pruebas reflejan la residuación algebraica.

Inversión

Especializar una álgebra de Heyting imponiendo que cada elemento tenga un complemento con a ∨ a' = 1 produce una álgebra booleana y restaura las leyes clásicas como el tercero excluido y la eliminación de la doble negación.

Límite

Requiere un retículo acotado con una implicación que satisfaga la condición de residuación; excluye retículos generales sin este adjunto o estructuras que imponen la negación clásica. Las álgebras de Heyting no necesitan ser complementadas.

Tensión semántica

Tensión con la álgebra booleana (lógica clásica) y con retículos sin implicación; la tensión reside entre la implicación constructiva (residuación) y la implicación material clásica, y entre la semántica interna constructiva y valoraciones clásicas externas.

Síntesis

Una álgebra de Heyting es el marco algebraico de la lógica proposicional intuicionista: un retículo acotado con una implicación residuada que codifica la condicional constructiva sin asumir complementos clásicos.