zbMATH — the first resource for mathematics

Herbrand’s theorem, Skolemization and proof systems for first-order Łukasiewicz logic. (English) Zbl 1188.03014
Authors’ abstract: “An approximate Herbrand theorem is established for first-order infinite-valued Łukasiewicz 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 Łukasiewicz logic, and a cut-free calculus with finitary rules for its one-variable fragment.”

03B50 Many-valued logic
03F05 Cut-elimination and normal-form theorems
06D35 MV-algebras
Full Text: DOI