Mūsu domāšanas loģiskās likumības izpaužas valodā un tāpēc ir novērojamas, analizējamas un pētāmas, vien balstoties uz valodas materiālu. Taču parastajām dabiskajām valodām ir vairākas īpašības, kas apgrūtina to darīt: tās nav pietiekami precīzas, laika gaitā mainās, tajās mēdz būt gan dažādas sintaktiskas, gan semantiskas dabas neviennozīmības. Turklāt dabisko valodu izteiksmēm ir savs saturs, no kā loģiskajā analīzē nākas abstrahēties. Loģikas formalizētās valodas tikušas ieviestas, lai šādas grūtības apietu.

Tradicionālajā loģikā tā saukto kategorisko spriedumu un dažādu veidu siloģismu struktūras attēlošanai viduslaikos izveidojās īpaša simbolisku pierakstu sistēma, ko jau var uzskatīt par ļoti vienkāršu formalizētu valodu ar nelielām iespējām. Daudz bagātākas pierakstu sistēmas loģikas vajadzībām radās vien 19. gs., kad veidojās mūsdienu algebra un matemātiskā loģika. Par pirmo simbolisko loģikas valodu mūsdienu izpratnē uzskata Gotloba Frēges (Friedrich Ludwig Gottlob Frege) tā saucamo jēdzienrakstu (vācu Begriffsschrift) – viņa 1879. gadā radīto predikātu loģikas valodu. Tā gan bija tipogrāfiski sarežģīta, jo balstījās uz grafiskām konstrukcijām, tāpēc neieviesās. Šajā ziņā ievērojami veiksmīgāka bija Bērtranda Rasela (Bertrand Arthur William Russell) un Alfrēda Vaitheda (Alfred North Whitehead) monogrāfijā “Matemātikas pamatprincipi” (Principia Mathematica) pirmajā sējumā (1910) ieviestā daudz bagātākā tipu teorijas valoda. Pāris turpmākajās desmitgadēs tika izdalīti vien dažādi noderīgi tās fragmenti, variēti izmantojamie simboli un pilnveidoti daži lietojamie paņēmieni. Izteikumu un predikātu rēķinu formālās valodas tika aprakstītas 1938. gadā iznākušajā Dāvida Hilberta (David Hilbert) un Vilhelma Akermana (Wilhelm Friedrich Akermann) grāmatā “Teorētiskās loģikas pamatiezīmes” (Grundzüge der theoretischen Logik). Kopš 20. gs. 30. gadiem formalizētu valodu veidošanas un lietošanas principi nav būtiski mainījušies, tikai, zinātnei un lietojumiem attīstoties, arī tajā izmantotās valodas, it īpaši to interpretācijas, kļūst arvien daudzveidīgākas. 

Vairums formalizēto valodu ir parasto (dabisko) valodu vienkāršoti modeļi ar precīzi aprakstītu viennozīmīgu sintaksi un semantiku, kas saglabā vien uz loģiku attiecināmas parasto valodu iezīmes. Formalizētas valodas pamatā ir tās alfabēts – brīvi izraudzīta galīga vai sanumurējama simbolu kopa. Galīgas šo simbolu rindas nosauc par (formāliem) vārdiem. Valodas sintakse nosaka, kuri no tiem ir pareizi darinātas, pie valodas piederošas izteiksmes, un iedala tās noteiktās kategorijās, kas nosaka to lietošanas iespējas (līdzīgi vārdšķirām dabiskajās valodās), bet tās semantika – kā katras kategorijas izteiksmes interpretējamas. Izmanto arī valodas, kurām gan ir precīza sintakse, bet semantika netiek aplūkota vispār vai ir novirzīta otrā plānā. Tādu “bezsemantikas” valodu sauc par formālu, tomēr dažkārt tāpat tiek sauktas arī formalizētas valodas.

Formalizētu (arī formālu) valodu apraksta kādā jau esošā valodā, piemēram, latviešu, tomēr jaunizveidotā valoda ir stingri jānošķir no aprakstīšanai izmantotās. Šajā sakarā aprakstāmo valodu mēdz saukt par objektvalodu, bet aprakstošo – par tās metavalodu. No loģikā lietotajām valodām (tikai par tādām turpinājumā būs runa) nozīmīgākās un plašāk zināmās ir izteikumu loģikas un predikātu loģikas valodas. Jāpiezīmē, ka datorzinātnēs lietojamajām formālajām valodām ir citi uzdevumi un tāpēc arī atšķirīgi to veidošanas principi. 

Loģikas valodās izteiksmes darina rekursīvi: aprakstot valodas sintaksi, uzrāda tās sākuma izteiksmes un veidotājkārtulas, pēc kurām no jau esošām izteiksmēm (iespējams, izmantojot arī palīgsimbolus, kā iekavas vai komati) darina jaunas saliktas, vienlaikus norādot arī izveidotās izteiksmes sintaktisko kategoriju. Turklāt jābūt ievērotiem šādiem noteikumiem: 

1. neviens vārds, ko nevar pakāpeniski šādā ceļā iegūt, nav izteiksme; 
2. katra sākuma izteiksme ir vienkārša, t. i., nav iegūstama ar veidotājkārtulu no citām; 
3. katrai saliktai izteiksmei var viennozīmīgi noteikt, ar kuru veidotājkārtulu un no kurām izteiksmēm tā izveidota; 
4. ja izteiksmes A sastāvā kādu izteiksmi B aizstāj ar tās pašas sintaktiskās kategorijas izteiksmi C, tad rodas izteiksme, kas pieder pie tās pašas kategorijas kā A; ja turpretī C ir no citas kategorijas, tad aizstāšanas rezultāts nav pareiza valodas izteiksme. 

