Some, but not all, closed terms of the lambda calculus have types; these types are exactly the theorems of intuitionistic implicational logic. An extension of these simple (?) types to intersection (or ??) types allows all closed lambda terms to have types. The corresponding ?? logic, related to the Meyer-Routley minimal logic B+ (without ?), is weaker than the ?? fragment of intuitionistic logic. In this paper we provide an introduction to the above work and also determine the ?? logics that correspond to certain interesting subsystems of the full ?? type theory.