Lógica intuicionista
# Lógica intuicionista

La lógica intuicionista, o lógica constructivista, es el sistema lógico originalmente desarrollado por Arend Heyting para proveer una base formal para el proyecto intuicionista de Brouwer. El sistema enfatiza las pruebas, en vez de la verdad, a lo largo de las transformaciones de las proposiciones.
La lógica intuicionista rechaza el principio del tercero excluido, pero conserva el principio de explosión. Esto se debe a una observación de Brouwer de que si enfatizamos las pruebas en vez de la verdad, entonces en los conjuntos infinitos el principio del tercero excluido falla cuando se aplica a una proposición para la que no existe demostración, ni de su verdad ni de su falsedad. En los conjuntos finitos siempre es posible verificar si una proposición es cierta o falsa; en los infinitos, no.

# Lógica intuicionista
## Constructivismo matemático

En la semántica de la lógica clásica, se asignan valores de verdad a fórmulas proposicionales del conjunto de dos elementos $\{\top ,\bot \}$ ("verdadero y "falso" respectivamente) independientemente si se tiene evidencia directa para cada caso. Esto se refiere a el Principio del tercero excluido, que excluye la posibilidad para cualquier valor verdadero aparte de "verdadero" o "falso", evitando así un enunciado contradictorio. En contraste, las fórmulas proposicionales en lógica intuicionista no tienen un valor definitivo de verdad asignado y solo son únicamente consideradas como "verdaderas" cuando se tiene evidencia directa.

# Lógica intuicionista
## Polémica

La lógica intuicionista es una de las maneras de abordar el Constructivismo en matemáticas. El uso de Lógicas constructivistas en general han sido vistas como un tema controvertido entre matemáticos y filósofos.
La objeción más reconocida que tiene es que excluye el principio del tercero excluido y la eliminación de doble negación, las cuales han sido reglas centrales para el Cálculo proposicional, y que David Hilbert escribió de ellas: "Quitar el Principio del tercero excluido a un matemático, sería lo mismo que quitar un telescopio a un astrónomo o los guantes a un boxeador. Prohibir la existencia a enunciados y el principio de exclusión es equivalente a renunciar a toda la ciencia de las matemáticas."