The pleasures of anticipation: Enriching intuitionistic logic

We explore a relation we call 'anticipation' between formulas, where A anti cipates B (according to some logic) just in case B is a consequence (accord ing to that logic, presumed to support some distinguished implicational con nective -->) of the formula A -->B. We are especially interested in the cas e in which the logic is intuitionistic (propositional) logic and are much c oncerned with an extension of that logic with a new connective, written as 'a', governed by rules which guarantee that for any formula B, aB is the (l ogically) strongest formula anticipating B. The investigation of this new l ogic, which we call ILa, will confront us on several occasions with some of the finer points in the theory of rules and with issues in the philosophy of logic arising from the proposed explication of the existence of a connec tive (with prescribed logical behaviour) in terms of the conservative exten sion of a favoured logic by the addition of such a connective. Other points of interest include the provision of a Kripke semantics with respect to wh ich ILa is demonstrably sound, deployed to establish certain unprovability results as well as to forge connections with C. Rauszer's logic of dual int uitionistic negation and dual intuitionistic implication, and the isolation of two relations (between formulas), head-implication and head-linkage, wh ich, though trivial in the setting of classical logic, are of considerable significance in the intuitionistic context.