Ciclo Kurt Gödel 1: Teorema de Completitud

B

[Borrado] #1 May '13

Hace ahora mismo 107 años y unos días (28 de abril) nació Kurt Gödel, la persona que desbarató cualquier atisbo de consistencia en las matemáticas y que puso fin a la noción de que las mismas no tenían límite, que eran autocontenidas. No obstante poca gente sabe que también unió lo que es verdadero y lo que se puede demostrar, que será la piedra angular de este hilo.

Todo será a nivel introductorio, aunque puede que haya alguna formulita. Si no tenéis TeX the world os puede ser útil. Si no os funciona ya lo pasaré a mathbin.

Paso 1: Qué es una interpretación de una fórmula

La mayoría de lenguajes formales (lógica de primer orden en nuestro caso) solo describen sintácticamente fórmulas que serán válidas o no. Es decir, tenemos una serie de normas que nos dicen si una proposición es correcta sintácticamente, por ejemplo los cuantificadores van al principio, los paréntesis engloban los términos de las funciones, etc.

Por ejemplo tenemos la siguiente fórmula correcta:

'[; \forall x_1 \forall x_2 \exists x_3 R(f(x_1,x_2),x_3) ;]'

Para todos los x1, para todos los x2, existe un x3 tal que la operación entre x1 y x2 está relacionada con x3.

Esto es sintácticamente correcto pero no significa nada. Tenemos que darle una interpretación.
La interpretación se da a las variables, a las relaciones y a las funciones, pero no a los símbolos lógicos: para todo significa lo que todos entendemos, existe igual, "o", "y", "no" e "implica" más de lo mismo, es decir los símbolos lógicos son los que vienen dados por sus tablas de verdad, y los cuantificadores los que entendemos desde siempre (ojo, hay lógicas que lo cambian pero ya no son la de primer orden: lógica difusa, lógica modal...).

Por ejemplo ahora nuestra interpretación será: Las variables son números enteros. la función f(x1,x2) es x1+x2, y la relación R(x,y) será "y divide a x".
En este caso nuestra fórmula se traduce a: Para todo x1, x2 existe un x3 tal que x3 divide a x1+x2.

Y esto es cierto en esta interpretación!!
Cuando tenemos una fórmula bien escrita que es cierta en alguna interpretación decimos que la fórmula es satisfactible: Se satisface bajo cierta interpretación. En este caso la interpretación, o el modelo, es A, y la fórmula la llamaremos φ, diremos que A satisface φ, o escrito en lenguaje matemático:
A ⊧ φ

Ahora tenemos esta fórmula:
'[; \exists x \neg x = x ;]'
Existe x tal que x no es igual a x.

Esta fórmula, le demos el significado que le demos a las variables (manzanas, números, espacios topológicos...) es siempre falsa: No es cierto que exista un elemento que no sea igual a sí mismo. Esta fórmula es insatisfactible.

En cambio su negación: Existe x tal que x es igual a x, es cierta lo interpretemos como lo interpretemos: Es una tautología, es una fórmula válida. Si a la fórmula la llamamos φ escribiremos:
⊧ φ

Volviendo a la primera fórmula, ahora interpretemos de otra manera: Los elementos son enteros de nuevo, la función es la suma, pero la relación significa que la multiplicación da 1. Ahora nuestra fórmula es: Para todos enteros x1, x2 existe un entero x3 tal que (x1+x2)x3 = 1. Esto no es cierto: si x1 = 2, x2 = 2 no existe ninguna x3 tal que x34 = 1. Esta fórmula por tanto se satisface en ciertas interpretaciones y no se satisface en otras: No es válida.

Si tenemos una fórmula con variables libres, por ejemplo φ[x]=R(x), también podemos interpretar y ver si es cierto: por ejemplo aquí las variables son los enteros y R es "es par", entonces la fórmula φ[2] (es decir, sustituyendo x por 2) se satisface bajo este modelo. Escribimos A ⊧ φ[2]

Otra cosa que se escribe comúnmente es algo como:

G ⊧ φ donde G es también una colección de fórmulas. Esto es una manera rápida de escribir
⊧ G -> φ , es decir que la fórmula "los axiomas de G implican φ" es una tautología, es decir que en cualquier interpretación en la que G se satisfaga φ también se satisface.

Paso 2: Demostración y derivación de una fórmula

