In 1978, Girard introducedβ-logic to generalizeω-logic. The basic category ofβ-logic is the categoryON of ordinals. For geometric structure reasons, Girard changed the basic categoryON into the more general categoryWF of well-founded orders (1983). The logic he obtained was calledΩ-logic. Here, we extend (unpublished) results ofβ-logic toΩ-logic.

Vauzeilles, J., Cut elimination for the Unified Logic, Annals of Pure and Applied Logic 62 1-16. In the paper entitled “On the Unity of Logic” Girard introduced and motivated the system LU. In Girard's article, the cut-elimination result for LU is stated and used as a key lemma, but not supported by any rigourous proof. In the present paper, we prove that LU enjoys cut elimination under minimal hypotheses: a notion of degree for a formula is introduced, which depends only (...) on the number of exponentials of the formula; this refinement yields much better bounds for cut elimination and leaves open many possibilities as to non-well-foundedness of formulae. (shrink)

Dans cet article, on utilise la théorie des dilatateurs pour décrire les premiers récursivement inaccessible et Mahlo.