Diferencia entre revisiones de «Lógica intuicionista»

La '''lógica intuicionista''', o '''lógica constructivista''', es el [[Sistema formal|sistema lógico]] originalmente desarrollado por Arend Heyting para proveer una base formal para el [[Intuicionismo|proyecto intuicionista]] de [[Luitzen Egbertus Jan Brouwer|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 [[principio de explosión]]. Esto se debe a una observación de Brouwer de que si enfatizamos lalas noción de pruebapruebas en vez de la de verdad, entonces en los conjuntos infinitos, el [[principio del tercero excluido]] parece fallar. Por ejemplo, si decimos que hay un número natural que es el último número primo, entonces no tenemos derecho a afirmar que esa proposición es verdadera o falsa, pues no tenemos una prueba ni de lo uno ni de lo otro.