Fijaos que hasta ahora todo lo que hemos hecho es, dada una afirmación, ver si se cumple o no al darle significado a sus partes. Para ver si se cumple pues usaremos nuestras herramientas de la aritmética, geometría, lo que corresponda a la interpretación. Pero no hemos hecho nada con la sintaxis de la fórmula. Todo ha sido en base a la semántica.
No obstante, nosotros podemos tener una serie de reglas de deducción sintáctica, algo que podríamos enchufar a un ordenador y que haga teoremas. Estas reglas se llaman LK, introducidas por Gentzen en 1936. Por ejemplo una regla dice:
_____________(Ax)
A , φ => B, φ

Básicamente esto significa que siempre que tengamos la misma fórmula a un lado y al otro de la implicación esto es totalmente deducible de la nada.

Otra dice:
A => B, φ[y/x]
______________(∃R)
A => B, ∃xφ
(es decir que del hecho que A implique B y φ para cierto y, se deduce que A implica B y la existencia de un cierto x que cumpla φ).

Y otra dice:
A, t=t => B
_______________(Ref)
A => B
(Es decir que t=t no añade información).

Vamos a demostrar que ∃x x = x es deducible:

____________________(Ax)
x = x [y/x] => x = x [y/x]
____________________(Ref) (es lo mismo que decir y = y => y=y)
=> x=x [y/x]
___________(∃R)
=> ∃x x=x

Como veis esto lo podría hacer un ordenador mismamente.
Cuando una fórmula φ es deducible se escribe:
⊢ φ

Si escribimos que de unos axiomas A se deduce un conjunto de fórmulas B, escribimos:
A ⊢ B

Paso 3: La relación
Fijaos que a priori tenemos por un lado el hecho de que una afirmación sea válida o no dados unos axiomas, y por otro el hecho de que sea deducible mediante un cálculo lógico. Intuitivamente puede parecer lo mismo... Y lo es!
Teorema de completitud (de Gödel)
⊧ = ⊢

Recordad que siempre hablamos de lógica de primer orden, y cálculo LK. Es decir, todo lo que es válido es deducible por una máquina. Es decir, si una fórmula es válida, entonces es perfectamente deducible.

Hay varias demostraciones, yo estudié el método de Schütte, que estudia los árboles que se generan de posibles deducciones, y demuestra que toda fórmula válida tiene un árbol finito de deducción.

La más simple y famosa es la de Henkin:
Decimos que un conjunto de fórmulas F es consistente si y solo si no existe ninguna fórmula φ tal que F ⊢ φ y F ⊢ ¬φ.
El teorema escrito en la manera de Henkin dice que un conjunto de fórmulas F es satisfactible (es decir, hay una interpretación en la cual F es cierta) si y solo si F es consistente.

Bueno, pues aquí tenéis el primer gran descubrimiento de la lógica , básicamente dice lo siguiente:
Con un ordenador podemos generar teoremas y tener la certeza de que serán cosas que pasarán en la interpretación.

Espero que os haya parecido un poco interesante, la próxima edición será sobre los de incompletitud. Creo sinceramente que estos teoremas cambiaron radicalmente la manera de pensar en matemáticas igual que la incertidumbre cambió radicalmente la manera de entender el mundo, y me sorprende que aún ahora, 100 años después, la mentalidad de la sociedad no haya cambiado tanto ni tenga estos resultados como algo "fundamental".

8

T-1000 #2 May '13 en la nevera

No entiendo nada pero me parece interesante estos temas.

3

Polakoooo #3 May '13 Mortadelo

Voy a leérmelo detenidamente aunque de primeras no entiendo nada.

De todas maneras me interesan más las implicaciones/aplicaciones/conclusiones de los teoremas que su formulación puramente matemática. No sé si me explico.

#4 ya, pero es que si no me lo dices así mascadito como has hecho ahora mi cerebro no me da para hacer esa conclusión por mí mismo. Y aún insinúas más cosas en las que me gustaría que profundizaras xD.

1 3 respuestas

B

[Borrado] #4 May '13

#3 te parece poca implicación el hecho de que podemos poner un ordenador a generar teoremas que serán válidos para nuestros modelos?
O que podemos hacer un modelo para un sistema axiomático siempre que este sistema axiomático sea consistente?

Estos resultados son fundamentales (en el sentido de que son la fundamentación) en las matemáticas modernas, y por ende en la comprensión de nuestros esquemas y procesos mentales a la hora de deducir. Pero la belleza está en cómo se estudia la matemática desde la propia matemática (y en el de incompletitud aún es mejor). En ese momento la gran pregunta era: Las matemáticas son un sistema cerrado? Es decir, podemos demostrar que las matemáticas son ciertas desde las propias matemáticas? El trabajo de Gödel fue revelador en ese campo.

