Teoria axiomatică

Când vorbim despre teoria matematică , ne referim la o sumă de enunțuri, definiții, metode de probă etc. Teoria calculabilitate este un exemplu. Prin teorie axiomatică , ne referim la ceva mai precis, axiome și consecințele lor, teoreme , enunțate într-un limbaj precis. În cele ce urmează vom spune cel mai adesea teoria pentru teoria axiomatică, care este folosită în mod obișnuit în logica matematică .

Desigur, există o relație între cele două noțiuni. Dar putem vedea că ar fi foarte simplist să definim teoria grupurilor ca trei axiome și consecințele lor.

Acest articol nu este destinat să discute sensul cuvântului „ teorie ” în afara contextului matematicii și chiar al matematicii formale.

Cele Elementele de Euclid sunt considerate ca primul exemplu al teoriei axiomatice, cu toate că unii au rămas axiome implicite. Noțiunea modernă a teoriei axiomatice dezvoltate în timpul XIX - lea secol și începutul XX - lea secol, în primul rând datorită descoperirii în XVII - lea secol de calcul , care a necesitat alte fundatii matematicii cele ale lui Euclid Elemente , pe de o parte din cauza celeilalte dezvoltarea geometriei și a algebrei moderne (vezi și programul lui Erlangen ).

Definiții

Când vrem să definim cu precizie această noțiune în logica matematică , în primul rând definim cu precizie limbajul teoriei : de exemplu un limbaj de ordinul întâi .

Potrivit autorilor, termenul „teorie” denotă:

orice set de enunțuri (formule închise, adică fără variabilă gratuită ) ale limbajului considerat;
sau un set de enunțuri închise prin deducție în logica considerată, fără mai multă precizie este vorba despre logica clasică .

În primul caz, cuvântul „teorie” se referă la un set de axiome ale teoriei. În al doilea, el se referă la teoremele teoriei.

O alegere imediată, deși greu interesantă, ar fi luarea tuturor teoremelor ca axiome; există deci întotdeauna un sistem de axiome pentru o teorie dată (în sensul închis prin deducție) și există chiar în mod necesar mai multe sisteme posibile de axiome pentru o teorie dată. Practic, indiferent de definiția utilizată, contextul face posibilă eliminarea ambiguităților.

Această noțiune foarte extinsă de teorie este cea utilizată în logica matematică, în special în teoria modelelor . Astfel, setul de enunțuri în limbajul aritmeticii, adevărat în numerele întregi obișnuite, este evident închis prin deducție. Dar, după cum putem deduce imediat din prima teoremă a incompletitudinii lui Gödel , nu există nicio modalitate de a oferi un sistem de axiome pentru această teorie, un mijloc care poate fi folosit în practica matematică, deoarece pentru aceasta este cel puțin, ar fi necesar pentru a putea recunoaște „fără prea mult efort” (înțelegem mecanic) o axiomă dintre enunțurile limbajului teoretic.

Prin urmare, suntem conduși să introducem o noțiune mai precisă, noțiunea de teorie recursiv axiomatizabilă (a se vedea restul acestui articol), care este, de altfel, o condiție prealabilă pentru enunțarea teoremei Gödel pe care tocmai am menționat-o.

Se spune că o teorie este coerentă , sau într-un mod echivalent non-contradictoriu sau chiar consecvent , atunci când există afirmații ale teoriei care nu pot fi dovedite. Aceasta înseamnă a spune, în orice caz, în logica clasică sau intuiționistă , că nu se poate demonstra o contradicție. În calculul predicat clasic de ordinul întâi , o teorie este consecventă dacă și numai dacă are un model : aceasta este teorema completitudinii . Teoriile utilizate în matematică ar trebui să fie coerente, chiar dacă, de îndată ce aceste teorii permit să dezvolte suficientă aritmetică, nu poate exista nicio demonstrație a acestei coerențe fără a presupune coerența unei teorii mai puternice, așa cum o arată cea de- a doua . teorema .

În cele ce urmează, vom considera că teoriile sunt teorii de ordinul întâi ale logicii clasice , chiar dacă de fapt majoritatea conceptelor menționate au un sens în logica intuiționistă , în logica de ordin superior etc.

Teorie recursiv axiomatizabilă

