Une preuve formelle est une séquence d’énoncés, verbaux ou mathématiques, qui est utilisée pour démontrer la nécessité logique d’une conclusion donnée. De telles preuves nécessitent une utilisation rigoureuse et précise du langage, car l’ambiguïté linguistique peut facilement rendre une preuve dénuée de sens. Dans de nombreux cas, afin d’éviter ce problème, on peut présenter une preuve formelle symboliquement ou mathématiquement afin d’éviter autant que possible la confusion introduite par le langage. De telles preuves strictement formelles partent généralement d’une ou plusieurs prémisses théoriques ou bien établies. Ces prémisses sont suivies d’axiomes ou d’énoncés qui découlent logiquement des énoncés précédents des prémisses et se terminent par une conclusion finale ou un théorème prouvé qui, comme les énoncés précédents, est un résultat logiquement nécessaire des prémisses et des axiomes initiaux.
Contrairement à une preuve formelle, la plupart des arguments de la vie quotidienne reposent sur un langage courant et ne sont généralement pas logiquement rigoureux. Ils peuvent, par exemple, ne pas provenir d’un ensemble de prémisses bien construit, ou ils peuvent s’appuyer sur des appels rhétoriques – quant à l’émotion ou à l’autorité – qui n’ont pas leur place dans une preuve formelle. Alors qu’une preuve formelle est précieuse en raison de sa capacité à démontrer l’exactitude d’un énoncé basé sur un ensemble de prémisses, il est important de se rappeler que les preuves formelles ont peu ou pas d’utilité lorsqu’on discute de tout ce qui ne peut pas être démontré de manière concluante dans le domaine de la logique. . De plus, ils ne s’appliquent que dans le contexte des prémisses originales et ne démontrent donc pas des vérités universelles.
La plupart des preuves formelles sont basées sur un langage formel composé soit d’un sous-ensemble de langage normal, soit de symboles. Une preuve formelle mathématique, par exemple, est exprimée en utilisant les symboles utilisés en mathématiques et ne repose pas du tout sur le langage verbal. Dans de nombreux cas, des mots sont substitués aux symboles de sorte que même une preuve formelle non mathématique peut être comprise sous la forme d’une simple logique symbolique sans l’utilisation de mots potentiellement ambigus.
De nombreux domaines différents, généralement universitaires, utilisent des preuves formelles. L’exemple le plus évident est celui des mathématiques, un domaine qui repose en grande partie sur l’utilisation de preuves. De même, l’informatique repose sur l’utilisation de progressions logiques strictes et formelles afin de garantir que des instructions absolument précises sont données aux ordinateurs. La philosophie, en particulier la philosophie analytique, repose également sur l’utilisation de preuves formelles pour démontrer l’exactitude de diverses affirmations philosophiques dans le contexte de diverses prémisses théoriques ou établies précédemment.