Gödelen ez-osotasunaren teoremak

Gödelen ez-osotasunaren teoremak logika matematikoaren bi teorema dira, teoria axiomatiko formalen frogagarritasun mugei buruzkoak. Emaitza hauek, Kurt Gödel-ek 1931. urtean argitaratuak, garrantzitsuak dira logika matematikoan zein matematikaren filosofian. Zabal onartzen da, unibertsalki onartzen ez bada ere, teorema hauek Hilberten programa ezinezkoa dela frogatzen dutela. Hots, ezinezkoa dela matematika guztietarako axioma multzo oso eta koherente bat aurkitzea.

Lehenengo ez-osotasunaren teoremak dioenez, ez dago axiomen sistema koherente bat bera ere prozedura eraginkorraren bidez (hau da, algoritmo baten bidez) sistemaren teoremak zerrenda ditzakeena eta gai dena zenbaki naturalen aritmetikari buruzko egia guztiak frogatzeko. Hots, zenbaki arrunten aritmetikaren axiomak barnebiltzen dituzten sistema formal koherenteetan, beti izango dira zenbaki arruntei buruzko esakune egiazkoak, baina sistemaren barruan frogaezinak direnak. Bigarren ez-osotasunaren teorema, lehenengoaren ondorioa da, eta sistemak ezin duela bere koherentzia propioa frogatu azaltzen du.

 Sintesia 
Ez-osotasunaren lehen teoremak dio ezen, zenbait baldintzatan, zenbaki naturalak eta aritmetika adierazkortasun nahikoarekin deskribatzeko gai den teoria matematiko formalik ez dela, aldi berean, kontsistentea eta osoa. Hau da, teoria horren axiomak elkarren artean kontrajartzen ez badira, zenbait enuntziatu ezin dira frogatu edo gezurtatu. Zehazki, teoremaren ondorioa aplikatzen da baldin eta kasuan kasuko teoria aritmetikoa errepikakorra bada, hau da, dedukzio-prozesua algoritmo baten bidez egin ahal bada.

Teoremaren proba guztiz esplizitua da, eta bertan formula bat eraikitzen da, Gödelen omenez G letrarekin adierazi ohi dena. Horren froga bat emanda, gezurtapen bat eraiki daiteke, eta alderantziz. Hala ere, epai horren interpretazio naturala zenbaki arruntei dagokienez benetakoa da.
Ez-osotasunaren bigarren teorema lehenengoaren kasu berezi bat da: teoria horren epai erabakiezinetako batek teoria horren sendotasuna «berresten» duela dio. Hau da, axioma-sistema trinkoa bada, ezin da frogatu axioma horien bidez.

Gödelen ez-osotasunaren teoremak matematika-logikaren aurrerapen handienetako bat dira, eta, matematika-komunitatearen gehiengoaren arabera, Hilbert-en bigarren problemari erantzun negatiboa eman zioten. Teoremen arabera, lehen mailako sistema axiomatikoek muga zorrotzak dituzte matematika oinarritzeko, eta kolpe gogorra izan ziren Hilberten programa deiturikoarentzat, matematika oinarritzeko helburua zuena. Bestalde, denboraldi batez, ez Hilbert ez haren laguntzaileetako beste batzuk ez ziren ohartu Gödelek bere programarako egindako lanak zuen garrantziaz.

 Testuingurua 
Gödelen ez-osotasunaren teoremek zenbait muga ezartzen dituzte arrazoibide matematiko baten bidez froga daitekeenari buruz. Zer «froga daitekeen» edo ez zehazki aipatu ahal izateko, teoria formal izeneko eredu matematiko bat aztertzen da. Teoria formal batek zeinu batzuk eta horiek manipulatu eta konbinatzeko arau multzo bat ditu. Arau horien bidez, zenbait zeinu-bilduma bereiz daitezke, hala nola formulak, eta zenbait formula-segida demostrazioak eratzen zituztenak. Halako teoria baten teoremak axioma gisa hartzen diren formulen hasierako bilduma batetik abiatuta froga daitezkeen formula guztiak dira.