O teorie recursiv axiomatizabilă este o teorie care poate fi axiomatizată în așa fel încât este posibil să se recunoască într-un mod pur mecanic axiomele dintre enunțurile limbajului teoriei. Acesta este cazul cu teoriile utilizate pentru a formaliza total sau parțial matematica obișnuită, cum ar fi aritmetica Peano sau teoria mulțimilor Zermelo-Fraenkel .

Intuitiv, am cere chiar și mai mult sistemelor de axiome: trebuie să putem verifica „fără să ne gândim” că o anumită afirmație este o axiomă. Aceasta este ceea ce captăm imperfect, spunând că această verificare este mecanică, adică am putea să o încredințăm unei mașini, unui computer. Un computer este capabil de verificări care nu sunt imediate pentru o ființă umană, cu atât mai mult dacă computerul este pur teoretic, cum ar fi mașina Turing , care este utilizată pentru a formaliza aceste noțiuni. De exemplu, geometria euclidiană, în formalizarea sa de primă ordine, este decisivă, ceea ce înseamnă că setul teoremelor sale este un sistem recursiv de axiome, deși este clar inutilizabil pentru axiomatiza cu adevărat geometria, dată fiind complexitatea procedurii deciziei. Dar această noțiune este bine formalizată, este cea care este potrivită pentru teoremele incompletitudinii sau indecizibilității .

O condiție este că enunțurile de limbaj ale teoriei în sine pot fi recunoscute mecanic, se spune că limbajul este recursiv . Se înțelege bine că acesta este cazul când simbolurile specifice ale limbajului (uneori numite semnătura limbii): simbolul constantelor, al funcției sau al operației, al predicatului sau al relației, sunt finite ca număr. De exemplu, aritmetica lui Peano folosește, în afară de vocabularul pur logic (inclusiv egalitatea), simboluri și, eventual, care sunt într-adevăr în număr finit. De asemenea, putem construi limbaje recursive cu semnătură infinită. $0, s, +, \ ori$ $\ leq$

Un caz particular evident al teoriei recursiv axiomatizabile este cel al teoriilor finit axiomatizabile , adică teorii pentru care putem da un număr finit de axiome. Astfel teoria grupurilor, teoria corpurilor sunt finit axiomatizabile.

Unele teorii au un număr infinit de axiome, dar acestea sunt descrise într-un mod finit, vorbim apoi de o schemă de axiome . De exemplu , aritmetica lui Peano , o teorie de primul ordin, afirmă recurența ca o schemă a axiomelor: avem nevoie de o axiomă pentru fiecare formulă pentru care afirmăm recurența. Aritmetica lui Peano este deci dată de o infinitate de axiome, dar putem vedea clar că vom putea recunoaște mecanic enunțurile care exprimă recurența dintre enunțurile limbajului.

Toate acestea sunt formalizate riguros prin codificarea formulelor limbajului prin numere întregi și prin utilizarea teoriei calculabilității . Odată ce enunțurile sunt codificate de numere întregi, spunem că un set de enunțuri este recursiv dacă funcția caracteristică a codurilor acestor afirmații este o funcție calculabilă . O teorie recursiv axiomatizabilă este deci o teorie care are un sistem recursiv de axiome.

De asemenea, este posibil să se definească aceste noțiuni fără a trece prin codări întregi, folosind teoria limbajelor formale. Se pare că aceste noțiuni sunt adesea utile într - un context ( teorema lui Gödel incompletitudine , teorema lui Church ) , în cazul în care trebuie să ne cod aritmetic formulele oricum.

Teoreme ale unei teorii recursiv axiomatizabile

În matematică, suntem de acord că putem recunoaște fără a întinde imaginația că „ceva”, spunem o serie de propoziții, este o dovadă. Deoarece aceasta este o dovadă formală, trebuie să fie posibil să se verifice etapele pas cu pas mecanic. Având în vedere definiția noastră a teoriei, o condiție necesară pentru ca acest lucru să fie adevărat este ca teoria să fie recursiv axiomatizabilă. Dacă examinăm orice sistem formal pentru logică, de exemplu un sistem à la Hilbert sau calculul secvențelor , ne convingem că această condiție este suficientă: astfel, putem verifica într-un mod pur mecanic că o formulă poate fi dedusă din două formule de modus ponens . Aici, din nou, formalizăm acest lucru riguros, codificând dovezile prin numere întregi și folosind teoria calculabilității și arătăm că

