# 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*,,vol. 20 (2010), no. 1, pp. 35–54.*Journal of Logic and Computation* - George Metcalfe, Nicola Olivetti, Dov Gabbay,
*Sequent and hypersequent calculi for abelian and Łukasiewicz logics*,,vol. 6 (2005), no. 3, pp. 578–613.*ACM Transactions on Computational Logic* - Petr Hájek,
,Kluwer,1998.*Metamathematics of Fuzzy Logic* - Ulrich Kohlenbach, Paulo Oliva,
*Proof mining: a systematic way of analysing proofs in mathematics*,,vol. 9 (2002), no. 31.*Proceedings of the Steklov Institute of Mathematics*