Teoria formal bati zenbait propietate eslei dakizkioke frogatzeko gai denaren arabera. 

 Teoria sendo batek ez du kontraesanik, hau da, ezin da aldi berean formula bat eta haren kontrakoa frogatu. Sendoa ez den teoria batek ez du erabilgarritasunik: eztanda-printzipioa dela eta, kontraesan batetik abiatuta froga daitezke haren formula guztiak, eta ez du balio arrazonamendu matematikoak modelizatzeko.
 Teoria oso batek «edozein galderari erantzuten dio», hau da, bere formula bakoitzerako froga daiteke, edo bere kontrakoaren froga bat dago (gezurtagarria da). Teoria oso bat optimoa da, eta bat dator egia logikoari buruzko intuizioarekin: epai orok egiazkoa edo faltsua izan behar duen bezala, teoria oso batean formula oro frogagarria edo gezurtagarria da.

Hala ere, ez-osotasunaren lehen teoremak ezartzen du ezen, hipotesi batzuen pean, teoria formal batek ezin dituela bi propietateak batera izan. Lehena teoria aritmetikoa izatea da, hau da, haren sinboloek zenbaki arruntak eta haien eragiketak eta erlazioak deskribatzeko balio izatea; eta horien gaineko oinarrizko propietate batzuk frogatzeko gai izatea. Bigarren hipotesia teoria errekurtsiboa izatea da, eta horrek esan nahi du bere zeinuak eta formulak demostrazioetan manipulatzeko arauak algoritmo baten bidez gauzatu behar direla: anbiguotasunik gabeko urratsen serie zehatz bat, denbora jakin batean egin daitekeena, eta programa informatiko baten bidez ere ezarri ahal izango dena.

 Lehen teorema 
Lehenengo teoremaren enuntziatuak hau dio:Teorema hori frogatzeko, formula jakin bat eraiki behar da, «ödelen  esaldia», ezin dena ez frogatu ez ezeztatu T teoria aritmetiko errekurtsiboarekin: ez G ez  (Gren ukapena zena) ez dira Tren teoremak. Esaten da, orduan, bai G bai  erabakiezinak edo independenteak direla T-n.

Horretara iristeko, zeinuak eta formulak zenbakien bidez kodetzeko metodo bat garatu zuen, Gödelen numerazioa izenekoa. Numerazio hori erabiliz, T teoria formal baten propietateak itzul daitezke, hala nola «zeinu horiek formula bat osatzen dute» edo «formula horiek ez dira T-n erakusten», zenbaki horien propietate aritmetikoetara. Zehazki, Gödel G-ren esaldia formula aritmetiko bat da, eta horren esanahia da «T teorian ez dago G-ren frogarik», edo bestela esanda, «T teorian ezin naiz frogatua izan».

 Ondorioak 
Gödel G-ren esaldia ez da frogagarria, baina egia da, hain zuzen ere, bere frogagarritasun eza adierazten baitu.Esto solo es cierto en la interpretación natural en que las variables de la teoría se interpretan como los números naturales. Horrek esan nahi du teoremaren baldintzetan teoria aritmetikorik ez dela gai aritmetikaren egiazko enuntziatu guztiak frogatzeko.

Gainera, nahiz eta aldi  faltsua izan (G-ren kontrakoa esateagatik) ezin da ezeztatu (G frogaezina delako). Nahi izanez gero, esaldi hori axioma gisa har daiteke, eta horrek ez du kontraesanik sortzen. Ondoriozko teoriak zenbaki arruntei eta faltsu batzuei buruzko egiazko enuntziatu asko ditu,  esalditik hasita. Teoria batek deskribatzen dituen objektuek aritmetikaren eredu ez-estandarra osatzen dute.Véase  para una exposición de nivel intermedio sobre la aritmética no estándar.

G (edo haren kontrakoa) axioma gisaa hartuta, T' teoria berri bat lortzen da, non G (edo haren aurkakoa) automatikoki froga baitaiteke. Hala ere, horrek ez du teorema baliogabetzen, G-k T teoriari dagokionez duen atzeraezintasuna baieztatzen baitu. T teoria berria ere osatugabea da: G' epai independente bat aurki daiteke, «T'n ezin naizela frogatu» dioena.

