Abstract deduction and inferential models for type theory

An inferential semantics for full Higher Order Logic (HOL) is proposed. The paper presents a constructive notion of model, that being able to capture relevant computational aspects is particularly suited for the applications of HOL to computer science. The inferential seman- tics is based on the introduction of new abstract deduction structures (ADS) that express the action of the Comprehension Axiom in a Higher Order Logic proof. The ADS\u2019s allow to define an inferential algebra of higher order potential proof-trees, endowed with two binary operations, the abstraction and the contraction, each consisting of constructive reductions between potential proofs. Typed formulas are interpreted by sequent trees, and the opera- tions between trees correspond to the logical connectives of the interpreted formula. Higher Order Logic is sound and complete w.r.t. the given inferential semantics