A mechanization of type theory

Abstract

A refutational system of logic for a language of order w ia presented. This langage is a slight modification of Church's \\-calculus with types. The system is complete, in the sense that a refutation of a set of sentences exists if and only if this set does not possess a general Henkin model. The main rule of inference is a generalization of Robinson's resolution to type theory, which allows us to get rid of the substitution rule.