Sistem formal

Versiunea actuală a paginii nu a fost încă examinată de colaboratori experimentați și poate diferi semnificativ de versiunea revizuită la 31 august 2021; verificările necesită 3 modificări .

Un sistem formal ( teorie formală , teorie axiomatică , axiomatică , sistem deductiv ) este rezultatul unei formalizări stricte a teoriei , care presupune o abstracție completă din sensul cuvintelor limbajului folosit și din toate condițiile care guvernează utilizarea aceste cuvinte din teorie sunt enunțate în mod explicit prin axiome și reguli care permit derivarea unei fraze din altele [1] .

Un sistem formal este o colecție de obiecte abstracte care nu au legătură cu lumea exterioară, în care regulile de operare cu un set de simboluri sunt prezentate într-o interpretare strict sintactică fără a ține cont de conținutul semantic, adică de semantică. Sistemele formale strict descrise au apărut după ce a fost pusă problema Hilbert . Primul FS a apărut după publicarea cărților lui Russell și Whitehead „Formal Systems”[ specificați ] . Aceste FS au fost prezentate cu anumite cerințe.

Bazele

O teorie formală este considerată definită dacă [2] :

  1. Este dat un set finit sau numărabil de simboluri arbitrare. Secvențele finite de simboluri sunt numite expresii teorie .
  2. Există un subset de expresii numite formule .
  3. Un subset de formule, numit axiome , a fost evidențiat .
  4. Există un set finit de relații între formule, numite reguli de inferență .

Există de obicei o procedură eficientă care permite unei anumite expresii să determine dacă este o formulă. Adesea un set de formule este dat de o definiție inductivă . De regulă, acest set este infinit. Setul de simboluri și setul de formule definesc colectiv limbajul sau semnătura unei teorii formale.

Cel mai adesea, este posibil să se afle în mod eficient dacă o formulă dată este o axiomă; într-un astfel de caz, se spune că teoria este efectiv axiomatizată sau axiomatică . Setul de axiome poate fi finit sau infinit. Dacă numărul de axiome este finit, atunci se spune că teoria este axiomatizabilă finit . Dacă mulțimea de axiome este infinită, atunci, de regulă, se specifică folosind un număr finit de scheme de axiome și regulile pentru generarea de axiome specifice din schema de axiome. De obicei, axiomele sunt împărțite în două tipuri: axiome logice (comune pentru o întreagă clasă de teorii formale) și axiome non- logice sau proprii (care determină specificul și conținutul unei anumite teorii).

Pentru fiecare regulă de inferență R și pentru fiecare formulă A , întrebarea dacă setul ales de formule este în relație cu R cu formula A este rezolvată efectiv și, dacă da, atunci A se numește o consecință directă a acestor formule în conformitate cu rigla.

O derivare este orice succesiune de formule astfel încât orice formulă a secvenței este fie o axiomă, fie o consecință directă a unor formule anterioare conform uneia dintre regulile de derivare.

O formulă se numește teoremă dacă există o derivație în care această formulă este ultima.

O teorie pentru care există un algoritm eficient care vă permite să aflați dintr-o formulă dată dacă derivarea acesteia există se numește decidabilă ; în caz contrar, se spune că teoria este indecidabilă .

Se spune că o teorie în care nu toate formulele sunt teoreme este absolut consecventă .

Definiție și varietăți

O teorie deductivă este considerată dată dacă:

  1. Sunt date un alfabet ( set ) și reguli pentru formarea expresiilor ( cuvinte ) în acest alfabet.
  2. Sunt date regulile de formare a formulelor (expresii corecte, bine formate).
  3. Din setul de formule, o submulțime T de teoreme ( formule demonstrabile ) este selectată într-un fel.

Varietăți de teorii deductive

În funcție de metoda de construire a unui set de teoreme:

Specificarea axiomelor și a regulilor de inferență

