Teoremes d'incompletitú de Gödel

Los **teoremes d'incompletitú de Gödel** son dos célebres teoremes de lóxica matemática demostraos por Kurt Gödel en 1931. Dambos tán rellacionaos cola esistencia de proposiciones indecidibles en ciertes teoríes aritmétiques.

El primer teorema de incompletitud afirma que, so ciertes condiciones, nenguna teoría matemática formal capaz de describir los númberos naturales y l'aritmética con abonda espresividá, ye al empar consistente y completa. Esto ye, si los axomes de dicha teoría nun se contradicen ente sigo, entós esisten enunciaos que nun pueden probase nin refutarse a partir d'ellos. En particular, la conclusión del teorema aplícase siempres que la teoría aritmética en cuestión sía recursiva, esto ye, una teoría na que'l procesu de deducción pueda llevase a cabu por aciu un algoritmu.

La prueba del teorema ye totalmente esplícita y nella constrúi una fórmula, denotada davezu  n'honor a Gödel, pa la que dada una demostración de la mesma, puede construyise una refutación, y viceversa. Sicasí, la interpretación natural de dicha sentencia en términos de númberos naturales ye verdadera.

El segundu teorema de incompletitud ye un casu particular del primeru: afirma qu'una de les sentencies indecidibles de dicha teoría ye aquella que «afirma» la consistencia de la mesma. Esto ye, que si'l sistema d'axomes en cuestión ye consistente, nun ye posible demostralo por aciu dichos axomes.

Los teoremes d'incompletitú de Gödel son unu de les grandes meyores de la lóxica matemática, y supunxeron —según la mayoría de la comunidá matemática— una respuesta negativa al segundu problema de Hilbert.

## Contestu
Los teoremes d'incompletitú de Gödel establecen ciertes llimitaciones sobre lo que ye posible demostrar por aciu un razonamientu matemáticu. Pa falar con precisión sobre qué «puede demostrase» o non, estúdiase un modelu matemáticu denomináu teoría formal. Una teoría formal consta d'una serie de signos y un conxuntu de regles pa manipolialos y combinalos. Por aciu estes regles pueden estremase ciertes coleiciones de signos como fórmules, y ciertes socesiones de fórmules como demostraciones. Los teoremes d'una cierta teoría son entós toles fórmules que puedan demostrase a partir d'una cierta coleición inicial de fórmules que s'asuman como axomes.

A una teoría formal pueden axudicáse-y ciertes propiedaes en función de lo que sía capaz de demostrar. 
* Una teoría consistente nun contién contradicciones, esto ye, nun ye posible demostrar al empar una fórmula y la so contraria. Una teoría que nun sía consistente nun tien utilidá: debíu al principiu d'esplosión, a partir d'una contradicción pueden demostrase toles sos fórmules, y nun sirve pa modelizar razonamientos matemáticos.
*Una teoría completa «respuende cualquier entruga», nel sentíu de que pa caúna de les sos fórmules o bien ye demostrable, o bien esiste una demostración de la so contraria (ye refutable). Una teoría completa ye óptima, y correspuéndese cola intuición sobre la verdá lóxica: al igual que toa sentencia tien de ser verdadera o falsa, nuna teoría completa toa fórmula ye demostrable o refutable. 

Sicasí, el primer teorema de incompletitud establez que, so ciertes hipótesis, una teoría formal nun puede tener dambes propiedaes al empar. La primera d'elles ye que sía una teoría aritmética, esto ye, que los sos símbolos sirvan pa describir los númberos naturales y les sos operaciones y rellaciones; y que sía capaz de demostrar delles propiedaes básiques sobre ellos. La segunda hipótesis ye que sía una teoría recursiva, lo cual significa que les regles pa manipoliar los sos signos y fórmules nes demostraciones han de poder executase por aciu un algoritmu: una serie precisa de pasos ensin ambigüedá que pueda llevase a cabu nun tiempu finito, ya inclusive implementase por aciu un programa informáticu.

## Primer teorema
L'enunciáu del primer teorema reza:

La demostración d'esti teorema pasa por construyir una cierta fórmula, la sentencia de Gödel» , que nun puede ser probada nin refutada en : nin  nin  (la negación de ) son teoremes de . Dizse entós que  y  son indecidibles o independientes en .

