[LauLuna]

Si mis formalismos llevan a confusión, realmente no tengo ningún inconveniente en ceder esta tarea de desarrollarlos a quien desee tomarla. No tiene más que "levantar la mano" y yo gustosamente le cederé mi puesto en esta especie de "estrado virtual" en el que siento que me hallo.

No, de ningún modo me parece eso recomendable. Creo que vamos muy bien.

Si habías definido 'conjunto axiomas' y 'sistema de axiomas' como sinónimos, entonces pido perdón, no lo recordaba. Tal vez convendría haber dicho algo así como 'si no hay una fórmula P tal que P y no -P sean demostrables en el conjunto de axiomas'; es la ausencia de la palabra 'demostrables' la que me ha confundido un poco.

Pero todo está claro ahora.

[argentinator]

Los cito a ambos, a ver si se amigan.

Argentinator, técnicamente (en Teoría de Modelos) una teoría es un conjunto C de sentencias en un lenguaje lógico formal con la condición de que C esté cerrado bajo la relación de consecuencia lógica: para todo p y q, si p pertenece a C y q es consecuencia lógica de p, q pertenece a C.

Pero en un sentido más amplio es usual llamar también teorías a los sistemas formales axiomáticos. En algunos de estos sistemas el conjunto de los teoremas es efectivamente una teoría, particularmente en los sistemas de primer orden: como la lógica de primer orden es completa (Gödel 1930), toda consecuencia lógica de los axiomas es también un teorema del sistema. Pero en algunos de ellos, como la aritmética de Peano de segundo orden, el conjunto de los teoremas no es una teoría en el sentido más estricto, porque no toda consecuencia lógica de los axiomas es un teorema.

Como sabes, los sistemas formales axiomáticos están compuestos por axiomas o esquemas axiomáticos y reglas de inferencia.

(Cuando digo sistema es que incluyo a las reglas de inferencia, si éstas son fijadas de antemano, como habitualmente se hace, entonces "sistema de axiomas" y "conjunto de axiomas" son virtualmente sinónimos).

Parece que en sistema se incluyen las reglas de inferencia.
Yo no había notado que había dos cosas distintas.
Por ahora para mí las reglas y axiomas que ha enumerado Gustavo son ''EL'' sistema. 

[argentinator]

Me voy a contestar yo solo algunas cosas.

1er pregunta:  ¿Qué pasa si deseo reemplazar x por t, cuando t es un término que ''adentro'' contiene a la misma x?
¿No es esto algo mal definido, no queda algo recurrente e infinito, como producto de reemplazos sin fin?

Estudiando el asunto me doy cuenta que caí en la trampa de mi propia estupidez.
Si uno reemplaza una variable por un término, se sigue obteniendo una fórmula sin problema alguno, y si en el reemplazo de x por t resulta que dentro de t figura la misma x, como por ejemplo, si t es el término (x+S(z)).(x.y) no parece haber ningún contrasentido en lo que queda tras el reemplazo de F(x) por F(t).

En todo caso, lo que uno puede apreciar es que el Axioma de Reemplazo dice más de lo que puede percibirse a simple vista, y que no está de más reflexionar cuán extravagante y general puede ser el ''reemplazo'' que se vaya a hacer con cierto término t.

2da pregunta: En cuanto a la restricción de los cuantificadores (en el axioma de reemplazo)...

Me estuve fijando en el libro de Martínez/Piñeiro, y los axiomas están del mismo modo en que Gustavo los ha introducido acá en el foro. En cuanto al Axioma de Reemplazo ya me queda más claro cómo se debe restringir el término t:
En la fórmula F(x) (libre en x) pueden aparecer ciertas variables \( z_1,...,z_m \) afectadas por cuantificadores.
Ninguna de esas variables debe figurar en t.
Es lo mismo que ha dicho Gustavo, pero hasta que no lo escribo yo mismo parece que no me convenzo.

Las dudas que expuse a continuación, esas aún no las he aclarado por mi cuenta.

[LauLuna]

Las dudas que expuse a continuación, esas aún no las he aclarado por mi cuenta.

