19. gs. beigās jau bija radusies matemātiskā loģika un dažādām matemātikas teorijām meklēti piemēroti aksiomātiski formulējumi predikātu loģikā. Taču vienā no loģikas sistēmām, arī kopu teorijā, uz kuru, kā jau bija noskaidrots, var balstīt lielu daļu matemātikas, atklājās pretrunas. Tika izmēģināti dažādi rīcības ceļi to novēršanai. Vācu matemātiķis Dāvids Hilberts (David Hilbert) ieteica matemātiski analizēt visus kādā teorijā iespējamos pierādījumus un tā mēģināt parādīt, ka pretrunas tajā atvasināt nevar. Taču šim nolūkam matemātiķu veidotie pierādījumi jāpadara par precīziem matemātiskiem objektiem, un arī to analīze jāveic ar ticamām un viegli pārbaudāmām matemātiskām metodēm. Vēlāk, 20. gs. 20. gadu sākumā, D. Hilberts nāca klajā ar īpašu (t. s. formālisma) programmu matemātikas pamatošanai; cita starpā, tā paredzēja, ka visi matemātikas apgalvojumi jāpieraksta precīzā simbolu valodā, jāapstrādā pēc precīzi definētām kārtulām un ka teorijas nepretrunības pierādījums arī jāveic līdzīgā formālā ietvarā, turklāt lietojot tikai finitāras (bezgalību nekādā formā neiesaistošas) metodes. Šī programma izrādījās nerealizējama iecerētajā formā, taču veicināja dažādu formalizējumu rašanos loģikā un matemātikā (ar laiku arī ārpus matemātikas) un to pētīšanu. Jāņem vērā, ka par formalizēšanu labāka pieeja ar matemātisku teoriju īpašībām un pamatošanu saistīto jautājumu risināšanai nav atrasta.

Tehniskajā nozīmē nosaukums “formāla sistēma” ir loģikā un matemātikas pamatos lietots termins D. Hilberta proponētajā stilā formalizētām teorijām un tām līdzīgām sistēmām; šis formalizēšanas stils ir tuvs matemātiķu parastajam skatam uz aksiomātiskām teorijām, bet nav vienīgais. Plašā nozīmē tā mēdz saukt jebkādu “formāli izveidotu” sistēmu.

Formālu sistēmu ℱ veido kāda formāla valoda ℒ un tajā izvēlēts deduktīvais aparāts 𝒟. Formālas valodas ir mākslīgi veidotas rakstu valodas; vairāk par tām skat. šķirklī Formalizētas valodas. Savukārt deduktīvais aparāts satur līdzekļus izvedumu (formālu pierādījumu) veidošanai sistēmā. Tas sastāv no aksiomām – izraudzītām attiecīgās valodas formulām – un pēc iespējas nedaudzām izveduma kārtulām; katra šī kārtula ir precīzs priekšraksts kādas noteiktas formas slēdzienu izdarīšanai (sistēmas valodā ℒ). 

Atgādne: loģikā ar slēdzienu saprot domāšanas darbību (arī tās izteiksmi valodā), kurā no viena vai vairākiem apgalvojumiem (spriedumiem), ko sauc par slēdziena premisām, atvasina jaunu – šī slēdziena gala secinājumu. Pareizs deduktīvs slēdziens neizmanto ne iesaistīto premisu saturu, ne kādu citu ārēju informāciju, bet balstās vienīgi uz kādu no attiecīgās loģikas sistēmas (matemātikā – arī attiecīgās teorijas) pamatlikumiem. 

Formālā valodā slēdziens izpaužas kā pāreja no vienas vai vairākām formulām pie citas. Katra izvedumkārtula fiksē izmantojamo premisu skaitu, nosaka, kādiem premisu komplektiem slēdziens ir izdarāms, kā arī norāda, kāds secinājums katrā gadījumā ir iegūstams.

Piemērs: viens no vienkāršākajiem klasiskās izteikumu loģikas likumiem nosaka:

ja apgalvojums “A vai B” ir patiess un A nav patiess, tad B ir patiess. 

Formālā šīs loģikas sistēmā tam atbilst kārtula, kas nosaka, ka, lai kādas arī būtu formulas A un B, no formulām A ∨ B un ¬A drīkst pāriet pie formulas B kā secinājuma. Īsi tādu kārtulu kodē kā figūru 

A ∨ B,¬A

B

