Algebraic and logistic investigations on free lattices [Algebraische und logistische Untersuchungen über freie Verbände]

Lorenzen, Paul

HAL, hal-01620945 / Harvested from HAL

Résumé

Les ``Recherches algébriques et logistiques sur les treillis libres'' de Lorenzen sont parues en 1951 dans The journal of symbolic logic. Ces ``Recherches'' ont immédiatement fait époque dans la théorie de la démonstration infinitaire, mais leur approche et méthode de démonstration n'ont pas été reprises. Plus précisément, Lorenzen prouve l'admissibilité de la coupure par double récurrence sur la formule de coupure et sur la complexité des dérivations sans recourir aux ordinaux, au contraire de la présentation de l'élimination des coupures dans la plupart des textes de référence en théorie de la démonstration. Nous proposons une traduction avec l'intention de donner une nouvelle impulsion à leur réception.Les ``Recherches'' sont surtout connues pour fournir une preuve constructive de non-contradiction de la théorie des types ramifiée sans axiome de réductibilité. Elles montrent qu'elle forme une partie d'un ``calcul inductif'' trivialement non contradictoire qui décrit notre connaissance de l'arithmétique sans détour. La preuve n'utilise que la définition inductive des formules et des théorèmes.Elles proposent aussi une définition d'un demi-treillis, d'un treillis distributif, d'un demi-treillis pseudocomplémenté et d'une algèbre de Boole dénombrablement complète comme des calculs déductifs, et montrent comment les présenter pour construire l'objet respectif librement engendré par un ensemble préordonné.Cette traduction est publiée avec l'aimable autorisation de la fille de Lorenzen, Jutta Reinhardt.

Détail

Publié le : 2017-10-26
Classification:  consistency of ramified type theory without axiom of reducibility,  free countably complete boolean lattice,  infinitary proof theory,  omega-rule,  free pseudocomplemented semilattice,  free semilattice,  free distributive lattice,  cut-elimination,  demi-treillis pseudocomplémenté libre,  treillis distributif libre,  demi-treillis libre,  théorie de la démonstration infinitaire,  élimination des coupures,  Paul Lorenzen,  induction,  algèbre de Boole dénombrablement complète libre,  non-contradiction de la théorie des types ramifiée sans axiome de réductibilité,  oméga-règle,  03G10; 01A60; 03-03; 03F05; 03F25; 03F65; 06-03; 06A12; 06B25; 06D05; 06E05; 06E10,  [MATH.MATH-LO]Mathematics [math]/Logic [math.LO],  [MATH.MATH-GM]Mathematics [math]/General Mathematics [math.GM],  [MATH.MATH-HO]Mathematics [math]/History and Overview [math.HO]