Speaker
Jin Wei
University of Pennsylvania
Talks at this conference:
Tuesday, 17:20, J335 
Constructive Version of Herbrand’s Theorem for FirstOrder Łukasiewicz Logic 
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 firstorder Ł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 cutfree proof other than guarantees the existence of one. The core ingredient of their proof is an approximate version of Herbrand’s theorem for firstorder Ł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 firstorder Ł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
