Constructive Version of Herbrand’s Theorem for First-Order Łukasiewicz Logic
Jin Wei
Matthias Baaz and George Metcalfe [1] provided a hypersequent calculus for infinite Łukasiewicz logic which is sound and complete with respect to \([0,1]\)-truth valued semantics and admits cut elimination. This result is further extended to first-order Łukasiewicz logic [2]. However, the cut elimination proof passes through semantics and the constructive information is missing. In particular, a proof with cut does not lead directly to a cut-free proof other than guarantees the existence of one.
The core ingredient of their proof is an approximate version of Herbrand’s theorem for first-order Łukasiewicz logic where a compactness argument is being used. Since Herbrand’s theorem is essentially a \(\Pi_2\)-statement, proof mining technique should be applicable here, provide a quantitative version of the theorem, and give an explicit upper bound for term witnesses of existence quantifiers. In this talk, I will describe my current progress in finding a constructive version of approximate Herbrand’s theorem for first-order Łukasiewicz logic. It will also be mentioned how this will contribute to a ultimate syntactic cut elimination proof, as well as some potential applications to continuous model theory.
Bibliography
- Matthias Baaz, George Metcalfe,Herbrand’s theorem, skolemization and proof systems for first-Order Łukasiewicz logic,Journal of Logic and Computation,vol. 20 (2010), no. 1, pp. 35–54.
- George Metcalfe, Nicola Olivetti, Dov Gabbay,Sequent and hypersequent calculi for abelian and Łukasiewicz logics,ACM Transactions on Computational Logic,vol. 6 (2005), no. 3, pp. 578–613.
- Petr Hájek,Metamathematics of Fuzzy Logic,Kluwer,1998.
- Ulrich Kohlenbach, Paulo Oliva,Proof mining: a systematic way of analysing proofs in mathematics,Proceedings of the Steklov Institute of Mathematics,vol. 9 (2002), no. 31.