Sistema formal

Un sistema formal o sistema llògic és un sistema abstracte compost per un llenguage formal, axioma, regles d'inferència i a voltes una semàntica formal, que s'utilisa per a deduir o demostrar teoremes i donar una definició rigorosa del concepte de demostració. Un sistema formal és una formalisació rigorosa i completa del concepte de sistema axiomàtic, els quals es poden expressar en llenguage formal o en llenguage natural formalisat. En crear un sistema formal es pretén capturar i abstraure l'essència de determinades característiques del món real, en un model conceptual expressat en un determinat llenguage formal. Alguns dels sistemes formals més coneguts són la llògica proposicional, la llògica de primer orde i la llògica modal.

En la teoria de la demostració, les demostracions formals es poden expressar en el llenguage dels sistemes formals, consistents en axiomas i regles d'inferència. Les teoremes poden ser obtinguts per mig de demostracions formals. Este punt de vista de les matemàtiques ha segut denominat formaliste; encara que en moltes ocasions este terme comporta una accepció pijorativa. En eixe sentit, David Hilbert va crear la metamatemática per a estudiar els sistemes formals, entenent que el llenguage utilisat per a això, denominat metallenguage era distint del llenguage del sistema formal que es pretenia estudiar, al que es diu llenguage objecte.

Un sistema aixina és la reducció d'un llenguage formalisat a mers símbols, llenguage formalisat i simbolisat sense contingut material algun; un llenguage reduït a mera forma que s'expressa per mig de fòrmules que reflectixen les relacions sintàctiques entre els símbols i les regles de formació i transformació que permeten construir les fòrmules del sistema i passar d'una fòrmula a una atra.

Una teoria axiomàtica és un conjunt de fòrmules en un determinat llenguage formal i totes les fòrmules deduibles de dites expressions per mig de les regles d'inferència possibles en dit sistema formal. L'objectiu de les teories axiomàtiques és construir sistemes formals que representen les característiques essencials de branques sanceres de les matemàtiques. Si se selecciona un conjunt més ampli o menys ampli de axioma el conjunt de teoremes deduibles canvien. L'interés de la teoria de models és que en un model en que satisfacen els axioma de determinada teoria també se satisfan les teoremes deduibles de dita teoria. És dir, si una teorema és deduible en una certa teoria, llavors eixa teorema és universalment vàlit en tots els models que satisfan els axioma. Açò és interessant perque en principi la classe de models que satisfà una certa teoria és difícil de conéixer, ya que les teories matemàtiques interessants en general admeten tota classe infinita de models no isomorfos, per lo que la seua classificació en general resulta difícilment abordable si no existix un sistema formal i un conjunt de axioma que caracterise els diferents tipos de models.

En el XX, Hilbert i uns atres varen sostindre que la matemàtica és un sistema formal. Pero en 1931, Kurt Gödel va demostrar que cap sistema formal en suficient poder expressiu per a capturar l'aritmètica de Peano pot ser al mateix temps consistent i complet. El teorema de la incompletitud de Gödel, junt en la demostració d'Alonzo Church de que la matemàtica tampoc és decidible, va terminar en el programa de Hilbert. No obstant, a pesar de les seues llimitacions, l'enfocament seguix sent àmpliament usat, bàsicament perque no s'ha trobat cap alternativa millor a l'enfocament formaliste de Hilbert i la pretensió de treballar en el sí de teories matemàtiques explícitament axiomatizadas, encara en les seues llimitacions.

Els sistemes formals també han trobat aplicació dins de l'informàtica, la teoria de l'informació i l'estadística.

Components

Un sistema formal està compost per:

1. Un conjunt de símbols primitius (l'alfabet o vocabulari).
2. Un conjunt de regles de formació (la gramàtica) que nos diu cóm construir fòrmules ben formades a partir dels símbols primitius. El llenguage del sistema serà el conjunt de totes eixes fòrmules.
3. Un conjunt d'axiomas o esquemes de axioma. Cada axioma deu ser una fòrmula ben formada.
4. Un sistema deductivo o conjunt de regles d'inferència. Estes regles determinen qué fòrmules es poden inferir de quines fòrmules. Per eixemple, una regla d'inferència clàssica és el modus ponens, segons el qual, donada una fòrmula A, i una atra fòrmula A→B, la regla nos permet inferir B.

Estos quatre elements completen la part sintàctica dels sistemes formals. No obstant, encara no s'ha donat cap significat als símbols discutits, i de fet, un sistema formal es pot definir sense tindre que fer-ho. Tal tasca correspon al camp cridat semàntica formal, que s'ocupa d'introduir un quint element:

5. Una interpretació formal. En els llenguages naturals, una mateixa paraula pot significar diverses coses depenent de l'interpretació que se li done. Per eixemple, en l'idioma espanyol, la paraula «banc» pot significar un edifici o un assent, mentres que en atres idiomes pot significar alguna cosa completament distint o res en absolut, i depenent de l'interpretació, variarà també el valor de veres de l'oració «el banc està prop». Les interpretacions formals assignen significats inequívocs als símbols primitius, i valors de veres a les fòrmules.

Per a entendre millor estos elements, definim un sistema formal minimaliste cridat M.

El sistema M té un alfabet en un únic símbol: a

Les fòrmules ben formades de M són aquelles que es construïxen en les següents regles de formació:

1. a és una fòrmula
2. Si φ és una fòrmula, llavors φa també és una fòrmula
3. Res més és una fòrmula

Per lo tant, el llenguage de M consta de les següents fòrmules: a, aa, aaa, aaaa, aaaaa, ...

M té un únic axioma: a

M té una única regla d'inferència: de φ es pot inferir φa

Les teoremes són aquelles fòrmules que es deduïxen dels axioma a través de les regles d'inferència en un número finito de passos. En este cas, les teoremes de M seran: aa, aaa, aaaa, aaaaa, ...

És dir totes les fòrmules ben formades, llevat a.

Tipos de sistemes formals

Artícul principal → Càlcul llògic.

Existix un debat sobre si és correcte parlar d'una llògica, o de vàries llògiques, pero en el XX s'han desenrollat no un, sino varis sistemes formals diferents, que capturen i formalisen distintes parts del llenguage natural.

Vore també

• Llògica matemàtica
• Llenguage formalisat
• Noció primitiva
• Teoria (llògica)

Bibliografia

• Raymond M. Smullyan, 1961. Theory of Formal Systems: Annals of Mathematics Studies, Princeton University Press (April 1, 1961) 156 pag. ISBN 069108047X
• S. C. Kleene, 1967. Mathematical Logic Reprinted by Dover, 2002. ISBN 0486425339
• Douglas Hofstadter, 1979. Gödel, Escher, Bach: An Eternal Golden Braid. 777 pag. ISBN 978-0465026562.