¿Acepta el formalismo intuicionista la ley del tercero excluido?
En el contexto de la respuesta dada a su pregunta relacionada, está utilizando dos definiciones diferentes de 'intuicionismo' de dos contextos históricos diferentes.
La noción de intuicionismo de Tarski eventualmente aceptaría "tertium non datur" en una forma debilitada como la que eventualmente propuso Quine, siempre que el proceso formal que define el significado de una fórmula sea algo que pueda ser entrenado en algún uso natural. Su objetivo es capturar la sensación de significado intuitivo que las declaraciones individuales tienen para los lectores.
La noción de intuicionismo de Brower rechazó inmediatamente el "tertium non datur" porque conduce a la especulación ingenua directamente a la paradoja. Su objetivo era mantener su razonamiento lo más ingenuo posible sin enfrentarse a la paradoja, en la creencia de que el razonamiento ingenuo captura un aspecto confiable de la intuición humana.
Los dos no tienen prácticamente nada en común y dan respuestas diferentes a su pregunta.
En general, el intuicionismo se considera una forma de constructivismo. Este último prohíbe utilizar la ley del medio excluido "A o no A". Por lo tanto, la respuesta a su pregunta es "No".
En un contexto no constructivista, la ley del tercero excluido es la base de todas las pruebas indirectas: para probar "A", debes demostrar que "no A" es falso. De acuerdo con la ley del medio excluido, entonces "A" es verdadera.
Como consecuencia, las pruebas indirectas no están permitidas en un contexto intuicionista. Esa es una restricción severa para el "matemático en activo".
nota _ ¿Quiere decir con "formalismo intuicionista" solo una formalización de los principios del intuicionismo?
nwr