Virallista järjestelmää on matemaattinen mallintaminen on yleensä erikoistunut kieli. Kielellisiä elementtejä, sanoja , lauseita , puheita jne. Edustavat äärelliset objektit (kokonaisluvut, sekvenssit, puut tai äärelliset kaaviot jne.). Muodollisen järjestelmän ominaisuus on, että sen elementtien oikeellisuus kieliopillisessa mielessä on todennettavissa algoritmisesti, toisin sanoen ne muodostavat rekursiivisen joukon .
Muodolliset järjestelmät ovat vastakohtana luonnollisille kielille , joiden käsittelyalgoritmit ovat erittäin monimutkaisia ja ennen kaikkea niiden on kehittyttävä ajan myötä sopeutuakseen kielimuunnoksiin.
Muodolliset järjestelmät ilmestyivät matemaattisessa logiikassa edustamaan matemaattista kieltä ja matemaattista päättelyä, mutta ne löytyvät myös muista yhteyksistä: tietojenkäsittelytiede, kemia jne.
Logistiikat suunnittelivat muodolliset järjestelmät asettamaan ja matemaattisesti tutkimaan tiettyjä matemaattiseen kieleen liittyviä ongelmia. Tästä näkökulmasta voimme pitää niitä yleisinä metateorioina, teorioina (matemaattisista) teorioista.
Matemaattisen kielen mallintamiseen tähtäävät logiikkajärjestelmät ratkaisevat kolme ongelmaa:
Muodolliset järjestelmät ovat mahdollistaneet matematiikan epistemologian syntymisen, jota kutsutaan formalistiseksi näkökulmaksi, jonka lopussa matematiikka näkyy pelinä symbolien manipuloinnina tiukkojen sääntöjen mukaisesti, mutta etukäteen vailla merkitystä; kaavojen merkitys rekonstruoidaan jälkikäteen vuorovaikutuksella, jota ne ylläpitävät keskenään päättelysääntöjen kautta.
Aksiomaattinen teoria on looginen järjestelmä, joka edustaa matemaattista teoriaa, toisin sanoen joukko tuloksia, jotka kaikki liittyvät samantyyppisiin kohteisiin. Axiomatic teoria perustuu joukko aksioomat ovat kaavat määritellään keskeiset tavoitteet ja suhteet teoriaa; näistä aksiomeista ja päättelysääntöjä käyttämällä johdetaan teorian teoreemat . Esimerkiksi joukko-teoria on muodollinen järjestelmä, jonka aksiomit määrittelevät joukon käsitteen. Aksioma on siis todistamaton ehdotus, joka toimii lähtökohtana päättelylle: esimerkiksi "kahden pisteen kautta kulkee yksi ja vain yksi suora viiva" on euklidisen geometrian aksioma.
Aksiomien tai kaavojen totuus määritellään suhteessa malliin , mahdolliseen maailmankaikkeuteen, jossa kaavat tulkitaan.
Kuten edellä mainitsimme, muodolliset järjestelmät ovat rekursiivisia joukkoja , toisin sanoen voimme tarkistaa algoritmisesti, kuuluuko jokin elementti (kaava, termi, vähennys) järjestelmään. Aksiomaattinen teoria, jota pidetään sen aksiomien joukona, ei pääse tästä säännöstä, toisin sanoen kysymys siitä, kuuluuko aksioma teoriaan vai ei, on ratkaistavissa .
Jos toisaalta ajattelemme, kuten on tapana, aksiomaattista teoriaa sen aksiomien seurausten joukoksi, toisin sanoen sen lauseiden joukko, niin tämä ei, lukuun ottamatta harvinaisia poikkeuksia, ole rekursiivinen, mutta vain rekursiivisesti lueteltava : voimme kirjoittaa ohjelman, joka laskee kaikki aksiomien seuraukset soveltamalla loogisia sääntöjä mekaanisesti ja kaikin mahdollisin tavoin. Toisaalta ei ole olemassa ohjelmaa, joka kaavan F perusteella tietää kuinka vastata, jos tämä on teorian lause; tai tarkemmin sanottuna, ei voi tehdä paremmin kuin luetella kaikki teorian lauseet edellisen ohjelman avulla: jos F on lause, niin se esiintyy luettelossa lopullisen ajan lopussa, mutta jos ei, ei aksioomien seurauksena, ohjelma ei koskaan pääty.
Aksiomaattinen teoria on johdonmukainen, jos on kaavoja, jotka eivät ole seurausta sen aksiomeista. Esimerkiksi Peanon aritmeikka on johdonmukainen, koska se ei todista kaavaa "0 = 1". Voimme vastaavasti määritellä johdonmukaisuuden tosiasiana, ettei ristiriitaa osoiteta.
Kurt Gödel osoitti, että mikään aksiomaattinen teoria, joka oli riittävän voimakas edustamaan aritmeettista, ei voinut osoittaa omaa johdonmukaisuuttaan muodollisella tavalla (katso Gödelin epätäydellisyyslause ).
Kuten edellä mainitsimme, ohjelmointikielet ovat muodollisia järjestelmiä: koska loogisia järjestelmiä käytetään matemaattisen kielen (lause, demonstraatiot) virallistamiseen, ohjelmointikielet virallistavat algoritmit . Ohjelmointikielet koostuvat vähintään kahdesta osasta:
Johon joskus lisätään kolmas komponentti:
Ohjelmointikielien lisäksi tietojenkäsittelytiede määrittelee useita muita muodollisten järjestelmien tyyppejä: määrityskielet, joiden avulla määritellään ohjelman haluttu käyttäytyminen siten, että se voidaan sitten testata, todentaa tai osoittaa, että tietty toteutus täyttää spesifikaation; viestintäprotokollat että tiukasti määrittelevät tiedonvaihtoa tietokoneiden välillä (tai matkapuhelin) verkossa ...
Kuudes Hilbert ongelma aiheutti vuonna 1900 Saksan matemaatikko David Hilbert pyrkii axiomatize fysiikkaa.
Annetussa konferenssissa 11. syyskuuta 1917 Zürichissä David Hilbert toteaa, että minkä tahansa fysikaalisen teorian aksiomien on kunnioitettava kokonaisuuden riippumattomuuden ja ristiriitattomuuden kriteerejä (kuten matematiikassa), tähän lisätään toisen kohdan osalta velvoite olla ristiriidassa toisen tieteenalan kanssa .