Bestiaire
Exemple 1
Ajout de a ⇒ b où a = a ⇒ b avec b quelconque.
Démonstration: Supposons a, comme a = a ⇒ b, on a a ⇒ b, et comme on a a on déduit b.
Utililsation
On a a ⇒ b et a = a ⇒ b, donc on a a.
Traduction
- On déduit a à partir de a ⇒ b car a = a ⇒ b . Problème : on utilise la vérité sur l'implication pour démontrer l'hypothèse.
- comme a = a ⇒ b, on a a ⇒ b, et comme on a a on déduit b. Problème : la preuve de l'implication applique l'application à prouver, donc si on la traduit on boucle.
Exemple 2
Ajout de ((1b = 1b) ⇒ a) ⇒ b avec a = (a ⇒ b) et b quelconque
Démonstration: Suppose que l'on ait (1b = 1b) ⇒ a. Comme 1b=1b, on déduit a. Comme a = (a ⇒ b), on déduit a ⇒ b et comme on a a, on déduit b.
Donc cette preuve contient la déduction d'utilisation de a ⇒ b.
Utililsation
Il nous faut montrer (1b = 1b) ⇒ a. Supposons 1b=1b, il nous faut montrer a. Comme a = (a ⇒ b) il nous suffit de montrer a ⇒ b. Pour cela supposons a. Nous avons (1b = 1b) ⇒ a, et comme on a ((1b = 1b) ⇒ a) ⇒ b on déduit b. Donc on a a ⇒ b, donc on a a, donc on a (1b = 1b) ⇒ a.
La preuve de l'hypothèse contient
- la déduction d'ajout de a ⇒ b, qui contient dans sa preuve:
◇ la déduction d'utilisation de ((1b = 1b) ⇒ a) ⇒ b
Traduction
- Il nous faut montrer (1b = 1b) ⇒ a. Supposons 1b=1b, il nous faut montrer a. Comme a = (a ⇒ b) il nous suffit de montrer a ⇒ b. Pour cela supposons a. Nous avons (1b = 1b) ⇒ a, et comme on a ((1b = 1b) ⇒ a) ⇒ b on déduit b. Donc on a a ⇒ b, donc on a a, donc on a (1b = 1b) ⇒ a. Problème : on utilise la vérité sur l'implication pour démontrer l'hypothèse.
- Comme (1b = 1b) ⇒ a et que 1b=1b, on déduit a. Comme a = (a ⇒ b), on déduit a ⇒ b et comme on a a, on déduit b.
Exemple 3
Ajout de ∀ i,x,y ;; ((i=imply) ∧ (x = (i x y))) ⇒ y
Démonstration similaire à l'exemple 1
Utilisation
On prend: i=imply, x = x ⇒ (1b = 0b), y = (1b = 0b)
Exemple 4
L'idée est de montrer l'importance du choix de la déduction d'ajout correspondante.
Ajout de (1b = 1b) ⇒ (1b = 1b)
Nous supposons 1b=1b et nous devons prouver 1b=1b. Pour cela nous montrons déjà (1b = 1b) ⇒ (1b = 1b) (de la manière normale), puis nous montrons 1b=1b, puis nous appliquons (1b = 1b) ⇒ (1b = 1b) et l'on déduit 1b=1b
Utilisation
On prouve 1b=1b puis on applique (1b = 1b) ⇒ (1b = 1b)
Traduction
On remplace la déduction d'application par la preuve p décrite ci-dessus de (1b = 1b) ⇒ (1b = 1b).
La traduction de p passe par une déduction d'application de (1b = 1b) ⇒ (1b = 1b). Si on utilisait le (1b = 1b) ⇒ (1b = 1b) principal, on aurait une boucle car pour traduire p on utiliserait p.
Exemple 5
Ajout de a ∨ (1b=1b) avec a = a ∨(1b=1b)
On prouve a ∨ (1b = 1b) puique l'on peut prouver 1b = 1b. Comme on a ∨ (1b=1b) = a et que l'on a a, on prouve a. Comme on a a, on déduit (par une autre déduction d'ajout) a ∨ (1b = 1b).
On a donc une déduction d'ajout de a ∨ (1b = 1b) à partir de a, qui est récursif et contenant une infinité de "or".
Utilisation
De a ∨ (1b=1b) on prouve 0b = 0b.
Traduction
Il me semble que l'on ne peut pas en déduire une mauvaise traduction mais on a néamoins déduit une formule infinie.
Si on utilise