Pa llegar a esta, Gödel desenvolvió un métodu pa codificar signos y fórmules por aciu númberos, llamáu numberación de Gödel. Usando esta numberación, ye posible traducir les propiedaes d'una teoría formal , tales como «estos signos constitúin una fórmula» o «estes fórmules nun son una demostración en », a propiedaes aritmétiques de dichos númberos. En particular, la sentencia de Gödel  ye una fórmula aritmética que'l so significáu ye «nun esiste una demostración de  na teoría », o n'otres pallabres, «nun soi demostrable na teoría ».

### Consecuencies
La sentencia de Gödel  nun ye demostrable pero ye cierta, pos afirma precisamente la so propia indemostrabilidad. Esto significa que nenguna teoría aritmética nes condiciones del teorema ye capaz de demostrar tolos enunciaos verdaderos de l'aritmética. 

Amás, anque  sía falsa (por afirmar lo contrario que ) nun ye refutable (puestu  ye indemostrable). Esta sentencia puede tomase como axoma si deseyar y esto nun produz una contradicción. La teoría resultante contién munchos de los enunciaos verdaderos sobre los númberos naturales y dellos falsos, empezando por . Los oxetos descritos por una teoría asina formen un modelu non estándar de l'aritmética.

Tomando  (o la so contraria) como axoma llógrase una nueva teoría  na que  (o la so contraria) ye demostrable automáticamente. Sicasí esto nun invalida'l teorema, yá que  afirma'l so indemostrabilidad relativa a la teoría . La nueva teoría  ye tamién incompleta: puede atopase una nueva sentencia independiente , qu'afirma «nun soi demostrable en ».

A última hora, nuna teoría formal que sía consistente y completa tien de fallar dalguna de les hipótesis: o bien nun ye recursiva y nun hai un algoritmu pa estremar los axomes del restu de fórmules; o bien nun son aritmétiques, y nun inclúin les propiedaes básiques necesaries de los númberos naturales. Por casu, na demostración del teorema de completitud semántica utilícense teoríes consistentes y completes que nun son recursivas. Per otru llau, l'aritmética de Presburger ye una coleición d'axomes sobre los númberos naturales qu'omite delles de les sos propiedaes, a tal puntu qu'una teoría basada nellos pue ser consistente y completa.

## Segundu teorema
El segundu teorema de incompletitud amuesa otru exemplu esplícitu d'una fórmula que nenguna teoría aritmética puede demostrar, amás de . De nuevu, usando la numberación de Gödel, puede atopase una fórmula, denotada , que'l so significáu ye «nun puede atopase una contradicción en », o n'otres pallabres, « ye consistente».

