Intersection Types as Logical Formulae