En la lógica proposicional, ¿cómo probar el teorema de eliminación de doble negación sin usarlo?

Creo que no es un teorema sino un axioma de la lógica proposicional convencional.

Actualizar:

De hecho, esto es lo que dice Wikipedia:

La eliminación doble negativa es un teorema de la lógica clásica, pero no de lógicas más débiles, como la lógica intuicionista y la lógica mínima. Debido a su carácter constructivo, una declaración como No es el caso de que no llueva es más débil que Llueve. El último requiere una prueba de lluvia, mientras que el primero simplemente requiere una prueba de que la lluvia no sería contradictoria. (Esta distinción también surge en el lenguaje natural en forma de litotes). La introducción de la doble negación es un teorema de la lógica intuicionista y la lógica mínima, como es .
Eliminación doble negativa

El teorema de la eliminación de la doble negación dice que para cada fórmula proposicional [matemática] \ phi [/ matemática] tenemos que [matemática] \ phi \ iff \ neg \ neg \ phi [/ matemática] es un teorema de lógica proposicional. Lógica proposicional clásica, es decir. La equivalencia de una fórmula y su doble negación no es un teorema en la lógica proposicional intuicionista, solo la implicación [matemáticas] \ phi \ Rightarrow \ neg \ neg \ phi [/ matemáticas] es intuitiva.

Dado que los sistemas de prueba habituales para la lógica proposicional clásica son sólidos y completos, podemos establecer que una fórmula es demostrable, ya sea presentando una prueba (dentro del sistema de prueba) o mostrando que la fórmula es una tautología o que la fórmula es demostrable utilizando las reglas de prueba del sistema de prueba.

En el caso de [math] \ phi \ iff \ neg \ neg \ phi [/ math], es fácil establecer que la fórmula es una tautología, ya que tenemos para cada fórmula [math] \ phi [/ math] que [math] \ neg \ phi [/ math] es verdadero si y solo si [math] \ neg \ phi [/ math] es falso. En consecuencia, [math] \ phi [/ math] y [math] \ neg \ neg \ phi [/ math] siempre tienen el mismo valor de verdad.

Podría probarlo utilizando algún principio que sea esencialmente equivalente, como las formulaciones de contraposición o reducción ad absurdum de conclusión positiva. Pero eso es todo lo que puedes hacer. Como han señalado otros escritores, la presencia de la eliminación de la doble negación es la característica que distingue la lógica clásica de la intuicionista, por lo que, por supuesto , no se puede probar a partir de otros principios lógicos. Si pudiera ser, sería intuitivamente válido, lo cual no es.