Prueba teóricamente intuitionist lógica es una sub-teoría de la lógica clásica. La Wikipedia el artículo indica que esta indicando que si tenemos un cierto conjunto de axiomas para intuitionist lógica de los axiomas puede ser encontrado en la sección titulada "de Hilbert estilo de cálculo", entonces la lógica clásica puede obtener obtenidos por incorporarse al sistema de la ley del medio excluido... en notación polaca ApNp, Peirce ley CCCpqpp, o la ley de la doble negación eliminación CNNpp, o con la definición de Np := Cp0, podríamos escribir CCCp00p.
Por lo tanto, todas las pruebas se hace en un intuitionist marco de la lógica de trabajo como pruebas para cualquier marco de la lógica clásica, pero no todas las pruebas que realiza en un clásico de la lógica del marco de trabajo en cualquier intuitionist marco de la lógica.
Por ejemplo, uno podría deducir que el Cpp de un clásico marco de la lógica de la siguiente manera:
thesis 1 CCpqCCqrCpr
thesis 2 CpCNpq
thesis 3 CCNppp
DD123 4 Cpp
Esto es no una posible prueba de la Cpp en cualquier intuitionist marco de la lógica, ya que CCNppp no es una tesis en cualquier intuitionist lógica (el término "tesis" se refiere a una fórmula que es o bien un axioma o teorema).
Semánticamente hablando intuitionist lógica califica como mucho más rica que la lógica clásica en la que la verdad para intuitionist lógica es de valor infinito, mientras que la de la lógica clásica es de dos valores. Semánticamente hablando, intuitionist lógica se comporta de la misma manera como la lógica clásica cuando la verdad-valores se limita a "True" y "False". En tal caso, cada fórmula sea interpretado desde la perspectiva de la lógica clásica o intuitionist lógica da el mismo resultado. Pero, intuitionist lógica puede obtener dijo a rechazar la ley de bivalence en que no hay dos valores de los modelos de intuitionist lógica calificar como adecuada para una semántica de la misma.