La demostración del segundu teorema rique traducir el primeru a una fórmula. El primer teorema afirma, ente otres coses, que si  ye consistente, entós  nun ye demostrable. La fórmula qu'afirma la consistencia de  ye , ente que la fórmula qu'afirma la indemostrabilidad de  ye la mesma . La fórmula que traduz el primer teorema (una parte d'él) ye , onde «» significa implicación. Gödel demostró qu'esta fórmula ye un teorema, y que polo tanto  nun ye un teorema: si dir, de les regles básiques de  como teoría formal deduciríase que  ye demostrable, en contradicción col enunciáu del primer teorema de incompletitud.

### Consecuencies
El segundu teorema de incompletitud llinda les posibilidaes de demostrar la consistencia d'una teoría formal , yá que nun puede faese utilizando namái la mesma . Amás, si atopa una teoría más fuerte  na que  pueda demostrase, la mesma consistencia de  nun va poder demostrase en  nin tampoco en . Por ello, el segundu teorema considérase una respuesta negativa al llamáu programa de Hilbert, que proponía demostrar la correición de los razonamientos matemáticos basaos n'oxetos infinitu usando tan solu razonamientos basaos n'oxetos finitos, menos potentes que los primeres.

## Enunciaos indecidibles

El primer teorema de inconmpletitud de Gödel demuestra la esistencia d'enunciaos indecidibles o independientes na aritmética de Peano, y tantu el primeru como'l segundu amuesen exemplos concretos d'enunciaos indecidibles. Dende entós atopáronse otros exemplos d'enunciaos independientes de los axomes de Peano, como por casu el teorema de Ramsey «fuerte». Esisten amás numberosos exemplos d'enunciaos independientes n'otres teoríes formales más fuertes que l'aritmética, como la hipótesis del continuu o'l axoma d'elección en teoría de conxuntos; o inclusive en teoríes non direutamente rellacionaes cola aritmética, como nel casu de la xeometría euclídea y el postuláu de les paraleles.

## Discutiniu ya implicaciones
Les resultancies de incompletitud afecten a la filosofía de les matemátiques, particularmente a los puntos de vista tales como'l formalismu, qu'usa la lóxica formal pa definir los sos principios.

Puede parafrasiase el primer teorema diciendo "nunca podrá atopase un sistema axomáticu que sía capaz de demostrar *toes* les verdaes matemátiques y nenguna falsedá".

Per otra parte, dende una perspeutiva puramente formalista esta paráfrasis considerar ensin significáu porque presupon que la verdá» y «falsedá» matemátiques tán bien definíes nun sentíu absolutu, en llugar de ser relatives a cada sistema formal.

La siguiente reformulación del segundu teorema ye inda más esmolecedor pa los fundamentos de les matemátiques:

:*Si puede demostrase qu'un sistema axomáticu ye consistente a partir de sigo mesmu, entós ye inconsistente*.

Por tanto, pa establecer la consistencia d'un sistema S precísase utilizar otru sistema T, pero una prueba en T nun ye totalmente convincente nun siendo que la consistencia de T yá se probara ensin emplegar S.
La consistencia de los axomes de Peano pa los númberos naturales por casu puede demostrase na teoría de conxuntos, pero non na teoría de los númberos naturales por sigo sola.
Esto apurre una respuesta negativa al problema número dos de la famosa llista de cuestiones abiertes importantes en matemátiques de David Hilbert (llamada *[[problemes de Hilbert]]*).

En principiu, los teoremes de Gödel inda dexen dalguna esperanza: podría ser posible producir un algoritmu xeneral que pa una afirmación dada determine si ye indecidible o non, dexando a los matemáticos evitar dafechu los problemes indecidibles. Sicasí, la respuesta negativa al Entscheidungsproblem demuestra que nun esiste tal algoritmu.

Ye de notar que los teoremes de Gödel namái son aplicables a sistemes axomáticos *abondo fuertes*. Esti términu significa que la teoría contién l'abonda aritmética pa llevar a cabu les instrucciones de codificación riquíes pola prueba del primer teorema de incompletud. Esencialmente, tou lo que s'esixe son dellos fechos básicos sobre la adición y la multiplicación tal que por casu formalícense na aritmética Q de Robinson.

Hai sistemes axomáticos inclusive más débiles que son consistentes y completos, por casu l'aritmética de Presburger que demuestra toles afirmaciones de primer orde ciertes aplicando namái la suma.

El sistema axomáticu puede consistir nun númberu infinitu d'axomes (tal que fai l'aritmética de primer orde de Peano), pero pa poder aplicase'l teorema de Gödel tien d'haber un algoritmu efectivu que sía capaz a verificar la correición de les pruebes. Por casu, el conxuntu de toles declaraciones de primer orde que son ciertes nel modelu estándar de los númberos naturales ye completu. El teorema de Gödel nun puede aplicase porque nun hai nengún procedimientu efectivu que decide si una cierta declaración ye un axoma. Ello ye que qu'esto sía asina ye una consecuencia del primer teorema de incompletud de Gödel.

Otru exemplu d'una especificación d'una teoría na que'l primera teorema de Gödel nun ye aplicable puede construyise de la siguiente manera: ordenemos toles posibles declaraciones sobre los númberos naturales primeru pol so llargor y depués en orde lexicográficu; empecemos con un sistema axomáticu primeramente igual a los axomes de Peano, repasemos la llista de declaraciones una a una, y, si la declaración actual nun puede demostrase nin refutar a partir del actual sistema d'axomes, entós añadámosla a la llista.
Esto crea un sistema que ye completu, consistente y abondo potente, pero non recursivamente enumerable.

El mesmu Gödel namái demostró una versión de los teoremes enriba espuestos que ye téunicamente un pocu más débil; la primer demostración de les versiones descrites enriba foi dada por J. Barkley Rosser en 1936.

N'esencia, la prueba del primer teorema consiste en construyir una declaración p dientro d'un sistema formal axomáticu al que se-y puede dar la siguiente interpretación meta matemática:

:p = «Esta declaración nun puede probase.»

Como tal, puede trate como una versión moderna de la paradoxa del mentirosu. Al contrariu de la declaración del mentirosu, p nun se refier direutamente a sigo mesmu; la interpretación de riba namái se puede "ver" dende fora del sistema formal.

