HTLC: Hyperintensional Typed Lambda Calculus

In this paper we introduce the logic HTLC, for Hyperintensional Typed Lambda Calculus. The system extends the typed lambda-calculus with hyperintensions and related rules. The polymorphic nature of the system allows to reason with expressions for extensional, intensional and hyperintentsional entities. We inspect meta-theoretical properties and show that HTLC is complete in Henkin's sense under a weakening of the cardinality constraint for the domain of hyperintensions.