Dérivation hypothétique vs séquent

[Hibou57]

Ça concerne les démonstrations en général, mais je crois que les gens versés dans les maths savent peut‑être aussi (si des gens en connaissent, ne vous privez pas de les taguer s’ils acceptent d’être dérangés pour ça).

Je me demande quelle est la différence entre une dérivation hypothétique dans la déduction naturelle et un séquent dans le calcul des séquents. Comme je les comprend, c’est la même chose, et alors je ne comprends pas pourquoi les deux sont distingués. J’imagine que ce n’est pas qu’une question de notation.

Je patauge depuis des plombes à essayer de savoir où est la différence, je suis désespère de comprendre.

 

[Hibou57]

Je n’en suis pas entièrement sûr, mais il me semble que dans la déduction naturelle, la décharge de la preuve et la dérivation hypothétique, désignent la même chose.

Ave les séquents, on peut désigner un contexte (à gauche du ⊢ ), pas avec une décharge de la preuve (ou si ?).

Une décharge de la preuve, je la comprend comme « ceci étant prouvé par ailleurs », c’est à dire dans un autre système logique ou de calcul. Un séquent, c’est finalement la même chose quand on parle par exemple de jugement syntaxique. Le jugement syntaxique, c’est finalement équivalent à « ceci étant prouvé par ailleurs », parce que la grammaire du langage des termes n’est pas du domaine du système de démonstration (même si on peut l’y introduire).

En gros, les séquents sont juste une notation qui permet plus de précisions en permettant d’indiquer d’où vient cette preuve faite ailleurs ? (et d’en faire usage par exemple en supposant la combinaison de deux contextes ou l’augmentation d’un contexte)

Si les deux sont bien la même chose (modulo la précision mentionnée plus haut), alors je les comprends comme des points de connection entre des systèmes de démonstration différents.

C’est ça ?

 

[Hibou57]

En plus, les séquents sont autant fréquents dans la déduction naturelle que dans le calcul des séquents; il ne faut pas se laisser tromper par les deux noms. Je n’ai toujours pas de réponse absolument certaine à la question, et en plus je m’en pose une autre, mais je ne la dis pas, ce serait encore plus en vain

 

[Hibou57]

Je n’en suis pas entièrement sûr, mais il me semble que dans la déduction naturelle, la décharge de la preuve et la dérivation hypothétique, désignent la même chose.

[…]

Ben non. La décharge de la preuve signifie que l’hypothèse doit être ignorée. Je me demande alors à quoi ça sert de le noter, il doit y avoir une raison, je me demande laquelle.

Some leaves of the tree are discharged (denoted by [Ci]), meaning that they are not to be considered hypotheses. If all leaves are discharged, then the conclusion holds without hypotheses (it will be the case, for example, of every propositional tautology).

Source : Notes for the Proof Theory Course (univ-paris13.fr) [PDF].

— Édit —

Voilà à quoi ça sert :

[…] the hypotheses A have been “discharged”, i.e., they are no longer hypotheses of the proof […]

J’imagine que c’est pour ne pas s’encombrer.

 

[Hibou57]

[…]
Je me demande quelle est la différence entre une dérivation hypothétique dans la déduction naturelle et un séquent dans le calcul des séquents. Comme je les comprend, c’est la même chose, et alors je ne comprends pas pourquoi les deux sont distingués. J’imagine que ce n’est pas qu’une question de notation.

[…]

Une réponse à cette question se trouve dans le document du précédent message : les séquents s’utilisent dans une certaines formulation de la déduction naturelle; c’est expliqué à la page 6. Il y a aussi une réponse implicite à la question sur le sens de la décharge des hypothèses : en comparant la page 3 et la page 6, j’ai l’impression que les hypothèses déchargées dans la déduction naturelle sans séquents, correspondent aux hypothèses s’ajoutant au contexte, dans la formulation avec des séquents; ça se voit avec les deux formulations de l’introduction de l’implication et les deux formulations de l’élimination de disjonction.

Je rapporte juste pour ne pas laisser des questions que j’ai posé, sans réponses, alors que j’ai fini par trouver les réponses.

Ceci dit, je me demande maintenant quel est l’intérêt d’avoir ces deux formulations différentes … seulement une différence de notation ou plus que ça ?