Nun trabayu publicáu en 1957 en *Journal of Symbolic Logic*, Raymond Smullyan amosó que los resultaos de incompletitud de Gödel pueden llograse pa sistemes muncho más elementales que los consideraos por Gödel. Smullyan tamién reivindicó les pruebes más simples col mesmu algame, basaes nos trabayos d'Alfred Tarski sobre'l conceutu de verdá nos sistemes formales. Más simples, pero non menos perturbadoras filosóficamente. Smullyan nun afiguró les sos reflexones sobre incompletitud namái n'obres téuniques; tamién inspiraron célebres llibros de divulgación como *¿Cómo se llama esti llibru?* 

Si'l sistema axomáticu ye consistente, la prueba de Gödel amuesa que p (y la so negación) non pueden demostrase nel sistema.
Por tanto p ye *ciertu* (p afirma nun ser demostrable y nun lo ye) y, sicasí, nun puede probase formalmente nel sistema.
Afítese qu'añader p a los axomes del sistema nun resolvería'l problema: habría otra sentencia de Gödel pa la teoría ampliada.

Roger Penrose afirma qu'esta (presunta) diferencia ente *lo que puede probase mecánicamente* y *lo que los humanos pueden ver como ciertu* amuesa que la intelixencia humana nun ye mecánica na so naturaleza. Tamién John R. Lucas ocupóse d'esta cuestión en *Mentes, Máquines y Gödel*.

Esta perspeutiva nun ta llargamente aceptada, porque tal que lo plantega Marvin Minsky, la intelixencia humana ye capaz d'errar y de *entender* declaraciones que son en realidá inconsistentes o falses. Sicasí, Minsky informó de que Kurt Gödel díxo-y a él en persona qu'él creía que los seres humanos tienen una forma intuitiva, non solamente computacional, de llegar a la verdá y por tanto'l so teorema nun llinda lo que puede aportar a sabíu como ciertu polos humanos.

Veanse **Refutaciones a la interpretación de Penrose** nos *Enllaces n'Inglés* de la seición *Enllaces esternos y referencies*

La posición de que'l teorema amuesa que los humanos tienen una habilidá que transciende la lóxica formal tamién puede criticase de la siguiente manera: Nun sabemos si la sentencia p ye cierta o non, porque nun sabemos (nin podemos saber) si'l sistema ye consistente.
De cuenta qu'en realidá nun sabemos nenguna verdá que tea fuera del sistema.
Tou lo que sabemos ye lo siguiente:

:O p ye indemostrable dientro del sistema, o'l sistema ye inconsistente.

Esta declaración ye fácilmente demostrable *dientro del sistema*.

**Otra implicación** ye que'l trabayu de Gödel motivó a Alan Turing (1912-1954) a estudiar qué funciones yeren susceptibles de poder ser calculaes y cuálos non. Pa ello sirvióse del so Máquina de Turing, una máquina de propósitu xeneral por aciu la que formalizó les funciones y procedimientos de cálculu. Demostrando qu'esistíen funciones que nun son posibles de calcular por aciu la Máquina de Turing. El paradigma d'esti conxuntu de funciones representar la función qu'establez "si dada una Máquina de Turing, ésta produz un resultáu o, otra manera, quédase calculando indefinidamente". Esta función, conocida col nome de Problema de parada (Halting Problem), va ser pieza fundamental pa demostrar la incomputabilidad de ciertes funciones.

## Demostración de los teoremes
La demostración de los teoremes d'incompletitú basar en tres conceptos:
#La numberación de Gödel, que dexa traducir les teoríes formales a operaciones d'aritmética pura.
#La potencia espresiva de les teoríes formales aritmétiques, que les sos espresiones recueyen diches operaciones.
#El lema diagonal, que dexa que les fórmules sían autorreferentes.
L'enunciáu orixinal por cuenta de Gödel, que la so demostración esbozar nesta seición, ye más débil que'l presentáu enriba, yá qu'en llugar de la consistencia de la teoría *T* esíxese una propiedá más fuerte, la ω-consistencia.