Galvenā izteiksmju kategorija ir formulas – formāli analogi tiem parastās valodas teikumiem, kuri izsaka kādu apgalvojumu; pārējās izteiksmes ir līdzeklis vai materiāls formulu veidošanai. Daudzās valodās vēl ir arī termi, kas atbilst parastās valodas nominālajām jeb lietvārda frāzēm. Bez šīm pamatkategorijām ir arī dažādi funktori un citādi operatori, ar kuru palīdzību, sekojot veidotājkārtulām, no vienas vai vairākām izteiksmēm darina jaunas. Piemēram, vienmēr, izņemot ļoti vienkāršas valodas, ir funktori saliktu formulu darināšanai no esošām (izteikumfunktori jeb loģiskie operatori); tie atbilst parastās valodas saikļiem, ar kuriem darina saliktus teikumus. Lielā daļā formalizēto valodu formulas var saturēt mainīgos un tad arī tā sauktos kvantorus.

Formalizētas valodas semantiku fiksē izvēlētu tās interpretāciju kopums. Valodas interpretācija noteiktā veidā sasaista to ar kādu ārpusvalodas realitāti – interpretācijas apgabalu (kas parasti ir kāda abstrakta loģiski matemātiska sistēma, dažkārt pat ļoti vienkārša) un nosaka, kuras formulas šajā apgabalā uzskatāmas par patiesām. Vienkāršākajos gadījumos, starp kuriem ir, piemēram, visas klasiskajā izteikumu un arī predikātu loģikā lietotās valodas, tas notiek šādi. Katrai sintaktiskajai kategorijai interpretācija piesaista piemērotu ar interpretācijas apgabalu saistītu entitāšu kopumu. Formulām vienmēr atbilst tā sauktās patiesumvērtības (parasti tās ir divas, aplams un patiess, bet ir valodas, kurās to ir vairāk), starp kurām vismaz viena ir izcelta. Tāpat, piemēram, divvietīgiem izteikumfunktoriem atbilst divvietīgas operācijas ar patiesumvērtībām. Ja valodā ir arī termi, tiem atbilstošās entitātes mēdz saukt par indivīdiem: tie ir objekti, par kuriem ar interpretētās valodas palīdzību “runā”. Tad funktoriem, kas no diviem termiem darina termu, atbilst divvietīgas operācijas ar indivīdiem utt. Tālāk interpretācija katrai vienkāršai izteiksmei, kas nav mainīgais, piekārto attiecīga tipa entitāti, kas tad ir šīs izteiksmes vērtība interpretācijā, bet īpašas semantiskās kārtulas nosaka, kā tālāk “izrēķināt” salikto izteiksmju vērtības. Rezultātā katra formula atkarībā no savu mainīgo (ja tādi ir) vērtībām iegūst kādu patiesumvērtību. Tās formulas, kas iegūst izceltu vērtību, nosauc par patiesām šajā interpretācijā, nekādu citu jēgu ar šo nosaukumu nesaistot.

Valodai var pieņemt arī vairākas interpretācijas, un tām var būt atšķirīgi apgabali. Formulu, kas patiesa visās pieņemtajās valodas interpretācijās, sauc par vispārpatiesu (arī identiski patiesu vai loģiski patiesu) un saka, ka formula A (loģiski) seko no kādas formulu kopas Γ, ja tā ir patiesa katrā pieņemtajā interpretācijā, kurā patiesas visas formulas no Γ. (Tukšai kopai Γ, kad interpretācijas netiek ierobežotas, tas nozīmē, ka A ir vispārpatiesa.) Kopu Γ sauc par saderīgu, ja vismaz vienā pieņemtajā interpretācijā visas tās formulas ir patiesas. 

Kopsavelkot: uzdot formalizētu valodu nozīmē uzdot tās alfabētu, veidotājkārtulas un interpretāciju kopu. Valodas tipu nosaka tas, kādas tajā ir sintaktiskās kategorijas un kāda veida interpretācijas tiek pieļautas. Viena tipa valodas var atšķirties ar vienkāršo (līdz ar to visu) izteiksmju sastāvu katrā sintaktiskajā kategorijā; konkrētais alfabēts un izteiksmju izskats nav loģikas vajadzībām būtisks. 

Dabisko valodu formalizēšana palīdz izprast, kā tajās izpaužas mūsu domāšanas loģiskās likumības. Pašā loģikā formālās valodas un to interpretācijas ir dažādu loģikas formālo sistēmu pamatā, kur pēc īpašām kārtulām veido formālus pierādījumus; parasti tie ir kādas formulu virknes, bet var būt arī sarežģītākas struktūras veidojumi. Datorzinātnē formalizētas loģikas valodas noder zināšanu reprezentāciju formālismos, ekspertu sistēmās, mākslīgā intelekta jomā, loģiskajā programmēšanā. Universālajā algebrā aksiomu loģiskā uzbūve daudzos gadījumos dod informāciju par noteiktām attiecīgo algebrisko sistēmu un to klašu īpašībām.