Peter B. Andrews, "Resolution In Type Theory," Journal of Symbolic Logic, Vol. 36, No. 3, Sept. 1971, 414-432.

The author introduces three systems: T, elementary type theory--essentially Church's system of type theory with only axioms 1-6; G, which is a formulation eliminating the cut-rule (he proves G is equivalent to T by using Smullyan's Unifying Principle and Abstract Consistency); and a resolution-style refutation system R. Cut-elimination for Schutte's [Schutte 1960] (relational) formulation of type theory was first proven by Takahashi [Takahashi 1967].

He gives a proof that all wff's have a unique (up to alpha-conversion) lambda-normal (i.e., beta-reduced) form by induction on the complexity of types involved in beta-redex's. Then, he associates wff's A with their lambda-normal form eta-A (where variables are chosen in a methodical way to ensure uniqueness). Abstract Consistency is modified for the higher-order setting by requiring of the class that if S union {A} is in the class then S union {eta-A} is in the class (and we treat forall as the pi operator). A semivaluation assigns a truth value to some wff's in a way which respects lambda-conversion, logical connectives, and quantifiers. Given any member S of an abstract consistency class, there is a semivaluation for which all members of S map to t (proven by a standard extension argument).

For every semivaluation V, the set {A | VA=t} is consistent. This is proven by constructing a "general model" where the domains are V-complexes--i.e., pairs of eta-wff's and values "agreeing" with the semivaluation V. This provides a notion of general model appropriate for T (elementary type theory).

It follows that every "abstract consistent" set is consistent.

Then, what can be considered the main result of the paper, the cut-elimination theorem for elementary type theory is proven. System G is introduced. The axioms are excluded middle for each atomic wff. The rules of inference are alpha conversion, beta expansion, rearrangement of disjunction components, weakening, negation introduction, conjunction introduction, existential generalization and universal generalization. (So, the idea is that we start from simple tautologies and "build" the theorem by introduction-style rules.) It follows easily that every theorem of G is a theorem of T. The converse implies cut-elimination (since G is cut-free). In order to prove the converse, preliminary lemmas giving beta-reduction, elimination-style rules and simplification as derived rules are proven. These results are used to prove that the class of finite sets of wff's {A1,...,An} for which G does not prove "-A1 or . . . or -An" is an abstract consistency class. If T proves A, then -A has no model, so {-A} is not in the abstract consistency class above, and so G proves --A, thus G proves A. This proof relies on a semantic argument using Smullyan's Unifying Principle.

The final system, system R, is a resolution-style refutation system for sets of sentences based on alpha-conversion, beta-reduction, rearrangement of disjunctive components, simplification, negation and conjunctive elimination, existential instantiation (using a choice function ["existential parameter"] at each type to create Skolem terms), universal instantiation, substitution and cut. He proves that if a sentence is refutable in T, then it is refutable in R, by using Smullyan's Unifying Principle applied to the class of sets of wff's which are not refutable in R (after variables are replaced by new constants). [Note: in Andrews 1974, a new refutation system B is introduced which introduces new parameters to perform existential instantiation instead of using choice functions as system R does. The difference between the systems is that the negation of the axiom of choice can be refuted in R, but not in B. A wff is provable in T iff it is refutable in B. So, system R is stronger than B, and hence T.]

Systems G and R are, in some sense, dual. System G starts from simple tautologies (excluded middle for atomic wffs) and builds the theorem using "expansion/introduction/generalization" rules. System R starts from a formula to refute and derives a contradiction using "reduction/elimination/instantiation/substitution/cut" rules. System T is a Hilbert-style system (in the sense that we axiomatize propositional logic using a few tautologies and derive the rest from these using modus ponens).

The results and proofs in this paper concerning systems G and R are analogous to the results for first-order systems proven in Andrews 1986, Chapter 3.

The search for refutations in R is compared and contrasted to the search for resolution refutations in first-order logic. The most obvious differences are beta-reduction and the fact that substitution may introduce new logical constants, so that the application of rules which reduce the problem to a set of clauses cannot be solely a preprocessing step.

Finally, the author gives examples of refutations in R including a proof that the successor of a natural is a natural (taking successor and zero as primitive constants and "naturals" defined in terms of these) and the fixed-point theorem example (if an iterate of f has a unique fixed point, then f has a fixed point--he uses derived equality rules for reflexivity and replacement for this proof).