Azken batean, teoria formal sendo eta oso batean, hipotesiren batek huts egin behar du: edo ez da errepikakorra, eta ez dago algoritmorik axiomak gainerako formuletatik bereizteko; edo ez dira aritmetikoak, eta ez dituzte sartzen zenbaki arrunten oinarrizko propietateak. Adibidez, osotasun semantikoaren teorema frogatzeko teoria sendoak eta osoak erabiltzen dira, eta ez dira errepikakorrak. Bestalde, Presburgerren aritmetika zenbaki arruntei buruzko axioma-bilduma bat da, zenbait propietate kanpo uzten dituena, halako moldez non haietan oinarritutako teoria bat trinkoa eta osoa izan baitaiteke.

 Bigarren teorema 
Osotasun ezaren bigarren teoremak teoria aritmetiko bakar batek ere froga ezin dezakeen formula baten beste adibide esplizitu bat erakusten du, Gz gain. Berriz ere, Gödelen numerazioa erabiliz, formula bat aurki daiteke, Consis T deritzona, zeinaren esanahia den «ezin da kontraesan bat aurkitu T-n», edo bestela esanda, «T sendoa da».Bigarren teorema frogatzeko, lehenengoa formula batera itzuli behar da. Lehenengo teoremak dio, besteak beste, T sendoa bada, orduan G ezin dela frogatu. T-ren sendotasuna baieztatzen duen formula Consis T da, eta -ren frogapenaren ezintasuna baieztatzen duen formula, berriz, G. Lehenengo teorema itzultzen duen formula (teoremaren zati bat)  da, non «» zeinuak inplikazioa adierazten duen. Gödel-ek frogatu zuen formula hori teorema bat dela, eta, beraz, Consis T ez dela teorema bat: hala balitz, T teoriaren oinarrizko arauetatik ondorioztatuko litzateke G froga daitekeela, osotasun ezaren lehen teoremaren enuntziatuarekin kontraesanean.En realidad, la prueba original de Gödel omite ciertos detalles técnicos.

 Ondorioak 
Ez-osotasunaren bigarren teoremak T teoria formal baten sendotasuna frogatzeko aukerak mugatzen ditu, ezin baita T bera bakarrik erabiliz egin. Gainera, T' teoria indartsuago bat aurkitzen bada, non Consis T froga baitaiteke, T'-ren tinkotasuna bera ezingo da frogatu T'-n, ezta T -n ere. Hori dela eta, bigarren teoremak kontsideratzen du Hilberten problemaren erantzuna negatiboa dela. Problema horrek objektu infinituen arrazonamendu matematikoen zuzentasuna demostratu nahi zuen soilik objektu finitutan oinarrituta, potentzia txikiagoa zutenak.

 Eztabaida eta ondorioak 
Ez-osotasuaren emaitzek matematikaren filosofiari eragiten diote, batez ere formalismoa bezalako ikuspuntuei, zeinak logika formala erabiltzen baitu bere printzipioak definitzeko.

Lehenengo teorema parafraseatu egin daiteke, esanez «inoiz ezingo dela aurkitu egia matematiko guztiak eta gezurrik ez frogatzeko gai den sistema axiomatikorik».

Bestalde, ikuspegi hertsiki formalistatik, parafrasi hori esanahirik gabekotzat hartuko litzateke, zeren eta aurresuposatzen baitu matematika-«egia» eta «faltsukeria» ondo definituta daudela zentzu absolutuan, sistema formal bakoitzari buruzkoak izan beharrean.

Bigarren teoremaren ondorengo birformulazioa are kezkagarriagoa da matematikaren oinarrietarako:

 Sistema axiomatiko bat berez sendoa dela froga badaiteke, orduan ez da sendoa.

Printzipioz, Gödel-en teoremek oraindik itxaropen pixka bat uzten dute: posible izan liteke algoritmo orokor bat sortzea, baieztapen jakin bat erabakiezina den ala ez zehaztuko duena, eta matematikariei arazo erabakiezinak erabat saihesteko aukera emango diena. Hala ere, Entscheidungsproblemari emandako erantzun negatiboak erakusten du algoritmo hori ez dagoela.

 Erreferentziak 

 Kanpo estekak 

Kategoria:1931 zientzian
Kategoria:Matematikaren oinarriei buruzko teoremak
Kategoria:Logika matematikoa
Kategoria:Modeloen teoria
Kategoria:Frogaren teoria
Kategoria:Epistemologia
Kategoria:Metateoremak