Formalni dokaz je niz tvrdnji, verbalnih ili matematičkih, koji se koristi za demonstriranje logičke nužnosti danog zaključka. Takvi dokazi zahtijevaju rigoroznu i preciznu upotrebu jezika, jer jezična dvosmislenost može lako učiniti dokaz besmislenim. U mnogim slučajevima, kako bi se izbjegao ovaj problem, može se predstaviti formalni dokaz simbolički ili matematički kako bi se izbjegla zbrka koju unosi jezik koliko god je to moguće. Takvi strogo formalni dokazi općenito počinju s jednom ili više dobro utvrđenih ili teorijskih premisa. Nakon ovih premisa slijede aksiomi ili tvrdnje koje logički slijede iz prethodnih tvrdnji i završavaju konačnim zaključkom ili dokazanim teoremom koji je, kao i prethodne tvrdnje, logički nužan rezultat početnih premisa i aksioma.
Za razliku od formalnog dokaza, većina argumenata u svakodnevnom životu oslanja se na zajednički jezik i općenito nisu logički rigorozni. Oni, na primjer, ne mogu potjecati iz dobro izgrađenog skupa premisa ili se mogu oslanjati na retoričke pozive – u pogledu emocija ili autoriteta – kojima nema mjesta u formalnom dokazu. Dok je formalni dokaz vrijedan zbog svoje sposobnosti da pokaže točnost iskaza na temelju skupa premisa, važno je zapamtiti da formalni dokazi imaju malo ili nimalo koristi kada se raspravlja o bilo čemu što se ne može uvjerljivo dokazati u području logike. . Također, primjenjuju se samo u kontekstu izvornih premisa i stoga ne pokazuju univerzalne istine.
Većina formalnih dokaza temelji se na “formalnom jeziku” koji se sastoji ili od podskupa normalnog jezika ili u simbolima. Matematički formalni dokaz, na primjer, izražava se pomoću simbola koji se koriste u matematici i uopće se ne oslanja na verbalni jezik. U mnogim slučajevima, riječi se zamjenjuju simbolima tako da se čak i nematematički formalni dokaz može razumjeti u obliku jednostavne simboličke logike bez upotrebe potencijalno dvosmislenih riječi.
Mnoga različita područja, obično u akademskim krugovima, koriste se formalnim dokazima. Najočitiji primjer je matematika, polje koje se uvelike temelji na korištenju dokaza. Slično, računalstvo se oslanja na korištenje strogih, formalnih logičkih progresija kako bi se osiguralo da se računalima daju apsolutno precizne upute. Filozofija, posebice analitička filozofija, također se oslanja na korištenje formalnih dokaza kako bi pokazala ispravnost različitih filozofskih tvrdnji u kontekstu različitih prethodno utvrđenih ili teorijskih premisa.