(Los **numberales**  son los símbolos qu'utilice'l llinguaxe de la teoría pa especificar los númberos naturales concretos. Nel exemplu de l'aritmética de Peano na seición siguiente, los numberales son los símbolos daos por: , , , etc.) 
La consistencia implica la consistencia (pero non al aviesu). L'enunciáu fuerte», nel que namái se riquir la consistencia de la teoría foi probáu por J. B. Rosser por aciu un métodu bien similar.

### Numberación de Gödel

La numberación de Gödel ye una ferramienta que dexa rellacionar les teoríes formales cola aritmética. El llinguaxe d'una teoría formal de primer orde ta compuestu por una cantidá —a lo sumo— numerable de signos, como por casu:

: ,  ,  , , ,  ,  ,  , ... ,  ,  ,  ,  

nel casu del llinguaxe de l'aritmética de Peano, onde amás de los símbolos lóxicos y les variables, apaecen dellos símbolos adicionales pa la arimética (onde  ye'l símbolu pa denotar «el númberu siguiente a»). Tamién el conxuntu de toles cadenes (socesiones finitas de signos) ye numerable, según el conxuntu de les socesiones finitas de cadenes. 

Una **numberación de Gödel** ye una asignación d'un únicu númberu natural pa cada elementu de cada unu d'estos trés conxuntos: signos, cadenes de signos y socesiones de cadenes.

Yá que la manipulación d'estos signos, cadenes y socesiones puede traducise en manipulación d'unos ciertos númberos, tantu la sintaxis qu'estrema les cadenes de signos «con sentíu» —les fórmules− como'l cálculu deductivu qu'estrema les socesiones de cadenes «que demuestren daqué» —les demostraciones— vense traducíes a operaciones *aritmétiques*. Esto ye, esisten una serie de rellaciones y funciones aritmétiques que se correspuenden coles regles sintáctiques y del cálculu deductivu, como por casu:

: :  ye (el númberu de Gödel de) un signu : :  ye (el númberu de Gödel de) una cadena (de signos)
:(Omítese «el númberu de Gödel de» d'equí p'arriba)
: :  ye una socesión (de cadenes)
: : la cadena  ye una fórmula : : la fórmula  ye un axoma :: « ye una fórmula consecuencia inmediata de les fórmules  y »
:: «la socesión  ye una demostración de la fórmula »

La forma precisa d'estes funciones y rellaciones ye aballadora y depende del criteriu que s'escoyera pa efectuar la numberación de Gödel. En particular la rellación  hai de construyise teniendo en cuenta un ciertu conxuntu d'axomes concretu, depués la rellación  fai referencia a una teoría concreta que nun s'especificó.

.

### Expresabilidad. Recursividad

Por aciu la numberación de Gödel, ye posible «traducir» los signos y regles d'una teoría formal  en númberos y operaciones aritmétiques. Ye posible dir más allá, yá que  ye una teoría *aritmética* y puédense «recodificar» les mentaes operaciones por aciu el llinguaxe formal de , al igual que puede faese con otres funciones y rellaciones aritmétiques como por casu:

:La función «multiplicar por 2» ta representada pola fórmula: 
:La rellación d'orde , puede espresase por aciu:  
:La rellación « y  son primos ente sigo» puede espresase como: .

Caúna d'estes rellaciones ye *espresada* pola so fórmula correspondiente, nel sentíu de que si dos númberos tán rellacionaos, puede demostrase la espresión formal correspondiente; y cuando nun lo tán, puede refutarse. Por casu:

:Pa cada enteru , tiense que si  ye par puede probase la espresión formal ; y si ye impar, puede refutarse dicha fórmula.
:Pa cada par d'enteros  y , si tiense  puede demostrase la fórmula ; cuando , puede refutarse dicha espresión.

Que les rellaciones presentaes na seición anterior —como — sían expresables, implica qu'una teoría formal aritmética ye lo suficientemente potente como pa «falar» de les carauterístiques d'una teoría formal arbitraria ysobremanera, de sigo mesma.

Probar que toes estes rellaciones y funciones son expresables ye senciellu si son ''recursivas'', esto ye, si pueden calculase o verificase por aciu un algoritmu, yá que puede demostrase que toa rellación recursiva ye expresable nuna teoría aritmética. Les teoríes formales pa les qu'esto ye posible —asignar los númberos de Gödel de manera qu'estremar los signos, cadenes, socesiones, fórmules, consecuencies y axomes, puede llevase a cabu con un algoritmu— son les llamaes teoríes **recursivas**, y por ello esta carauterística asumir como hipótesis nos teoremes d'incompletitú.

