Lógica intuicionista y constructivismo

La lógica intuicionista rechaza la ley del tercero excluido, sosteniendo que una afirmación matemática es verdadera solo si podemos construir una prueba de ella.

Definition

La lógica intuicionista es la lógica de la prueba constructiva, en la que una disyunción requiere una prueba de uno de los disyuntos y una afirmación existencial requiere la construcción de un testigo, de modo que el tercero excluido y la prueba por contradicción para las afirmaciones de existencia no son generalmente válidos.

Scope

Este tema abarca la lógica intuicionista y la filosofía constructivista de las matemáticas que la motiva. Trata la visión de Brouwer de las matemáticas como construcción mental, la formalización de Heyting y la interpretación de los conectivos basada en la prueba (BHK), el fallo del tercero excluido y la eliminación de la doble negación, la semántica de Kripke y topológica para la lógica intuicionista, y el argumento de Dummett basado en la teoría del significado de que el antirrealismo sobre la verdad apoya la lógica intuicionista en general.

Core questions

• ¿Por qué debería fallar la ley del tercero excluido y para qué afirmaciones?
• ¿Cuál es la interpretación constructiva de los conectivos lógicos?
• ¿El argumento a favor del intuicionismo es específicamente matemático, o se generaliza a través de la teoría del significado?
• ¿Cómo iluminan los modelos de Kripke y topológicos la validez intuicionista?

Key concepts

• ley del tercero excluido
• prueba constructiva
• interpretación BHK
• traducción de doble negación
• modelos de Kripke para el intuicionismo
• verificacionismo

Key theories

Interpretación BHK (basada en la prueba)

La interpretación de Brouwer-Heyting-Kolmogorov explica cada conectivo por lo que cuenta como una prueba de una afirmación compuesta, de modo que 'A o B' requiere una prueba de A o una prueba de B, lo que bloquea el tercero excluido irrestricto.

Argumento antirrealista de Dummett

Dummett argumenta que una teoría del significado restringida por lo que los hablantes pueden manifestar favorece la semántica condicional de verificación sobre la semántica condicional de verdad, y que este antirrealismo exige la lógica intuicionista en todos los ámbitos, no solo en matemáticas.

History

Brouwer fundó el intuicionismo en las décadas de 1900-1920 como un rechazo constructivista de las matemáticas clásicas; Heyting formalizó la lógica intuicionista en 1930. El cálculo de problemas de Kolmogorov y la interpretación BHK aclararon su significado, Kripke posteriormente proporcionó una semántica relacional, y Dummett reformuló el intuicionismo como una consecuencia general del antirrealismo semántico.

Debates

¿El antirrealismo generaliza el intuicionismo más allá de las matemáticas?

Si el argumento de Dummett basado en la teoría del significado extiende con éxito el caso de la lógica intuicionista de las matemáticas al discurso en general, o si la motivación original está esencialmente ligada a la naturaleza constructiva de los objetos matemáticos.

Key figures

• L. E. J. Brouwer
• Arend Heyting
• Michael Dummett
• Andrey Kolmogorov
• Per Martin-Lof

Seminal works

• heyting1956
• dummett2000

Frequently asked questions

¿La lógica intuicionista rechaza todas las pruebas por contradicción?

No todas. Los intuicionistas aceptan probar una negación derivando una contradicción de la suposición, ya que así es como se define la negación. Lo que rechazan es establecer una afirmación de existencia positiva o disyunción simplemente refutando su negación, porque eso no produce un testigo constructivo y se basa en la eliminación de la doble negación, que no es intuicionísticamente válida.