Sistem formal

De la Wikipedia, enciclopedia liberă.
Salt la navigare Salt la căutare

În logica matematică , noțiunea de sistem formal este utilizată pentru a oferi o definiție strictă a demonstrației conceptului. Cu alte cuvinte, noțiunea de sistem formal corespunde unei formalizări riguroase și unei noțiuni cuprinzătoare de sistem axiomatic .

Descriere

Un sistem formal constă din:

  • un alfabet, care este un set (finit sau numărabil ) de simboluri ;
  • o gramatică care specifică care secvențe finite ale acestor simboluri sunt formule bine formate . Gramatica trebuie să fie recursivă în sensul că trebuie să existe un algoritm pentru a decide dacă o succesiune de simboluri este sau nu o formulă bine formată.
  • un subset al ansamblului de formule bine formate: axiomele sistemului formal. De asemenea, în acest caz, setul de axiome trebuie să fie recursiv.
  • unele reguli, respectivele reguli de inferență , care combină formule bine formate cu n -uple de formule bine formate. Mai specific, o regulă de inferență este un subset al tuturor n + 1 -duplurilor de formule bine formate: primele n formule din fiecare dintre aceste n + 1 -duple se numesc premise , în timp ce ultima formulă se spune că este una dintre ei.consecinta.

Cele mai frecvente exemple de sisteme formale sunt teoriile de ordinul întâi .

Dat fiind un sistem formal, setul teoremelor sale este definit recursiv ca fiind cel mai mic set de formule bine formate care sunt

  • axiome sau
  • pot fi obținute prin regulile de inferență ale sistemului folosind alte teoreme obținute anterior.

Până în prezent s-au folosit doar noțiuni sintactice, adică nu s-a făcut nicio referire la noțiunea de adevăr. Intuitiv, formulele bine formate sunt enunțuri care au sens, iar axiomele sunt enunțuri care trebuie considerate adevărate. Dacă presupunem că regulile de inferență vor aduce afirmații adevărate în alte afirmații adevărate, atunci toate teoremele sunt adevărate.

Cu toate acestea, trebuie remarcat faptul că definiția sistemului formal (și, prin urmare, definiția dovezii) poate fi dată independent de noțiunea de adevăr.

Chiar și noțiunea de adevăr poate fi însă formalizată prin construirea unei semantici pentru sistemul formal sau prin atribuirea fiecărui subset al setului de simboluri a unei clase de structuri (sau modele ), împreună cu o noțiune de satisfacție, care spune când o formulă este adevărat sau fals într-un model dat.

Cu toate acestea, atribuirea unei semantici nu este simplă și nu este întotdeauna posibilă, dacă doriți să existe o corespondență exactă între afirmațiile demonstrabile și afirmațiile adevărate , adică cele adevărate din fiecare model ( teorema completitudinii ) și dacă doriți ca definiția sistemului formal să fie recursivă.

Elemente conexe

Alte proiecte

linkuri externe

Matematica Portalul de matematică : accesați intrările Wikipedia care se ocupă de matematică