Gaisi Takeuti's book *Proof Theory* proves cut elimination for Simple Type Theory (a combined result of several researchers).  Thus it proves consistency of Simple Type Theory with full comprehension in each type and with cut as a proof rule.  I will abbreviate that consistency statement as Con(STT).  

Since different authors mean different things by Simple Type Theory I give a fuller description of Takeuti's meaning at the end of the post.  

Takeuti's result of interest to me is: 

> Conservativity Theorem: If you extend a first order theory $T$ to
> $\widetilde{T}$ by adding all finite higher types (with full
> comprehension, and cut rule) then  $\widetilde{T}$ is conservative
> over $T$.

 

My question: What metatheory is best for these results?

First, I believe that Exponential Function Arithmetic (EFA) can formalize the proof theory showing "If Con(STT) then the cut-free proof system for SST is complete."   I also believe EFA can formalize the unhypothetical theorem "extending any first order theory $T$ to $\widetilde{T}$ where only cut-free proofs are used in the type theory, is conservative." I have not checked these very well and when I look at the Reverse Math results on completeness of first order logic I see that depends on exactly how the theorem is stated -- and gives reason to think the cut elimination theorem for STT lies a bit above EFA.  But I hope the result is already known or at least already obvious to proof theorists. 


Second, I believe the straightforward choice of EFA plus Con(STT) is the best metatheory for this. So we regard cut elimination for STT, and the Conservativity Theorem, as depending on Con(STT) and not as proving it.   If my beliefs above are correct, then this metatheory is adequate and well suited to the task.  But is some better known, or more canonical, metatheory no stronger than this one yet still sufficient?

What Takeuti means by STT:  By Simple Type Theory Takeuti means logic of all finite orders, with $n$-ary operators to form  the  "subsets of the product" of any list of types, and not assuming an axiom of infinity (in the ground type or anywhere).  So this is not a substantial foundation.  Like First Order Logic it is a framework for inference with no substantial content in itself.  A theory in STT will have its own non-logical axioms.

He presents it using predicate terms, not as a lambda calculus.  He allows atomic predicate constants or variables in each typed arity, and formulas built from them. Any theory presented in this logic will have its own non-logical vocabulary.  Takeuti presents the proof system as a sequent calculus which actually has no axioms but has inference rules.  The Existential quantifier introduction rule implies that for every formula $A(x,y,z)$ there is a provable sequent 

> $\rightarrow\ \exists\varphi\ (\ \varphi(x,y,z) \equiv A(x,y,z)\ ).$

He calls this a comprehension axiom, but does not make it an axiom of the proof system.  Rather he derives it from the sequent rule.  Restrictions on comprehension (such as to make it predicative in various senses) are made by restricting the formulas allowed in Existential quantifier introduction.  By "full comprehension" he means no restrictions are made on the formulas in this rule (though of course all formulas must be correctly typed in the first place).