| dbo:abstract
|
- Le calcul des propositions est un calcul logique restreint. On emploie souvent le nom de proposition pour désigner une formule logique non quantifiée. Il existe deux façons de valider une formule du calcul des propositions :
* ou bien on montre que cette formule est vraie dans tout modèle (voir ci-dessous). On dit alors que est une tautologie, et on note .
* ou bien on montre que cette formule est prouvable ou dérivable en utilisant un système de déduction, et on note . Un système de déduction correct doit être construit de façon que, à partir de formules vraies (tautologies), on puisse déduire d'autres formules vraies. Dans ce cas, si est vérifié, alors l'est également. Le système de déduction sera complet, si inversement, il permet de déduire toute formule vraie. Autrement dit, si est vérifié, le système de déduction doit permettre de démontrer qu'on a également . Le théorème de complétude du calcul des propositions énonce que les systèmes de déduction, décrits dans les articles calcul des propositions ou déduction naturelle ou calcul des séquents, sont complets.Il y a équivalence entre être une tautologie et être prouvable. Le théorème de complétude du calcul des propositions classique a été démontré par Paul Bernays en 1926. (fr)
- Le calcul des propositions est un calcul logique restreint. On emploie souvent le nom de proposition pour désigner une formule logique non quantifiée. Il existe deux façons de valider une formule du calcul des propositions :
* ou bien on montre que cette formule est vraie dans tout modèle (voir ci-dessous). On dit alors que est une tautologie, et on note .
* ou bien on montre que cette formule est prouvable ou dérivable en utilisant un système de déduction, et on note . Un système de déduction correct doit être construit de façon que, à partir de formules vraies (tautologies), on puisse déduire d'autres formules vraies. Dans ce cas, si est vérifié, alors l'est également. Le système de déduction sera complet, si inversement, il permet de déduire toute formule vraie. Autrement dit, si est vérifié, le système de déduction doit permettre de démontrer qu'on a également . Le théorème de complétude du calcul des propositions énonce que les systèmes de déduction, décrits dans les articles calcul des propositions ou déduction naturelle ou calcul des séquents, sont complets.Il y a équivalence entre être une tautologie et être prouvable. Le théorème de complétude du calcul des propositions classique a été démontré par Paul Bernays en 1926. (fr)
|
