HAUPTSATZ, logique mathématique

Article

• DÉMONSTRATION THÉORIE DE LA

  • Écrit par Jean-Yves GIRARD
  • 6 140 mots
  • 1 média
  Théorème d'élimination des coupures (Hauptsatz de Gentzen). Dans LK, la règle de coupure (C) est inutile, autrement dit tout théorème de LK est démontrable sans coupures.La démonstration de ce résultat, assez longue et délicate, consiste à remplacer toute coupure de formule principale A par...