2 respuestas

B

[Borrado] #5 May '13

La lógica clásica, en resumen. Conocía lo básico, espero la segunda parte, promete ser revelador.

Gran trabajo

1 respuesta

B

[Borrado] #6 May '13

#3 dime las cosas que te interesa que profundice y lo intento (tampoco soy un experto XD).
#5 tú lo has dicho, esto es la lógica clásica y realmente visto desde la perspectiva actual de las matemáticas ya queda un poco lejos: La lógica se dividió en teoría de modelos, teoría de la prueba, teoría de conjuntos, etc. y hay resultados muy impactantes en teoría de modelos por ejemplo como el teorema de compacidad. Pero todo eso no habría existido nunca sin este primer gran teorema de completitud.

Deoxys #7 May '13

Mola, nunca me había parado a pensarlo. Espero tu próximo thread

De todas formas, ¿Cómo generas teoremas con un ordenador? ¿Generas fórmulas aleatorias y luego aplicas el teorema? No parece muy práctico.

1 respuesta

urrako #8 May '13

#3 Básicamente esto sentó las bases sobre las que se comenzó a trabajar en lo que se podía calcular (entendiendo cálculo como cálculo lógico, es decir, como el desarrollo de una serie de sentencias que arroje un resultado de verdad -o de no verdad- y este lleve asociado una acción). Gödel, turing y Von Neumann desde la Matemática comenzaron lo que sería la Computación. Que me corrija Duronman si me equivoco.

3 2 respuestas

eisenfaust #9 May '13

#8 Eh, no os olvideis de Alonzo Church, cabrones xd

2 1 respuesta

B

[Borrado] #10 May '13

#7 Aleatorias no, partes de tus axiomas y generas mediante las reglas del cálculo LK nuevos teoremas.

Ojo, no es muy práctico tener un generador de teoremas "al azar" y menos con las reglas de cálculo --las cosas se hacen de manera mucho más eficiente ahora-- pero como ya he comentado, este teorema sentó las bases, dijo "es posible" en los años 20 y evidentemente hasta ahora ha mejorado mucho. Como dice urrako en #8 , él, Von Neumann y Turing fueron los elementos clave en el desarrollo de la computación. Pero todo hay que mirarlo desde la perspectiva correspondiente (años 30).

edit: Y Alonzo Church #9 xD, de cálculo lambda no tengo ni idea así que no lo conocía.

1 1 respuesta

Eyvindur #12 May '13 Cofrade

Nada como leer chino mientras me tomo el café de la tarde xD.

Btw, buen trabajo #1, me lo he leído pero me pierdo 5 veces por línea.

5

Zerokkk #13 May '13

Vamos que en base a este teorema, podemos deducir si una fórmula es cierta en base a la interpretación que se le de, no? O mejor dicho, ver bajo que interpretaciones lo es (según si es satisfactible o no en base a ellas).

Se escapa bastante de las matemáticas de toda la vida, es como una mezcla de las mismas con operaciones lógicas de cualquier lenguaje de programación, así que como has dicho, deduzco que esto ha sentado las bases de dichas operaciones lógicas.

Bastante interesante, sí.

1 respuesta

B

[Borrado] #14 May '13

#13 no exactamente, lo que dice el teorema es que, si una fórmula es cierta en cualquier modelo que tome otras fórmulas como ciertas, entonces esta fórmula es deducible a partir de las otras fórmulas y las reglas del cálculo lógico. Y viceversa. Por ejemplo tú tienes una deducción que traducida dice algo así:

Siempre que haya una relación que cumpla estas propiedades, se tienen estas otras propiedades. (y toda una deducción de por medio)

Entonces no importa la interpretación que les des a los elementos o a la relación, siempre que la relación cumpla las propiedades que pides se cumplirán las otras.

Esto no implica que dada una fórmula puedas saber si es deducible o no. Esto está relacionado con el problema SAT y la herbrandización de las fórmulas con cuantificadores y es un poco más complicado, hasta donde yo llegué era un problema semidecidible (no sé si hay más hecho al respecto)

B

[Borrado] #15 May '13

#4

1

Lexor #16 May '13 Tirachinas

herbrandización ¿?

