Lazi

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