Formālās sistēmas ir tā saukto loģisko rēķinu paveids (angļu logical calculus, proof system, vācu logischer Kalkül, Logikkalkül, franču calcul logique, krievu логическое исчисление) – t. s. Hilberta tipa rēķini. Tādi ir, piemēram, izteikumu un arī predikātu rēķinu standartformulējumi. Ir arī loģiskie rēķini ar citādi iekārtotu deduktīvo aparātu, piemēram, naturālā izveduma sistēmas, sekvenču rēķini, analītisko tablo metode. Dažkārt gan par loģiskajiem rēķiniem sauc tikai sistēmas deduktīvo aparātu.

Īsumā – izvedumi ir formāli, pēc izveduma kārtulām veidoti pierādījumi. Par galīgu formulu virkni saka, ka tā ir izvedums, ja katrs šīs virknes loceklis ir vai nu aksioma, vai arī iegūstams no kādiem agrākiem virknes locekļiem pēc vienas no sistēmas veidotājkārtulām. Saka arī, ka tā ir kādas formulas B izvedums, ja B ir šīs virknes pēdējais loceklis, bet formulu B sauc par izvedamu, arī par teorēmu, ja tai eksistē tāds izvedums. Līdzīgi formalizē pierādījumus, kur izmanto hipotēzes vai citādus pieņēmumus: pieņemot, ka Γ ir kāda formulu kopa, kuras izmanto līdzīgi aksiomām, var runāt par formulas B izvedumu no Γ vai, piemēram, ka tā ir izvedama no Γ. 

Tagad var aprakstīt divas svarīgas formālo sistēmu īpašības, kas gan ir vēlamas, bet ne jebkurai sistēmai piemīt.

1. Formālu sistēmu sauc par (sintaktiski) bezpretrunīgu, ja tajā ne visas formulas ir izvedamas. Ja sistēmā ir loģiskā operācija negācija (piemērots tās variants), tad tā izrādās bezpretrunīga tad un tikai tad, ja neviena formula nav izvedama kopā ar savu negāciju (pēc principa “no pretrunas var izsecināt jebko”). 
2. Formālu sistēmu ar negāciju sauc par (sintaktiski) pilnu, ja katra formula, kas nav atkarīga no mainīgajiem (kad tādi sistēmas valodā ir), vai nu tā pati, vai tās negācija ir izvedama.

Ir zināms, piemēram, ka gan klasiskie izteikumu, gan klasiskie predikātu rēķini ir sintaktiski bezpretrunīgi, bet ne pilni.

Formālu sistēmu ℱ var saukt par interpretētu, ja, vadoties no noteiktiem apsvērumiem, izvēlēta kāda tās valodai atbilstošu interpretāciju kopa ℐ (tā pārvēršot šo valodu formalizētā valodā, kas ļauj runāt par formulu vispārpatiesumu un sekošanu). Tad var vaicāt, cik saskaņots ir sistēmas deduktīvais aparāts ar interpretācijām no ℐ (vai otrādi). Saka, ka interpretēta sistēma ℱ ir:

1. semantiski pilna, ja tajā katra vispārpatiesa formula ir izvedama; 
2. semantiski bezpretrunīga, ja, otrādi, tajā katra izvedamā formula ir vispārpatiesa; 
3. adekvāta, ja izpildīti abi iepriekšējie nosacījumi. 

Līdzīgi salīdzinot sekošanu un izvedamību no hipotēzēm, definē sistēmas ℱ semantisko pilnību, semantisko bezpretrunību un adekvātību plašākā nozīmē. Interpretēta formāla sistēma ir semantiski bezpretrunīga tad un tikai tad, kad tās aksiomas ir vispārpatiesas, bet izvedumkārtulas no interpretācijā patiesām premisām vienmēr noved pie patiesa secinājuma. Panākt, lai tā būtu arī adekvāta, izdodas ne ar katru interpretāciju kopu ℐ. Ir zināms, piemēram, ka gan klasiskie izteikumu rēķini, gan klasiskie predikātu rēķini ir adekvāti. 

Formālas sistēmas jēdziens ir viens no centrālajiem matemātiskajā loģikā, jo mūsdienās ikviena pietiekami attīstīta loģikas sistēma tiek noformēta kā interpretēta formāla sistēma. Cenšas panākt, lai tā būtu adekvāta. Formālas sistēmas izmanto arī gan matemātikas un pat dažu dabaszinātņu pamatos, gan saistītās datorzinātnes jomās. Piemēram, automatizētas teorēmu pierādīšanas sistēmas iespējamas vien teorijām, kas noformētas kā formālas sistēmas vai citādi loģiskie rēķini, un vienīgi tādām teorijām (kas faktiski ir patstāvīgi matemātiski objekti) var pētīt to vispārīgās īpašības.