Creo que preguntabas si el conjunto de los términos es recursivo, es decir, si hay un algoritmo que, dada una cadena de símbolos del lenguaje, decida si esa cadena es o no un término.

Sí, si es recursivo. Hay una manera de examinar los símbolos de una cadena uno a uno para decidir si una cadena responde o no a las reglas de formación de términos. Es posible decidir si la cadena es o no un término con un solo símbolo, es decir, una variable ó 0. Es posible decidir (en un número finito de pasos) si la cadena es de la forma St, t+t', txt', donde t y t' son términos.

El hecho de que determinados conjuntos de fórmulas del sistema (el de los términos, el de las variables, el de los enunciados, el de los axiomas, ...) sean recursivos será luego una pieza clave en la demostración del teorema.

Un saludo.

[Gustavo Piñeiro]

Tal vez convendría haber dicho algo así como 'si no hay una fórmula P tal que P y no -P sean demostrables en el conjunto de axiomas'; es la ausencia de la palabra 'demostrables' la que me ha confundido un poco.

Sin embargo...

Definición: Un conjunto de axiomas es consistente si no existe una fórmula \( P \) tal que \( P \) y \( -P \) sean a la vez demostrables.

..la palabra "demostrables" estaba allí, tan campante al final de la definición.

Otra definición, que faltó en la lista anterior:

Definición: Un conjunto (o un sistema) de axiomas es completo si para todo enunciado \( P \) sucede que, o bien \( P \), o bien \( -P \), es demostrable.

Todo sistema inconsistente es trivialmente completo, pero no es ésa una completitud deseable.

<<                >>

[argentinator]

Vuelvo a tener dudas sobre el Axioma de Reemplazo.
¿No permite reemplazos demasiado arriesgados o generales?
Durante largo tiempo creí que se usaba para reemplazar una variable por una constante, o un ''calculito'' que involucra sólo constantes.
Pero el hecho de que se admitan también variables en el reemplazo, me parece extraño, con peligro de caer en alguna incoherencia, aunque no veo en realidad ninguna todavía...

Pasando a otra cosa.
Gustavo, en vuestro libro veo que ahora deberían seguir los axiomas de primer orden de la aritmética y la definición de recursiva de verdad, en ese orden.
¿Se puede dar una noción de verdad sin haber dado antes los axiomas de la aritmética?
Pregunto, porque veo que en la definición de verdad se usan numerales, y me cuesta aceptar que la noción de verdad dependa de la aritmética.

Tampoco entiendo bien el papel que los numerales juegan en todo esto.
Estuve leyendo el libro de "Nagel y Newman, El Teorema de Godel", y hace una distinción entre numerales y números, la cual creí que entendía, pero buscando en la lista de axiomas de "Godel \( \forall{} \)" no encuentro el momento a partir del cual se hace esa distinción (no quiere decir que no la haya). Así que ando algo mareado con el hecho de que se han de usar los mismos números naturales en la definición de verdad.

[Gustavo Piñeiro]

1er pregunta: Se ha establecido que todo término contiene constantes o variables. En particular x es una variable. ¿Qué pasa si deseo reemplazar x por t, cuando t es un término que ''adentro'' contiene a la misma x?
¿No es esto algo mal definido, no queda algo recurrente e infinito, como producto de reemplazos sin fin?

Ya diste la respuesta en otro comentario. Sólo ratifico lo dicho allí: no hay ningún problema, ni sucede ninguna regresión infinita. En "x = x" podemos reemplazar "x" por, digamos, "x + 0" y obtenemos "x + 0 = x + 0".

2da pregunta: En cuanto a la restricción de los cuantificadores...
Si t es un término, es una lista de signos en la que no figura el signo de cuantificación \( \exists{} \).
Así que si pido que las variables que figuran en t no estén afectadas por cuantificadores, entiendo que esos cuantificadores son ''externos'' a t. Así que imagino que se refiere a cuantificadores que podrían aparecer dentro de F.
¿Pero qué significa exactamente la restricción?

