George Metcalfe

Density elimination

Abstract: Elimination of the cut rule is a fundamental topic in Proof Theory, corresponding to the removal of lemmas from proofs. However, the addition and elimination of other rules also merit investigation. In this talk I will consider one such rule, important in the meta-mathematics of Fuzzy Logic: the so-called ``density rule'' of Takeuti and Titani. Adding this rule to axiomatizations for certain classes of substructural logics guarantees completeness with respect to dense linearly ordered algebras. Density elimination, performed on corresponding Gentzen systems, then establishes this completeness property for the original axiomatizations. The method provides an interesting example of a proof-theoretic proof of an algebraic result where no algebraic proof is known.