într-o teorie recursiv axiomatizabilă, „a fi o dovadă” este decisiv .

Deducem din acest rezultat că putem enumera mecanic teoremele unei teorii recursiv axiomatizabile. Cu alte cuvinte, putem construi o mașină teoretică, care va funcționa la nesfârșit și va oferi una câte una toate teoremele teoriei. Mai formal,

ansamblul teoremelor unei teorii recursiv axiomatizabile este recursiv enumerabil .

Acest lucru nu permite o verificare mecanică a faptului că o afirmație este o teoremă. Putem porni mașina, atâta timp cât nu obținem afirmația pe care încercăm să o demonstrăm, fără alte informații, nu știm dacă este pentru că mașina o va da mai târziu sau nu.

Să schițăm o dovadă informală a acestui rezultat. Luați în considerare faptul că dovezile sunt scrise folosind un număr finit de litere. Toate literele trebuie să fie numărate: faceți două litere, trei litere etc. Mărimea unei dovezi este numărul de litere utilizate pentru a o scrie. Numărăm repetările și o dovadă poate fi de dimensiuni arbitrare mari, dar există doar un număr finit (posibil zero) de dovezi de o dimensiune dată. Se pot enumera astfel într-un mod mecanic dovezile prin enumerarea succesivă a tuturor celor de o dimensiune fixă, apoi a tuturor celor de o dimensiune strict mai mare și aceasta la nesfârșit. Deducem o enumerare mecanică a teoremelor: este suficient să citim concluzia probei de fiecare dată. Într-adevăr, nimic nu împiedică această enumerare să producă repetări (dar ar fi posibil să construim una care să le evite). Cu toate acestea, dacă rulăm mașina care enumeră teoremele, există puține șanse să găsim o teoremă interesantă pentru o perioadă foarte, foarte lungă de timp. $x_ {0}$ $x _ {{10}}$

De fapt, avem reciprocitatea rezultatului. Prin urmare, putem afirma

o teorie este recursiv axiomatizabilă dacă și numai dacă ansamblul teoremelor acestei teorii este recursiv enumerabil.

Construim un sistem de axiome decisiv pentru un set recursiv de teoreme enumerabile folosind un mic truc logic. Este

A_ {0}, \ A_ {1}, \ A_ {2}, \ \ dots \, \ A_ {n}, \ \ dots

secvența teoremelor enumerate de o mașină. Vom construi la fel de mecanic succesiunea conjuncțiilor succesive ale afirmațiilor acestei teorii, adică

{\ displaystyle A_ {0}, \ (A_ {0} \ land A_ {1}), \ (A_ {0} \ land A_ {1} \ land A_ {2}), \ \ dots \, \ (A_ {0} \ land A_ {1} \ land \ dots \ land A_ {n}), \ \ dots}

că alegem ca un nou sistem de axiome. Deoarece secvența de pornire este ansamblul teoremelor unei teorii și, prin urmare, este închisă prin deducție, am extras astfel o subsecvență infinită. Afirmațiile acestei secvențe axiomatizează în mod trivial teoria inițială. Succesiunea axiomelor obținute este enumerată într-un mod strict crescător ca mărime (de exemplu numărul de semne necesare pentru a scrie enunțul), deoarece fiecare axiomă este obținută prin completarea celei anterioare prin corelație cu o afirmație nouă. Pentru a ști dacă orice afirmație B este o axiomă, este suficient, prin urmare, să le enumerați până să găsiți fie afirmația B , și atunci este într-adevăr o axiomă, fie o afirmație de mărime strict mai mare, iar acest n nu este. Din punct de vedere tehnic, dacă formalizăm, vom folosi următorul rezultat de calculabilitate: setul de imagini al unei funcții recursive strict în creștere este un set recursiv .

Dovedim exact în același mod (deoarece închiderea prin deducție nu intervine în dovadă) că

o teorie care are un set recursiv de axiome enumerabile are un set recursiv de axiome.

