Abstract

Il s’agit d’une methode qui permet d’associer à chaque formule bien formée du système S5 de logique modale un nombre naturel invariant pour toutes les formules qui appartiennent a la même classe d’equivalence que la première.En particulier, étant donné que la méthode associe à toutes les tautologies du système le nombre o et a toutes les contradictions du système un certain nombre Φ, il suffit de calculer le nombre qui, en vertu des associations fondamentales, reste associé à n’importe quelle formule pour décider si cette dernière est tautologique, contradictoire ou contingente.Les relations logiques reliant deux formules du systeme -par exemple, des implications, des incompatibilités, des oppositions contradictaires, etc.- sont révéciés par un simpIe examen oculaire des nombres assoc iés aux formules données et une rapide vérification manuelle ou informatique fondée sur la comparaison des chiffres du même rang de ces nombres, écrits en hexadécimal.Finalement, l’analyse de la composition binaire du nombre associé a une formule donnée permet d’obtenir l’expression de la première sous sa forme normale conjonctive.La méthode décrite constitue donc une nouvelle méthode arithmétique de décision pour le système modal indiqué