 |
La logique intuitionniste (ou ses variantes plus fortes ou plus faibles) est au- jourd'hui presque universellement reconnue comme étant la logique de la preuve. Dans le présent texte, nous étudions une logique plus forte que la logique intui- tionniste (LI) : la logique intuitionniste avec négation forte (LINF) qui est une extension préservative de LI. En effet, tous les théorèmes de LI sont des théo- rèmes de LINF. Dans la deuxième section, nous allons d'abord présenter une axiomatisation à la Hilbert de LINF et discuter de la signification intuitive de la négation forte. Nous présentons brièvement le cadre canonique de Kripke pour cette axiomatisation, cadre basé sur l'ensemble des ensembles saturés déductive- ment clos, et affirmons que l'axiomatisation est fiable et complète pour ce cadre. Dans la troisième section, nous présentons un ensemble de règles de construction d'arbres de Beth pour vérifier la validité d'un énoncé quelconque de LINF. Nous montrons comment les arbres construisent des contre-modèles pour les énoncés non valides. Dans la quatrième et dernière section, nous introduisons la notion de modèle minimal et nous présentons une procédure pour définir des modèles canoniques minimaux à partir d'un arbre de Beth qui possède des chemins ouverts.
