A Gentzen-Style Proof System for First-Order Łukasiewicz Logic and Its Completeness

Abstract: Continuous model theory for metric structures is grounded in first-order Łukasiewicz logic and thus inherits an Hilbert-style axiomatization. However, the syntactic study with this proof system encounters difficulties, mainly the failure of the deduction theorem due to issues with contraction. Gentzen-style proof systems for Łukasiewicz Logic have been developed to address these challenges, with hypersequent calculi for propositional and first-order Łukasiewicz Logic introduced by Metcalfe, Olivetti, and Gabbay (2005) and Baaz and Metcalfe (2010). In this talk, I will give a brief introduction to their work and present my own result establishing the first-order completeness. I will also discuss potential directions of research, including syntax cut elimination and the development of a constructive fragment of Łukasiewicz Logic, with potential applications to continuous logic.

logic

Audience: researchers in the topic

Online logic seminar

Series comments: Description: Seminar on all areas of logic