Así, una de las cosas que la lógica matemática no es el estudio de los teoremas como objetos abstractos. Hay también muchos teoremas acerca de la lógica matemática, y estos teoremas pueden tener conexiones con otros campos.
Además, la lógica matemática que también ha demostrado que ciertas conjeturas no son formalmente decidable dentro de ciertos sistemas formales. Esto significa que los matemáticos necesitan más fuerte que los sistemas formales para probar.
Sin embargo, tiene un teorema matemático han probado mediante la construcción de la prueba con la lógica matemática? O probar que es una prueba de que existe?
Con esto quiero decir que para la declaración de $C$ que es una conjetura matemática, en lugar de escribir una prueba de $C$, escriben, ya sea constructiva o no constructiva prueba de que la prueba de que existe.
Por ejemplo:
- El uso de la prueba de la teoría para demostrar que hay una secuencia de inferencias para llevar a $C$ (esto está implícito en los anteriores dos balas, por supuesto)
- Uso del modelo de la teoría para demostrar que todos los modelos de la teoría $T$, donde $T$ es una teoría que los matemáticos suelen utilizar para pruebas, satisfacer $C$
- El uso de la informática para la construcción de un programa de $P$, de tal manera que el Curry–Howard correspondencia aplicado a $P$ resultados en una prueba de $C$
Lo que yo soy no buscando ejemplos donde alguien escribe una prueba de $C$, citando los teoremas de la lógica matemática. En este caso, se han escrito una prueba, no simplemente demostró que existe. Como, que todavía es super cool, y tiene enormes implicaciones para el resto de las matemáticas, pero estoy preguntando acerca de algo diferente.
EDIT: Si la hipótesis se utiliza un lexema $L$ que satisface la anterior, que está bien. Sin embargo, se debe utilizar directamente la declaración el lema indica, no el hecho de que se ha abstracta sido probada. Es decir, la prueba de $C$ consiste en mostrar que $L$ implica $C$, no es que la existencia de una prueba de $L$ implica $C$.
Esta es una técnica de advertencia. T no se puede probar "$\forall C. Provable(C) \implies C$". Por otra parte, si se hace por algunos $C$, es vacuously cierto incluso en $T$, ya que uno puede técnicamente sólo escribir una prueba directa de $C$ en $T$. Sin embargo, si $T$ es el sonido, entonces Comprobable(C) no en el hecho de implicar C. Dado que los matemáticos generalmente asumen que las teorías que trabajan en son de sonido (a menos que estén trabajando en la teoría de su meta-matemática significado en lugar de su solidez), esto debe ser aceptable. Por otra parte, lo que demuestra una prueba podría ser más manejable que la escritura es la prueba algunos casos.
