par application des règles, il faut bien
sûr que
soit vrai. Cela revient essentiellement à
vérifier que chaque règle est valide (et à une induction sur la
longueur de la preuve). Une autre question est de savoir
si ces règles sont ``suffisantes'' dans le sens où si
est vrai alors il existe une preuve utilisant les règles
précédentes de cela.
On peut aussi se poser la question de l'automatisation de
l'utilisation de ces règles: un ordinateur pourrait-il automatiquement
faire une telle preuve. (on peut noter que la règle de déduction permet
d'appliquer tous les théorèmes de la logique).