1 respuesta

M0E #17 May '13 meneador

¿Podemos demostrar que las matemáticas son ciertas desde las propias matemáticas?

En ese momento es cuando me explotó la cabeza.

1 respuesta

B

[Borrado] #18 May '13

#16 perdona, no te contesté en su momento. La herbrandización de una fórmula, y su forma normal de Skolem son transformaciones de una fórmula lógica que varían su significado pero tienen la propiedad de mantener la validez o la satisfactibilidad de las mismas.

Hablando en cristiano, tú tienes una fórmula en plan "Para todo x existe una y tal que x e y están relacionados", pues de ahí construyes otra frase que dice "Para todo x, x y f(x) están relacionados" (y la interpretación de la f ya la darás tú). Esto no es lo mismo pero conserva propiedades lógicas que te interesan para demostrar dos teoremas esenciales:
El teorema de Herbrand: Básicamente, puedes convertir fórmulas de lógica de primer orden (es decir, con cuantificadores "existe" y "para todo" ) a fórmulas de lógica proposicional o booleana (es decir, solo "o", "y" y "no" ) .
El teorema de Löwenheim-Skolem: Este te dice que con una teoría hecha con lenguaje de primer orden no puedes restringir la cardinalidad de tu modelo. Es decir, si tú tienes una serie de fórmulas y hay un modelo con infinitos elementos que las cumple, entonces hay modelos con "cualquier infinito" que se te pueda ocurrir (lo de los infinitos tiene guasa y no me voy a extender). Este junto a otro básicamente te dice que o bien tu modelo no puede tener más de "N" elementos para N prefijado, o bien tiene cualquier rango de "infinidad" de elementos.

No sé si te he aclarado algo porque esto de Herbrand y Skolem ya son palabras mayores y antes de entender el teorema hay que entender el problema xD cosa que yo no entiendo.

#17 xD, pues fue la gran pregunta a principios de siglo pasado, y el segundo teorema de Gödel que explicaré en otro hilo lo echó todo a perder, claro. Los matemáticos (Hilbert) entonces creían que la matemática era un lenguaje mucho más potente que el natural y que por tanto era "completo" en el sentido de autocontenido... Y no. No obstante (y esto ya lo explicaré mejor), esto es cierto en una teoría suficientemente "débil" como la geometría de Euclides (con sus axiomas bien hechos ya que Euclides asumió cosas que no escribió) ya que se puede axiomatizar sin usar teoría de conjuntos. Pego aquí una cita de la wikipedia:
...when we begin to formulate the theory, we can imagine that the undefined symbols are completely devoid of meaning and that the unproved propositions are simply conditions imposed upon the undefined symbols.
Then, the system of ideas that we have initially chosen is simply one interpretation of the undefined symbols; but..this interpretation can be ignored by the reader, who is free to replace it in his mind by another interpretation.. that satisfies the conditions...
Logical questions thus become completely independent of empirical or psychological questions...
The system of undefined symbols can then be regarded as the abstraction obtained from the specialized theories that result when...the system of undefined symbols is successively replaced by each of the interpretations...
—Padoa, Essai d'une théorie algébrique des nombre entiers, avec une Introduction logique à une théorie déductive qulelconque

Y para poner algo de Russell que no puede faltar aquí:
If our hypothesis is about anything, and not about some one or more particular things, then our deductions constitute mathematics. Thus, mathematics may be defined as the subject in which we never know what we are talking about, nor whether what we are saying is true.

Estos fragmentos resumirían lo que pasaron a ser las matemáticas en el siglo pasado. Hasta entonces las matemáticas estudiaban "objetos" ideales en un mundo platónico, y bueno, aún ahora hay distintas aproximaciones al tema pero eso ya entra más en filosofía.

elkaoD #19 May '13

#10 "de cálculo lambda no tengo ni idea"

¡Buuuuu!

La verdad es que es sencillo y a la vez acojonante. Échale un vistazo.

Todo esto lo di el año pasado y aún me despierto sudando a veces mientras grito "SKOLEEEEEMMMMMM!!".

La verdad es que mola pero qué mal lo pasé (asignatura: Conocimiento y Razonamiento Automatizado) con tanta matemática. Cuando llegamos a verificación y demás (invariantes en bucles y otras mierdas) mi cerebro hizo reset.

ALSO: queremos LaTeX en MV.

B

Bidroid #20 May '13

Entro al hilo
me siento subnormal
salgo.

1