Skolemization in Simple Type Theory: the Logical and the Theoretical Points of View

Gilles Dowek (1)

1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique

Peter Andrews has proposed, in 1971, the problem of finding an analog of the Skolem theorem for Simple Type Theory. A first idea lead to a naive rule that worked only for Simple Type Theory with the axiom of choice and the general case has only been solved, more than ten years later, by Dale Miller. More recently, we have proposed with Thérèse Hardin and Claude Kirchner a new way to prove analogs of the Miller theorem for different, but equivalent, formulations of Simple Type Theory. In this paper, that does not contain new technical results, I try to show that the history of the skolemization problem and of its various solutions is an illustration of a tension between two points of view on Simple Type Theory: the logical and the theoretical points of view.

Domaines: Logique en informatique [cs.LO]

Gilles Dowek. Skolemization in Simple Type Theory: the Logical and the Theoretical Points of View. 2008. ⟨hal-04088449⟩