Skolem Functions

Skolem functions can be traced back to the famous paper by Thoralf Skolem (1920). Model theoretically they allow for the representation of abstract existential assumptions in axioms by concrete functions. Therefore, any mathematical theory has an open conservative extension. Proof theoretically Skolem functions can be used to eliminate strong quantifiers and thereby to reduce Herbrand`s theorem for arbitrary quantifier prefixes to its purely existential variant. lt is of course always possible to replace strong quantifiers by Skolem functions depending an the scope of weak quantifiers (or by any other function term), the problem is how to obtain the original formula from the Skolemized version in a correct way (reSkolemization). In this project we intend to develop and classify algorithms for reSkolemization in the settings of classical and intuitionistic logic. We intend to analyze mathematical proofs (especially the Schütte-van der Waerden solution to the Kissing Number Problem for dimension three) with respeet to trigonometric functions which we believe to represent Skolem functions in many relevant cases. The main result of the proposed project will lie in a deeper understanding of the proof theoretic impact of the presence of functions in mathematical proofs. This might have applications to all areas where Skolem functions are present, especially to automated theorem proving which most important variants as resolution calculus rely an open i.e. Skolemized formalisms.