Calcul des séquents

[Anonyme]

Bonjour,

J'aimerais savoir où je pourrais trouver la démonstration (au propre)
de la propriété d'élimination des coupures dans le calcul des séquents
(de Gentzen). A défaut, je serais très reconnaissant si quelqu'un peut
me donner l'idée (à propos, mon objectif est de comprendre pourquoi le
théorème est vrai en logique linéaire, donc si je peux trouver
directement la preuve dans le cadre de la logique linéaire, c'est
encore mieux).

Merci beaucoup.

[Anonyme]

On 5 Jun 2004 05:16:31 -0700, Anonyme wrote:
>Bonjour,
>
>J'aimerais savoir où je pourrais trouver la démonstration (au propre)
>de la propriété d'élimination des coupures dans le calcul des séquents
>(de Gentzen). A défaut, je serais très reconnaissant si quelqu'un peut
>me donner l'idée (à propos, mon objectif est de comprendre pourquoi le
>théorème est vrai en logique linéaire, donc si je peux trouver
>directement la preuve dans le cadre de la logique linéaire, c'est
>encore mieux).

Euh, je ne sais plus comment Gentzen a fait sa preuve, mais ça devait
être une preuve assez syntactique et peu digeste. Je dirais, mais je
ne suis pas 100 % certain, que tu dois pouvoir trouver sa preuve dans
"From Frege to Godel", Harvard University Press. (Je crois). C'est
un bouquin génial pour qui s'intéresse de près ou de loin à la logique.

Si j'ai bonne mémoire (et il est possible que je me trompe
radicalement), pour la logique linéaire on utilise les réseaux
de preuve. On montre d'abord que tout réseau correspond à une
preuve, puis le contraire, puis on examine ce que sont les coupures
dans les reseaux de preuve, et on termine. Oui, je sais, c'est
un peu vague, comme description. Le cours de Roberto di Cosmo,
disponible sur Internet, donne tous les détails, il me semble.

http://www.pps.jussieu.fr/~dicosmo/CourseNotes/LinLog/


--
Frédéric