Density Elimination and Rational Completeness for First-Order Logics

Density elimination by substitutions is introduced as a uniform method for removing applications of the Takeuti-Titani density rule from proofs in firstorder hypersequent calculi. For a large class of calculi, density elimination by this method is guaranteed by known sufficient conditions for cut-elimination. Moreover, adding the density rule to any axiomatic extension of a simple first-order logic gives a logic that is rational complete; i.e., complete with respect to linearly and densely ordered algebras: a precursor to showing that it is a fuzzy logic (complete for algebras with a real unit interval lattice reduct). Hence the sufficient conditions for cut-elimination guarantee rational completeness for a large class of first-order substructural logics.

• Type: Conference
• Year: 2007
• Where: LFCS
• Authors: Agata Ciabattoni, George Metcalfe
• Keywords: Density Elimination, Density Rule, LFCS 2007, Takeuti-Titani Density Rule