Saltar al contenido

El teorema de completitud de Gödel y la indecidibilidad de la lógica de primer orden

Esta pregunta se puede resolver de diferentes maneras, pero te dejamos la que en nuestra opinión es la solución más completa.

Solución:

Obtuviste la idea correcta para la parte 1, pero es inusual usar la notación lógica que usas: $neg$, $paratodos$, y $existe$ son operadores lógicos, pero $modelos$ es un símbolo metalógico; a los puristas no les gustará que los mezcles. Entonces, puede ser mejor usar el inglés ‘algunos’ y ‘todos’ y ‘no’

Para la parte 2: ¡aquí es donde usas el resultado de la parte 1! En particular, para decidir si $varfi$ es válido o no, usted puede decidir si $negvarphi$ es satisfactoria o no: si $negvarphi$ es satisfactoria, entonces $varfi$ no es válido, pero si $negvarphi$ no es satisfactorio, entonces $varfi$ es válido. Y ahora solo combina eso con el resultado de completitud de Gödel (para ser precisos: el teorema de que un enunciado es demostrable si y solo si es válido… la parte más difícil del ‘si’ es el teorema de completitud): si $varfi$ es válido, entonces es demostrable, y si $varfi$ no es válido, entonces no es demostrable.

Entonces, para esa primera parte: si tienes un algoritmo $mathcalA$ que puede averiguar si $varfi$ es satisfactorio o no para ningún$varfi$, luego algoritmo de diseño $mathcalB$ que está tratando de averiguar si $varfi$ es demostrable o no de la siguiente manera:

  1. Tomar $varfi$

  2. Negar $varfi$

  3. Algoritmo de llamada $mathcalA$ con $negvarphi$

4a. Si algoritmo $mathcalA$ dice que $negvarphi$ es satisfactorio, luego imprima ‘$varfi$ no es demostrable!’

4b. Si algoritmo $mathcalA$ dice que $negvarphi$ no es satisfactorio, luego imprima ‘$varfi$ es demostrable!’

Para mis propios fines, estoy archivando aquí mi mejor intento de integrar, de manera compacta, todo lo que se mencionó en las respuestas a mi pregunta original. Cualquier comentario o crítica de cualquier tipo es siempre bienvenido. Gracias de nuevo a los colaboradores.

Definiciones. Una sentencia $varfi$ es válido si esto es true en todos los modelos. A diferencia de, $varfi$ es satisfacible si esto es true en algún modelo.

Teorema de completitud con solidez. Una oración en lógica de primer orden es demostrable si y solo si es válida.

Entonces, las respuestas a los problemas mencionados anteriormente se pueden dar de la siguiente manera:

  1. Dejar $mathscrM_x$ ser un modelo, $xinmathbbN$. Dejar $varfi$ ser una oración en lógica de primer orden. Dejar $P(x)$ ser el predicado “$varfi$ es true en $mathscrM_x$.” Entonces $forall x P(x) equiv neg exists x P(x)$ y $existe x P(x) equiv neg forall x neg P(x)$ por las definiciones anteriores y las leyes de De Morgan.

  2. Supongamos que tenemos $mathcalA$. Dejar $mathcalB$ Sea el algoritmo definido por el siguiente procedimiento. Paso 1: tomar $varfi$ como entrada Paso 2: negar $varfi$. Paso 3: llamar $mathcalA$ con entrada $negvarphi$, escrito $mathcalA(negvarphi)$. Paso 4, caso (a): Si $mathcalA(negvarphi)$ devoluciones “$negvarphi$ es satisfactoria”, entonces por las equivalencias anteriores $varfi$ no es válido y por el teorema de completitud no es demostrable. Paso 4, caso (b): Si $mathcalA(negvarphi)$ devoluciones “$negvarphi$ no es satisfacible”, entonces por las equivalencias anteriores $varfi$ es válido y por el teorema de completitud es demostrable. Así haciendo uso de $mathcalA$ hemos obtenido $mathcalB$ tal que $mathcalB$ decide si $varfi$ es demostrable o no. Por un argumento simétrico podemos obtener $mathcalA$ si se da $mathcalB$.

Si aceptas, puedes dejar un ensayo acerca de qué le añadirías a este ensayo.

¡Haz clic para puntuar esta entrada!
(Votos: 0 Promedio: 0)



Utiliza Nuestro Buscador

Deja una respuesta

Tu dirección de correo electrónico no será publicada. Los campos obligatorios están marcados con *