și, prin urmare, noțiunea de teorie axiomatizabilă printr-un set recursiv de enumerabile de axiome nu este de mare interes (la fel de bine am putea lua direct toate teoremele).

Completitudine și decizie

Pentru teoriile recursiv axiomatizabile, putem stabili o legătură între noțiunea de decizie în sens logic . O afirmație este decisă dacă ea sau negarea acesteia este o teoremă, iar noțiunea de decidabilitate în sens algoritmic, un set este decisiv - sau recursiv - dacă putem decide mecanic să aparținem acestui set.

Spunem că o teorie este completă atunci când toate enunțurile limbajului teoriei sunt decisive în teorie, adică fiecare afirmație este o teoremă sau negația sa este o teoremă.

Spunem că o teorie este recursivă (spunem, de asemenea , decizibilă , dar vom evita acest lucru în cele ce urmează, deoarece acest lucru se pretează prea mult la ambiguitate în acest context), atunci când setul teoremelor sale este recursiv.

O teorie recursivă este evident recursiv axiomatizabilă: este suficient să luăm toate teoremele ca axiome. Se arată că există teorii recursiv axiomatizabile care nu sunt recursive, cum ar fi aritmetica Peano , dar și teorii mult mai simple, calculul predicatelor într-un limbaj suficient de bogat, precum cel al aritmeticii sau un limbaj cu cel puțin un simbol predicat binar (vezi teorema Bisericii ). Dar putem arăta că:

O teorie recursiv axiomatizabilă și completă este recursivă (adică decisă în sens algoritmic).

Să arătăm acest rezultat. Putem presupune că teoria este consecventă, deoarece ansamblul teoremelor unei teorii inconsistente este ansamblul tuturor formulelor închise, care este recursiv imediat ce limbajul teoriei este recursiv. Dacă o teorie este coerentă și completă, ansamblul afirmațiilor care nu sunt teoreme este ansamblul afirmațiilor a căror negație este o teoremă. Putem deduce foarte ușor că este și recursiv enumerabilă. Totuși, setul de enunțuri în limbajul teoriei este recursiv. Știm în teoria calculabilității că dacă o mulțime este recursiv enumerabilă și dacă complementul său dintr-un set recursiv este recursiv enumerabil, acest set este recursiv .

Să detaliați argumentul, adaptându-l la cazul nostru particular. Avem o mașină care enumeră teoremele teoriei, care ar trebui să fie coerentă. Vrem să știm dacă afirmația este o teoremă. Lansăm aparatul și comparăm în fiecare etapă afirmația produsă cu și cu negarea sa. Pe măsură ce teoria este completă, acest proces se încheie: ajungem să producem fie negarea sa. Tocmai am definit un proces mecanic care face posibil să știm dacă o afirmație dată este demonstrabilă (mașina a produs ) sau nu demonstrabilă (mașina a produs negarea , prin urmare, prin consistența teoriei, nu este demonstrabilă). Prin urmare, teoria este recursivă. $B$ $B$ $B$ $B$ $B$ $B$

Prin contrapunere, obținem imediat că o teorie recursiv axiomatizabilă care nu este recursivă nu poate fi completă. Prin urmare, putem demonstra foarte bine prima teoremă de incompletitudine a lui Gödel folosind acest rezultat (ca în referința bibliografică indicată).

Referințe

William Craig (în) observă acest lucru, iar generalizarea la seturi recursiv de axiome enumerabile în cele ce urmează este Axiomatizabilitatea în cadrul unui sistem , The Journal of Symbolic Logic , Vol. 18, nr. 1 (1953), pp. 30-32. Această „observație” este numită Teorema lui Craig de către filosofii conform (en) Hilary Putnam , „ Teorema lui Craig ” , The Journal of Philosophy , vol. 62, nr . 10,1965, p. 251-260. Metoda folosită de Craig pentru dovada este ușor diferită: a j- declarația - lea a secvenței originale se înlocuiește cu aceeași declarație repetată i ori.

Bibliografie

René Cori și Daniel Lascar , Logica matematică II . Funcții recursive, teorema lui Gödel, teoria mulțimilor, teoria modelelor [ detaliul edițiilor ]

Această lucrare prezintă rezultatele descrise aici, dar într-un mod mai riguros, fără apel implicit la teza Bisericii .

Vezi și tu