A formális rendszer egy általában specializált nyelv matematikai modellezése . A nyelvi elemeket, szavakat , mondatokat , beszédeket stb. Véges objektumok (egész számok, szekvenciák, fák vagy véges grafikonok stb.) Ábrázolják. A formális rendszer jellemzője, hogy elemei nyelvtani értelemben vett helyessége algoritmikusan ellenőrizhető, vagyis rekurzív halmazot alkot .
A formális rendszerek szemben állnak a természetes nyelvekkel , amelyeknél a feldolgozási algoritmusok rendkívül összetettek, és mindenekelőtt az idő előrehaladtával kell fejlődniük ahhoz, hogy alkalmazkodjanak a nyelv átalakításához.
A matematikai logikában a formális rendszerek a matematikai nyelv és a matematikai érvelés ábrázolása érdekében jelentek meg , de más kontextusokban is megtalálhatók: informatika, kémia stb.
A hivatalos rendszereket logikusok tervezték, hogy a matematikai nyelvvel kapcsolatos problémákat feltegyenek és matematikailag tanulmányozzák. Ebből a szempontból tekinthetjük őket általános metateóriáknak, a (matematikai) elméletekről szóló elméleteknek.
A matematikai nyelv modellezését célzó logikai rendszerek három problémát oldanak meg:
A formális rendszerek lehetővé tették a matematika ismeretelméletének megjelenését, az úgynevezett formalista nézőpontot , amelynek végén a matematika szigorú szabályok szerinti szimbólumok manipulációs játékaként jelenik meg, de eleve értelmetlen; a képletek jelentését utólag rekonstruálják az egymással az érvelés szabályain keresztül fenntartott kölcsönhatások.
Az axiomatikus elmélet egy logikai rendszer, amely matematikai elméletet képvisel, vagyis az eredmények azonos halmazra vonatkoznak. Az axiomatikus elmélet axiómák halmazán alapul, amelyek olyan képletek, amelyek meghatározzák az elmélet alapvető tárgyait és kapcsolatait; ezekből az axiómákból és az érvelés szabályainak felhasználásával vezetjük le az elmélet tételeit . Például a halmazelmélet egy formális rendszer, amelynek axiómái meghatározzák a halmaz fogalmát. Az axióma tehát egy bizonyítatlan állítás, amely az érvelés kiindulópontjaként szolgál: például „két ponton keresztül egy és csak egy egyenes halad át” az euklideszi geometria axióma.
Az axiómák vagy képletek igazságát egy modellhez , egy lehetséges univerzumhoz viszonyítva határozzuk meg, amelyben a képleteket értelmezzük.
Mint fentebb említettük, a formális rendszerek rekurzív halmazok , vagyis algoritmikusan ellenőrizhetjük, hogy egy elem (képlet, kifejezés, dedukció) tartozik-e a rendszerhez. Az axiomatikus elmélet, amelyet axiómáinak halmazaként tekintenek, nem kerüli el ezt a szabályt, vagyis azt a kérdést, hogy tudják-e, hogy egy axióma az elmélethez tartozik-e vagy sem, eldönthető .
Ha viszont - szokás szerint - axiomatikus elméletet gondolunk axiómáinak következményeinek halmazára, vagyis tételeinek halmazára, akkor ez a ritka kivételeket kivéve nem rekurzív, de csak rekurzív módon felsorolható : írhatunk egy programot, amely a logikai szabályok mechanikus és minden lehetséges alkalmazásával felsorolja az axiómák összes következményét. Másrészt nincs olyan program, amely az F képlet ismeretében tudja, hogyan válaszoljon, ha ez az elmélet tétele; vagy pontosabban nem lehet jobb, mint az elmélet összes tételének felsorolása az előző program segítségével: ha F tétel, akkor egy véges idő végén megjelenik a felsorolásban, de ha nem, akkor nem az axiómák következménye, a program soha nem ér véget.
Az axiomatikus elmélet akkor következetes, ha vannak olyan képletek, amelyek nem axiómáinak következményei. Például Peano számtana következetes, mert nem bizonyítja a "0 = 1" képletet. A koherenciát ekvivalensen definiálhatjuk annak tényeként, hogy nem mutatunk ellentmondást.
Kurt Gödel kimutatta, hogy minden olyan axiomatikus elmélet, amely elég erős ahhoz, hogy az aritmetikát képviselje, nem tudja formálisan bemutatni saját következetességét (lásd Gödel hiányosságainak tétele ).
Mint fentebb említettük, a programozási nyelvek formális rendszerek: mivel a logikai rendszereket a matematikai nyelv (tétel, demonstrációk) formalizálására használják , a programozási nyelvek algoritmusokat formalizálnak . A programozási nyelvek legalább két alkotóelemből állnak:
Amihez néha hozzáadódik egy harmadik komponens is:
A programozási nyelveken kívül a számítástechnika a formális rendszerek számos más típusát is meghatározza: olyan specifikációs nyelvek, amelyek a program kívánt viselkedésének meghatározására szolgálnak, hogy ezután kipróbálhassák, ellenőrizhessék vagy bebizonyíthassák, hogy egy adott megvalósítás megfelel-e a specifikációnak; a hálózati számítógépek (vagy mobiltelefonok) közötti információcserét szigorúan meghatározó kommunikációs protokollok ...
Az 1900-ban David Hilbert német matematikus által felvetett hatodik Hilbert-probléma célja a fizika axiomatizálása.
Adott konferencián 1917. szeptember 11 Zürichben David Hilbert kijelenti, hogy bármely fizikai elmélet axiómáinak tiszteletben kell tartaniuk az egész függetlenségének és ellentmondásmentességének kritériumait (mint a matematikában), ehhez a második ponthoz hozzátartozik az a kötelezettség, hogy ne mondjon ellent egy másik tudományos területnek .