În setul de formule, se evidențiază un subset de axiome și se specifică un număr finit de reguli de inferență - astfel de reguli cu ajutorul cărora (și numai cu ajutorul lor) pot fi formate noi teoreme din axiome și derivate anterior. teoreme. Toate axiomele sunt incluse și în numărul de teoreme. Uneori (de exemplu, în axiomatica lui Peano ), o teorie conține un număr infinit de axiome care sunt specificate folosind una sau mai multe scheme de axiome . Axiomele sunt uneori numite „definiții ascunse”. În acest fel, se specifică o teorie formală ( teorie axiomatică formală , calcul formal (logic) ).

Întrebând doar axiome

Sunt date doar axiome, regulile de inferență sunt considerate a fi bine cunoscute.

Cu o astfel de specificare a teoremelor, se spune că este dată o teorie axiomatică semi-formală . Exemple

Geometrie

Specificarea numai a regulilor de inferență

Nu există axiome (mulțimea de axiome este goală), sunt date doar reguli de inferență.

De fapt, teoria astfel definită este un caz special al celei formale, dar are propriul nume: teoria inferenței naturale .

Proprietățile teoriilor deductive

Consecvență

O teorie în care mulțimea de teoreme acoperă întregul set de formule (toate formulele sunt teoreme, „enunțuri adevărate”) se numește inconsistentă . În caz contrar, se spune că teoria este consecventă . Elucidarea inconsecvenței unei teorii este una dintre cele mai importante și uneori cele mai dificile sarcini ale logicii formale.

Completitudine

O teorie se numește completă dacă în ea pentru orice propoziție (formulă închisă) fie ea însăși, fie negația ei este derivabilă . În caz contrar, teoria conține afirmații nedemonstrabile (afirmații care nu pot fi nici dovedite, nici infirmate prin intermediul teoriei în sine) și se numește incomplete .

Independenta axiomelor

Se spune că o axiomă individuală a unei teorii este independentă dacă axioma respectivă nu poate fi dedusă din restul axiomelor. Axioma dependentă este în esență redundantă, iar eliminarea ei din sistemul de axiome nu va afecta în niciun fel teoria. Întregul sistem de axiome ale unei teorii este numit independent dacă fiecare axiomă din el este independentă.

Rezolvabilitate

O teorie se numește decidabilă dacă conceptul de teoremă este eficient în ea , adică există un proces eficient (algoritm) care permite oricărei formule să determine într-un număr finit de pași dacă este sau nu o teoremă.

Rezultate cheie

  • În anii 30. În secolul al XX-lea, Kurt Gödel a arătat că există o întreagă clasă de teorii de ordinul întâi care sunt incomplete. În plus, formula care afirmă consistența unei teorii este, de asemenea, nederivabilă prin intermediul teoriei în sine (vezi teoremele de incompletitudine ale lui Gödel ). Această concluzie a fost de mare importanță pentru matematică, deoarece aritmetica formală (și orice teorie care o conține ca subteorie) este doar o astfel de teorie de ordinul întâi și, prin urmare, incompletă.
  • În ciuda acestui fapt, teoria câmpurilor reale închise cu adunare, înmulțire și relație de ordine este completă ( teorema Tarski-Seidenberg ).
  • Alonzo Church a demonstrat că problema determinării validității oricărei formule logice a predicatelor arbitrare este algoritmic indecidabilă .
  • Calculul propozițional este o teorie consistentă, completă, decidabilă.

Vezi și

Exemple de sisteme formale

Note

  1. ↑ Kleene S.K. Introducere în metamatematică . - M. : IL, 1957. - S. 59-60. Arhivat la 1 mai 2013 la Wayback Machine
  2. ↑ Mendelssohn E. Introducere în logica matematică . - M . : „Nauka”, 1971. - P. 36. Copie de arhivă datată 1 mai 2013 la Wayback Machine

Literatură

  Accesați articolul Wikidata  Dicționare și enciclopedii
 Logici
Filosofie • Semantică • Sintaxă • Istorie
Grupuri logice
logica clasica
logica matematica
Logica non-clasica
Logica filozofică
Componente
Lista simbolurilor booleene