6.5 Définir les autres opérateurs
Contexte
On a définit par des extensions ∀, ∃ et ⇒. Mais pour les autres connecteurs logiques ?
Question
Comment, à partir des mots clés, définir ⊤,⊥,∧, ∨, ¬ ?
Étude
Définir T et ⊥ pour avoir ¬ T = ⊥ et ⊥ = ¬ ⊤ ?
Si on les définit comme ça T = (1b = 1b) et ⊥ = (1b = 0b), on n'a pas les égalités souhaitées.
Si ⊥ = (1b = 0b), (¬ x) = (x ⇒ ⊥) et ⊤ = (¬ ⊥) :
Mais alors ¬⊤ = ((1b = 0b) ⇒ (1b = 0b)) ⇒ (1b = 0b), qui n'est pas égal à 1b = 0b.
On voit qu'il faudrait une récurrence pour arriver à nos fins. On doit avoir T = ¬ ¬ ⊤, donc T = ( ⊤ ⇒ ⊥ ) ⇒ ⊥. Par récurrence on obtient une formule récursive mais où la parité des implications pour savoir si c'est vrai ou faux. C'est trop tordu.
Donc il fait laisser tomber les égalités et utiliser l'équivalence logique. De toute manière on n'a pas d'égalité entre propositions en général.
Définitions
T = (1b = 1b)
⊥ = (1b = 0b)
(x ∧ y) = ∀ b | (if b 1b 1b = 1b) ⇒ $T[x,y] b
(x ∨ y) = ∃ b | (if b 1b 1b = 1b) ∧ $T[x,y] b
(x ⇔ y) = ((x ⇒ y) ∧ (y ⇒ x))
(¬ x) = (x ⇒ ⊥)
Remarques
⊥ et T
On a ∀ x |⊥ ⇒ x. On le montre en utilisant if 0b a b = if 1b a b sous l'hypothèse 1b = 0b.
On n'a ni (¬ T) = ⊥ ni ⊥ = (¬ ⊤).
∧
On voit facilement que x ∧ y ⇒ x et x ∧ y ⇒ y : on prend b = 1b et b = 0b.
∨
Montrons que si on a x ⇒ z et y ⇒ z alors on a (x ∨ y) ⇒ z :
Supposons les conditions. Soit b tq (if b 1b 1b = 1b) ∧ $T[x,y] b. On a if b 1b 1b = 1b. On utilise la règle du tiers exclus :
Supposons b = 0b. On a $T[x,y] b, donc on a x. Comme x ⇒ z on a z.
Donc par la règle du tiers exclu, on déduit z.
¬
(¬ T) = (T ⇒ ⊥)
On n'a pas à prioris ¬ ¬ x ⇒ x, ce qui fait que l'on a des problèmes si on définissait classiquement ∧ et ∨ en fonction de ⇒
Regardons le cas ¬ ¬ x sous la condition x ∨ (¬ x) :
On a trivialement x ⇒ x.
D'après la propriété de ∨ démontrée ci-dessus, on a x ∨ (¬ x) ⇒ x. Donc on déduit x.
Réponse
Voir les définitions.