### Diagonalización
Pa construyir la sentencia autorreferente  hai d'escurrise una manera por que una fórmula fale de les propiedaes del so númberu de Gödel correspondiente. Esto hai de faese de manera indireuta, yá que dada una fórmula  con númberu de Gödel , otra fórmula que «fale» de  por aciu el numberal  polo xeneral va tener un númberu de Gödel mayor que , y por tanto nun puede ser la mesma . Esto consíguese por aciu el llamáu **lema diagonal**.

A última hora, dada una propiedá cualesquier  esiste una sentencia  qu'afirma «el mio númberu de Gödel cumple la propiedá ».

### Demostración del primer teorema
Sía una teoría formal aritmética y recursiva  ω-consistente. Sía la fórmula , onde  ye la fórmula qu'espresa la rellación numbérica  —relativa a la teoría formal —. Pol lema de diagonalización esiste una sentencia  con númberu de Gödel , pa la que se demuestra , esto ye, qu'afirma «nengún númberu codifica una demostración (en ) de la fórmula representada por », o otra manera, «nun soi demostrable (en )». La negación d'esta sentencia, , ye equivalente a , o «la mio negación ye demostrable (en )».

Supóngase entós que  puede demostrase. Entós esiste un númberu  que cumple , y en  puede probase entós , lo cual implica formalmente ; y esto ye imposible si  ye consistente. Por tantu nun esiste una demostración de , y cumplir  pa tolos númberos , lo cual resulta nun númberu infinitu de teoremes formales  pa cada numberal . Como  ye ω-consistente, nun puede asoceder entós que  sía un teorema, polo que  ye indemostrable, y  ye indecidible.

### Demostración del segundu teorema
La demostración del segundu teorema de incompletitud rique d'un fechu téunicu que Gödel orixinalmente nun probó. Sía una teoría  nes condiciones anteriores y sía la fórmula , onde  ye'l númberu de Gödel de la sentencia .  afirma que la teoría  ye consistente (pos dexa daqué ensin demostrar). La versión formal (de la primer parte) del primer teorema de incompletitud puede espresase como  y esto ye equivalente precisamente a . De cuenta que, de poder probar formalmente esta sentencia,  sería indemostrable yá que se tendría entós una demostración de , en contradicción col primer teorema.

El fechu téunicu que se precisa ye precisamente una prueba de que la demostración del primer teorema de incompletitud puede «traducise» nuna demostración formal de la sentencia . Esto ye posible en toa teoría aritmética recursiva, yá que verifiquen unes ciertes *condiciones de demostrabilidad*.

## Ver tamién
* Consistencia lóxica
* Autorreferencia
* Loxicismu
* Teorema de Löb
* Teorema de completitud de Gödel
* Sobre proposiciones formalmente indecidibles de Principia Mathematica y sistemes rellacionaos

## Referencies

## Bibliografía
*
*.
*
*  
:Traducíu al castellán en: 
*
*
*
*
*.
*
* 
*

## Enllaces esternos
* **Refutaciones a la interpretación de Penrose:**
** *[http://cs.nyu.edu/cs/faculty/davism/penrose.ps Is Mathematical Insight Algorithmic?]*
** *[http://cs.nyu.edu/cs/faculty/davism/penrose2.ps How Subtle is Gödel's Theorem]*
** *[http://citeseer.ist.psu.edu/laforte98why.html Why Gödel's Theorem Cannot Refute Computationalism]*
** *[http://citeseer.ist.psu.edu/106920.html Human and Machine Understanding of Mathematics]*
* Ignacio Jané, *[http://divulgamat.ehu.es/weborriak/historia/Gaceta/historia93b.pdf La obra de Gödel en lóxica matemática y teoría de conxuntos] * Una introducción sintética y histórica que respeta los conceutos orixinales, evitando tracamundios. 
* Reseña en castellán de Torkel Franzén, *Gödel's theorem : an incomplete guide to its use and abuse*. El llibru de Franzen, de 2005, ta siendo bien citáu como obra d'interés pa introducir al verdaderu sentíu de los teoremes de Gödel y prevenir frente a la so aplicación inxustificada en campos non matemáticos.
* Kārlis Podnieks: *Around Goedel's Theorem*, http://www.ltn.lv/~podnieks/gt.html
* Hilbert's second problem
*  Primer demostración del teorema de completitud.
*