Formaalijärjestelmä

Formaalijärjestelmä on matemaattinen rakenne, jolla määritellään formaalinen kieli, muodostussäännöt, aksioomakokoelma sekä johtamissäännöt. Sen tarkoituksena on mahdollistaa todistusten rakentaminen pelkän syntaksin perusteella: lauseet muodostetaan sääntöjen mukaan, ja niiden totuusarvoon liittyvä semantiikka määritellään erillisellä tavalla. Näin syntaksisesta prosessista voidaan erottaa merkitys.

Peruselementit ovat: formaalikieli (tunnukset ja lauseet), muodostussäännöt (miten lauseet voivat rakentua), aksioomakokoelma (lähteet todistuksille) sekä päätössäännöt (esim. modus ponens), joiden nojalla aksioomista ja aiemmista lauseista johdetaan uusia lauseita. Lause, jota voidaan johtaa näiden sääntöjen avulla, on teoreema; muut lauseet voivat toimia annetun järjestelmän sisäisinä väittäminä tai hypoteeseina.

Esimerkkejä formalisteista ovat propositiologiikka ja predikaattilogiikka sekä erilaiset Hilbert-tyyppiset järjestelmät, luonnollisen todistamisen menetelmät ja sequenttialgebra. Käytännön sovelluksissa ne tarjoavat tavan formalisoida matematiikkaa, logiikkaa sekä tietojärjestelmissä tapahtuvaa todistamista ja ohjelmistojen oikeellisuuden varmistamista.

Ominaisuudet: äänenkestävyys tarkoittaa, että kaikki todistettavat lauseet ovat semanttisessa mielessä totuuksia, ja täydellisyys, että kaikki semanttisesti pätevät lauseet voidaan todistaa järjestelmän keinoin. Riittävän vahvoihin aritmetiikan järjestelmiin kohdistuvat Gödelin epätäydellisyyslauseet: ei voi olla sekä täydellinen että johdonmukainen järjestelmä, eikä järjestelmä pysty osoittamaan oman johdonmukuutensa.

Käyttöalueet kattavat matematiikan perustan, tietojenkäsittelyn teorian sekä automaattisen todistamisen ja ohjelmistojen virheiden havaitsemisen.