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’s 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.
Abstract deduction and inferential models for type theory
MARTELLI, MAURIZIO
2010-01-01
Abstract
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’s 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.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
