O dovadă formală este o succesiune finită de propoziții (numite formule bine formate în cazul unui limbaj formal ), fiecare dintre acestea fiind o axiomă , o ipoteză sau rezultă din propozițiile precedente din secvență printr-o regulă de inferență . Ultima propoziție a secvenței este o teoremă a unui sistem formal . Noțiunea de teoremă nu este, în general, eficientă, de aceea nu există nicio metodă prin care să găsim de fiecare dată o dovadă a unei propoziții date sau să determinăm dacă există una. Conceptul de deducție naturală este o generalizare a noțiunii de demonstrație.
Teorema este o consecință sintactică a tuturor formulelor bine formate care o preced în dovadă. Pentru ca o formulă bine formată să fie prezentă într-o demonstrație, aceasta trebuie să fie rezultatul aplicării unei reguli a aparatului deductiv.
Dovezile formale sunt adesea construite folosind computerele ca asistenți de dovedire . În mod semnificativ, aceste dovezi pot fi verificate automat, de asemenea, de către computer. Verificarea dovezilor formale este, în general, simplă, în timp ce găsirea probelor ( dovada automată a teoremelor ) este, în general, intratabilă pe computer și / sau doar semidecidibilă, în funcție de sistemul formal utilizat.
Un limbaj formal este un set de suite finisate în simboluri . Un astfel de limbaj poate fi definit fără referire la semnificațiile oricăreia dintre expresiile sale; poate exista înainte să i se atribuie o interpretare - adică un sens. Demonstrațiile formale sunt exprimate în limbaj formal.
O gramatică formală (numită și reguli de formare ) este o descriere exactă a formulelor bine formate ale unui limbaj formal. Este setul de șiruri peste alfabetul limbajului formal care constituie formule bine formate. Cu toate acestea, nu descrie semantica lor (adică, ce înseamnă).
Un sistem formal (numit și calcul logic sau sistem logic ) constă dintr-un limbaj formal împreună cu un sistem deductiv . Sistemul deductiv poate fi alcătuit dintr-un set de reguli de transformare (numite și reguli de inferență ) sau un set de axiome , sau ambele. Un sistem formal este utilizat pentru a obține o expresie din una sau mai multe alte expresii.
O interpretare a unui sistem formal este atribuirea semnificației simbolurilor și a valorilor secvențelor unui sistem formal. Studiul interpretărilor se numește semantică formală . A da o interpretare este sinonim cu construirea unei structuri .