Certain operations are definable in type-free lambda-calculus, and polymorphic lambda-calculus, but not in simple types. Similarly, some logical constructions are possible in classical logic and higher-order, but not propositional, intuitionistic logic. These facts are often related via the Curry-Howard isomorphism. This talk will collect some observations concerning definablity of logical connectives and data types in various logics and lambda-calculi.