Completeness and cut-elimination theorems for high-order classical logic. Constructive method (Q1901891)

We are interested in the relation of the truth in models and the deducibility (both with cuts and without cuts) in theories of higher order, i.e., in theories with type-theoretic structure, with (in general, impredicative) the axiom of convolution and, probably, with the axiom of extensionality. We offer a special form of Boolean-valued or Heyting- valued semantics for these theories, which is used for the proof of completeness theorems and cut-elimination theorems. Our main purpose is constructivity of the metamathematics we apply.