En efecto, en el libro se muestra un ejemplo del sentido de esa restricción. Supongamos el enunciado \( \forall{x}\exists{y}(x\neq{}y) \). Si aplicamos el esquema lógico y reemplazamos x por 0 obtenemos la fórmula (intutivamente verdadera, aunque aún no hemos definido qué es la "verdad"): \( \exists{y}(0\neq{}y) \), pero si reemplazamos x por y (reemplazo "prohibido" porque es una variable afectada por un cuantificador) nos queda \( \exists{y}(y\neq{}y) \), que no querríamos que fuera demostrable.   

Una cuestión filosófica:
Para decidir si una expresión es un término o no lo es, tengo que rechazar por ejemplo las expresiones que tengan cuantificadores.
Cuando se da la definición de término, está bien, se hace de modo constructivo.
Pero ¿qué pasa si me dan una expresión t cualquiera, y debo determinar si es o no un término?
Para probarlo, debo pasar uno a uno por sus signos, y si encuentro un símbolo que no corresponde a constantes o variables o paréntesis, concluir que t no es un término.
Sin embargo, no estoy seguro de si la propiedad de ''no ser un término'' forma parte de las reglas que definen lo que es un término.
Me refiero a que yo me doy cuenta con mi propia razón que una expresión no es un término, pero no estoy seguro de si esto se deduce propiamente de las reglas dadas, las cuales se dan en ''positivo'' (o sea, para afirmar cuándo tengo un término), pero no en negativo (cuando deseo probar que algo no es un término).

"No ser un término", al menos en teoría, está perfectamente definido: una expresión no es un término si no puede ser construida siguiendo las reglas que permiten construir los términos (parece un trabalenguas, pero es así). Otra cuestión es dar un método práctico para determinar si una expresión dada es, o no es, un término. Tal método (o algoritmo, para ser más preciso) existe. No se reduce a ver meramente que no haya cuantificadores ni otros símbolos lógicos, ya que (((((0+ no los tiene y no es un término.

Creo (nunca lo había pensado antes) que ese método debería rastrear los paréntesis anidados que forman la expresión. Debe detectar los símbolos "más profundamente enterrados" entre paréntesis, ver que forman una expresión del tipo corercto (0 + x, 0.x, etc.) y de allí ir rastreabdo símbolos mientras va subiendo por los niveles de paréntesis. No sé si he sido claro (casi seguramente no), pero creo que por allí va la idea.

Saludos,

[Numerarius]

Se me ocurre una analogía que, tal vez, podría resultar útil.

La capacidad de reconocer que una fórmula lógica está bien construída se podría comparar (por ejemplo) a la capacidad que tiene un compilador para reconocer un programa en lenguaje Java.

En este sentido, me refería antes a que existen autómatas que reconocen cadenas sintácticamente correctas.

[Fernando Revilla]

Bien, los términos de un lenguaje \( \mathcal{L} \) de primer orden quedan perfectamente determinados por las siguientes reglas:

(i) Las variables \( x_i \) y las constantes \( a_j \) del lenguaje son términos.
(ii) Si \( f_i^n \) es letra de función y \( t_1,\ldots,t_n \) son términos de \( \mathcal {L} \) entonces, \( f_i^n(t_1,\ldots,t_n) \) es un término de \( \mathcal{L} \).
(iii) El conjunto de todos los términos de \( \mathcal{L} \) es el generado por (i) y (ii).

Es decir, las reglas anteriores "deciden" si una expresión de \( \mathcal{L} \) es o no término.

Saludos.

[argentinator]

Lo que noto es que cuando vaya a hacer la rutina que reconozca si cierta expresión satisface el Axioma de Reemplazo, no va a ser sencillo. O, al menos, va a haber que andarse con cuidado.
Hasta que no haga el/los programas, no voy a convencerme de que ciertas reglas ''deciden'' o no tal o cual cosa.

Phidias... Eso del ''conjunto de todos los términos'' no lo veo bien en este contexto en que no hay conjuntos.
Esa totalidad no está bien definida.
Uno sólo puede estar seguro de una afirmación del tipo:
"Si t satisface tal y tal, entonces t es un término".
Pero no se puede decir metamatemáticamente algo como:
"Para todo t tal que blablabla: t es un término".

De manera que sólo puedo observar cada t, uno a uno.
Hablar de todos los t es algo que se entiende, pero no es finitario. ¿Prohibido? Creo que sí.