next up previous contents
Next: Comparaison avec la physique Up: Phénoménologies de l'objet Previous: De la vérité à

La Σ1-restriction

L'affaiblissement de l'idée de Théétète, qui affaiblit la vérité par la possibilité, ne suffit pas pour la phénoménologie de la physique. Les états d'esprit ``atomiques" sont les états des machines löbiennes atteints par le déployeur universel. Il faut en tenir compte. On peut argumenter que ces états correspondent aux arrêts possibles des machines possibles, et, en terme de propositions, sont analogues aux énoncés Σ1 (de la forme ∃n P(n) avec P récursif). On peut trouver dans [Vickers, 1989] une motivation implicite pour un concept similaire d'observation (voir aussi [Abramsky, 1987]). Avec la thèse de Church l'ensemble des propositions Σ1, qui existe indépendamment de nous avec le réalisme arithmétique, constitue un déployeur universel abstrait. On peut donc raisonnablement espérer isoler une logique de ``l'observable" en restreignant la logique des énoncés prouvable et consistant sur les réalisations arithmétiques Σ1. Cela revient à restreindre l'interprétation arithmétique des variables propositionnelles des formules modales aux énoncés arithmétiques Σ1. Les machines löbiennes prouvent leur propre Σ1-complétude. Plus précisément elle prouve les formules:

p →Bew(p )

où p désigne un énoncé Σ1. Visser a démontré que le système, que j'appelle V, comprenant les théorèmes de G accompagné de la formule p →p et fermé pour le modus ponens et la nécessitation, axiomatise complètement la logique de la prouvabilité où les formules atomiques sont restreintes aux énoncés Σ1 [Visser, 1985]. Il convient toutefois d'affaiblir la règle de substitution aux énoncés atomiques. Par exemple, on ne peut pas remplacer p par dans p →p. En fait, l'interprétation arithmétique de est Π1 Σ1. Si p représente un énoncé Σ1, alors l'interprétation arithmétique de p est aussi Σ1. On peut donc substituer p par p, p, etc. On obtient à nouveau une théorie V* complète pour la vérité de ces propositions en abandonnant la nécessitation et en complétant la théorie avec la formule de réflexion T (p →p). Notons que V* prouve p ↔p, mais (heureusement) V* ne prouve pas (p ↔p). Pourquoi heureusement ? Car si V* prouvait les nécessitations de p →p, la logique V* collapserait avec le calcul propositionnel. On peut montrer que V et V* sont décidables. Pour isoler la part prouvable et la part vraie correspondant à la phénoménologie de la matière il suffit d'appliquer à la fois la restriction Σ1 de Visser et l'affaiblissement de l'idée de Théétète sur la prouvabilité ``Bew" gödélienne. Cela revient à étudier le couple de logiques Z1 = KDX3 et Z1* = KBX4 qui correspondent aux logiques du où p est interprété par

Bew(p ) & Bew(p )

Avec p Σ1. B est la formule p → p. Dans les modèles de Kripke, elle correspond à la symétrie de la relation d'accessibilité du référentiel qui la respecte. V et V* permettent de construire un démonstrateur de théorèmes pour les parts communicables et non-communicables respectivement. Ceci est rendu possible grâce aux théorèmes de complétude pour V et V* de Visser (Visser 1985). X3 et X4 désigne à nouveau les formules (peut-être en nombre infini) nécessaires pour obtenir un résultat de complétude. La partie prouvable est donc obtenue ainsi:

Z1 = KDX3 = {A V DEON(A)}

La partie vraie (prouvable ou non prouvable) est obtenue ainsi:

Z112139* = KBX4 = {A V12139* DEON(A)}

