January 24, 2022
Aurore Alcolei (LACL)Herbrand theorem is a cornerstone result for giving a computational meaning to first order classical formulas. The validity of a formula is equivalent to having a finite procedure able to choose witnesses to satisfy the formula in any model. Those witnesses are generally called Herbrand witnesses.
Hebrand witnesses can be extracted from proof sequents but unlike them they cannot be composed. This opens the way for investigations: what kind of missing ingredient should be added to the witnesses in order to make them composable? Can we avoid the sequent calculus bureaucracy while doing so?
In this talk I will propose a semantic answer to these questions: I will show how Herbrand witnesses can be viewed as term-strategies in an extended model of causal games, hence inheriting the composition procedure already embedded in this model.