Intersection Logic

The intersection type assignment system IT uses the formulas of the negative fragment of the predicate calculus (LJ) as types for the terms. However, the deductions of IT only correspond to the proper subset of the derivations of LJ obtained by imposing a meta-theoretic condition about the use of the conjunction of LJ. This paper proposes a logical foundation for IT. This is done by introducing a logic IL. Intuitively, a derivation of IL is a set of derivations in LJ such that the derivations in the set can be thought of as writable in parallel. This way of looking at LJ, by means of IL, means that the meta-theoretic condition mentioned above can be transformed into a purely structural property of IL. The relation between IL and LJ surely has a first main benefit: the strong normalization of LJ directly implies the same property on IL, which translates into a very simple proof of the strong normalizability of the terms typable with IT.