Comme pour G et G*, ainsi que Z et Z*, et à la différence de S4Grz ou de IL, la différence est non vide. Cette différence, Z1* Z1, suggère une interprétation arithmétique des qualia ``arithmétiques". Cela donne en effet une logique de propositions non-communicables, concernant des énoncés ``immédiatement observables". Remarque. Je précise que tous les théorèmes de complétude arithmétique cités jusqu'ici concernent les logiques modales propositionnelles. On peut démontrer qu'au niveau des logiques du premier ordre aucune des théories modales n'admettent une extension décidable complète. Précisons quelques points. On consultera l'annexe A pour une brève introduction à la sémantique de Scott-Montague. On pourrait se demander ce que donnerait la Σ1-restriction sur le sujet, vu à la troisième personne (S4Grz). L'idée est de capturer une notion de sensation vraie. On obtient une logique S4GrzΣ1 qui possède tous les axiomes et qui est fermée pour toutes les règles d'inférence. Cette logique collapse. Elle prouve l'équivalence de toutes formules avec leur nécessitation et leur possibilisation. Autrement dit S4GrzΣ1 est égale au calcul propositionnel. Son carré est strictement équivalent au non-arithmétisable, et donc non diagonalisable, prédicat de vérité. Je montre plus loin que tout espoir n'est pas perdu pour une notion de sensation vraie. Z1*, comme V*, frôle le collapse, en ce sens que, pour les formules atomiques p, Z1* prouve p ↔ p (V* prouve p ↔p), mais même pour les formules atomiques le collapse est évité car Z1* ne prouve pas (p ↔ p). Notons que Z1 ne prouve ni p → p, ni p →p. Ceci montre en particulier que Z1* Z1 est non vide. Ce qui évite le collapse à Z1*, est l'absence de fermeture pour la nécessitation. Et cette absence résulte de l'exigence de la consistance de l'extension et de la non-prouvabilité gödélienne de la consistance. Ni G, ni V ne prouvent ∧. Aucune des logiques Z ne sont fermées pour la nécessitation. Les logiques Z et Z1 admettent cependant une sémantique de Scott-Montague (voir plus bas). On utilisera le fait que p est équivalent à p qui est équivalent à (p ∧p) qui est équivalent à (p ∨p) qui est équivalent à p ∨p qui est équivalent à p ∨ p. Dans le tableau suivant je donne quelques résultats qui étendent les nuances intensionnelles décrites plus haut. La formule ``Dual T" est la duale modale de T: p →p. Elle est introduite pour distinguer Z de Z1. G ne prouve pas p → p, même pour p atomique (par exemple p = ) et donc Z ne prouve pas p →p. V prouve p → p, pour p atomique puisque, pour p atomique, V prouve p →p, et donc V prouve p → p ∨p.
G G* S4Grz(*) Z Z* Z1 Z1* S4GrzΣ1
T - + + - + - + +
Nec + - + - - - - +
Diag + + - + + + + -
N + + + - + - + +
RM + - + + - + - +
B - - - - - - + +
4 + + + - - - - +
D - + + + + + + +
5 - - - - - - - +
dual T - + + - + + + +
Z est fermé pour la règle de monotonie RM: {A →BA →B} % DEUX 211 Preuve. D'abord G est fermé pour RM. En effet, par une simple application de la nécessitation et de K, on a la fermeture de G pour {p →qp →q}. A présent pour Z, cela découle du fait que (q ∧p) ∧(p →q) entraîne q. Et cela vaut a fortiori pour Z1, où les p et q sont limités aux formules atomiques. Cela entraîne encore que Z et Z1 sont fermés pour la règle RE {p ↔qp ↔q}. Grâce à quoi, ces logiques bénéficient d'une sémantique de Scott-Montague. Z* n'est pas fermé pour RM, ni pour RE. On vérifie en effet facilement que Z* ↔, mais Z* ↔. Ceci n'est pas étonnant. G* lui-même n'est pas fermé pour RE et RM, puisque G* ↔, mais G* ↔. Z* démontre N: Z* , et T: Z* p →p. Je suis la nomenclature de Chellas où N désigne la règle d'adjonction de la formule . Z* est une conséquence directe de G* . Et Z* est une conséquence (classique) directe de G* p →p. Z* est donc une extension de KT-, KT sans Nécessitation, et pourrait être proposé pour une forme de connaissance immédiate et incorrigible de la part d'une machine. Ce résultat montre que Z est strictement inclus dans Z*. Question. ÊEst-il possible d'obtenir une axiomatisation de Z* à partir de Z + T + la suppression de RM? On montre facilement que Z^* p →p. Donc Z non plus puisque Z ⊂Z^*. Z Z_1 perdent la fermeture pour la nécessitation, elles admettent cependant une sémantique de Scott-Montague. Il est facile de se convaincre qu'elles prouvent en outre les formules K, M, R, où: K est l'axiome de Kripke, (p →q) → (p →q) M est la formule (p ∧q) →(p ∧ q), R est la formule (p ∧q) →(p ∧q). Cela est aisé à vérifier. Notons que les logiques Z, sont décidables, puisque G et G^* le sont. Le fait que les formules M et R sont des théorèmes permet de montrer que pour les mondes α, les systèmes de voisinages de Scott-Montague N(α) sont des quasi-filtres: