Règle de coupure
From Wikipedia, the free encyclopedia
Cet article est une ébauche concernant la logique.
En logique mathématique, la règle de coupure est une règle d'inférence du calcul des séquents, qui généralise le modus ponens. Sa signification est que, si une formule A apparaît comme conclusion dans un séquent et comme hypothèse dans un autre, on peut alors inférer un séquent dans lequel la formule A n'apparaît pas.
Son écriture formelle en calcul des séquents est:
- coupure
Intuition
On peut s'imaginer la formule qui intervient dans la coupure comme ce que les mathématiciens appellent un « lemme ». Dans les prémisses, le premier séquent démontre le lemme, le deuxième séquent utilise le lemme. Dans la conclusion, le séquent résultant de la coupure, énonce comment les conclusions dépendent des hypothèses sans faire référence au lemme.
