Herbrand's Theorem, Skolemization and Proof Systems for First-Order Lukasiewicz Logic

Abstract. An approximate Herbrand theorem is established for firstorder infinite-valued Lukasiewicz Logic and used to obtain a proof-theoretic proof of Skolemization. These results are then used to define proof systems in the framework of hypersequents. In particular, a calculus lacking cut-elimination is defined for the first-order logic characterized by linearly ordered MV-algebras, a cut-free calculus with an infinitary rule for the full first-order Lukasiewicz Logic, and a cut-free calculus with finitary rules for its one-variable fragment.

• Type: Journal
• Year: 2010
• Where: LOGCOM
• Authors: Matthias Baaz, George Metcalfe
• Keywords: Cut-free Calculus, Infinite-valued Lukasiewicz Logic, LOGCOM 2010, Lukasiewicz Logic