Tengo dos simples preguntas.
A) ¿Se deduce el teorema de completitud de Birkhoff directamente del teorema de completitud de Gödel?
B) ¿Es el teorema de completitud de Birkhoff constructivo en el siguiente sentido? Dada una prueba semántica en álgebra universal, ¿podemos construir explícitamente una prueba sintáctica a partir de ella?
A) Un teorema de completitud para una lógica dice que $T\models \phi$ si y sólo si $T\vdash \phi$ es decir, cada modelo de $T$ satisface $\phi$ si y sólo si existe una prueba de $\phi$ de $T$ . Para dar sentido a esta afirmación, tenemos que fijar un sistema de pruebas para nuestra lógica - los teoremas de completitud tratan de lógicas junto con nociones de consecuencia sintáctica.
El teorema de completitud de Gödel dice que la lógica de primer orden con un sistema de prueba estándar es completa, y el teorema de completitud de Birkhoff dice que la lógica ecuacional con un sistema de prueba estándar es completa. Ahora bien, la lógica ecuacional se encuentra naturalmente dentro de la lógica de primer orden, por lo que el teorema de completitud de Gödel nos dice que si hay una ecuación $\phi$ que está (semánticamente) implicado por algunos axiomas ecuacionales $T$ , entonces hay un de primer orden prueba de $\phi$ de $T$ . Por lo que sabemos, esta prueba de primer orden podría salirse de los límites de la lógica ecuacional.
El teorema de exhaustividad de Birkhoff refuerza esto diciendo que se puede encontrar una prueba en nuestro sistema de prueba ecuacional.
B) No lo sé con seguridad, pero me sorprendería mucho que la respuesta fuera afirmativa.
Gracias por la respuesta. No estoy seguro de "Por lo que sabemos, esta prueba de primer orden podría salirse de los límites de la lógica ecuacional". - ¿podría añadir un ejemplo? ¿Cuál es precisamente la diferencia entre la lógica ecuacional y la lógica de primer orden cuando se aplica, por ejemplo, a la teoría de los anillos?
Una prueba de primer orden es una secuencia de fórmulas de primer orden, cada una de las cuales se sigue de la anterior mediante una regla de prueba válida. En nuestra situación, los supuestos y las conclusiones son ecuaciones, pero los pasos intermedios de la prueba de primer orden pueden incluir fórmulas de primer orden arbitrarias, es decir, con negación, disyunción, cuantificadores existenciales, etc., que no forman parte de la lógica ecuacional.
La lógica ecuacional se limita a enunciados de la forma $t_1(\overline{x}) = t_2(\overline{y})$ , donde $t_1$ y $t_2$ son términos. En primer orden se puede expresar que un anillo es un campo, por ejemplo, pero no se puede hacer con una ecuación.
I-Ciencias es una comunidad de estudiantes y amantes de la ciencia en la que puedes resolver tus problemas y dudas.
Puedes consultar las preguntas de otros usuarios, hacer tus propias preguntas o resolver las de los demás.
