Une démonstration de la complétude de LK

Jean Goubault-Larrecq

Nous allons donner une démonstration relativement courte de la complétude de LK. Les points essentiels seront décrits en section 1, mais la tentative de preuve qui y est décrite est erronée. Nous analyserons pourquoi, et réparerons la preuve en section 2.

Nous montrerons ensuite que la méthode des tableaux à variables libres avec règle d⁺⁺ est complète en section 3. Le résultat sera beaucoup plus fort, et montrera non seulement la complétude, mais encore qu'on n'a jamais besoin de coupure, ni de contraction (sauf sur les règles g), et que n'importe quelle stratégie d'expansion de tableaux est complète du moment qu'elle est équitable.

Une tentative presque réussie
La preuve réparée
Complétude de la méthode des tableaux
References

This document was translated from L^AT_EX by H^EV^EA.

This document was cut into pieces by H^AC^HA.