Yo soy alguien que le gusta definiciones precisas para las matemáticas de la terminología. Así que, ¿hay algún texto donde hay una definición precisa de un efectivo de la prueba? El concepto es vago para mí.
Respuestas
¿Demasiados anuncios?
No hay una sola definición formal de una "efectiva de prueba", así como no existe una única definición formal de "constructiva" a prueba.
Lo que se sabe es que, si la existencia de un objeto matemático es demostrable a partir de determinados axioma de sistemas, a continuación, el objeto en sí mismo debe ser computable. Esto es más claro cuando el objeto es de un tipo al que "computable" fácilmente se aplica: un conjunto de números naturales, una función de los números naturales a los números naturales, etc.
Uno de esos axioma del sistema, el uso de la lógica clásica, es el sistema de segundo orden aritmética conocida como $\mathsf{RCA}_0$. Debido a que este sistema tiene un modelo en el que cada objeto es computable, cualquier objeto que la teoría resulta de existir debe ser computable. Hay sistemas que tienen propiedades similares, pero el uso no-clásica intuitionistic lógica.
No la lógica clásica, otra forma de obtener computable a los testigos para existencial declaraciones es el método de la realizabilidad; esto está estrechamente relacionado con el BHK interpretación constructiva de las matemáticas. Hay sistemas para que cada comprobable instrucción tiene un computable realizer, y estos realizers dar computable a los testigos.
También estrechamente relacionado con los campos de la computables análisis (que, por convención, se utiliza la lógica clásica) y análisis constructivo (que, por convención, se utiliza intuitionistic lógica). Estas áreas están directamente relacionadas con las pruebas de que los objetos construidos son computables o constructivo en varios sentidos.
Willemien
Puntos
2422
Una estrictamente la definición formal de una axiomática de la prueba:
Una prueba de un teorema es una lista de fórmulas donde:
1) Cada fórmula es
1a) un axioma o
1b) puede ser deducida a partir de una o más fórmulas anteriores en la lista por una determinada regla de inferencia.
y
2) el teorema de la prueba es la última fórmula en la lista.
Aviso que casi ninguna prueba se da de esta manera.
