Lazi

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 ⊤ = (¬ ⊥) :

Donc ⊤ = ( (1b = 0b) ⇒ (1b = 0b) ).
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 = 1b. On a $T[x,y] b, donc on a y. Comme y ⇒ z on a z.
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.
CQFD

¬

(¬ 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 (¬ x) ⇒ ⊥ et comme ⊥ ⇒ x, on a ¬ 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.