Natural deduction for intuitionistic least and greatest fixedpoint logics : with an application to program construction

Sammanfattning: This thesis discusses intuitionistic least and greatest fixedpoint logics, i.e., intuitionistic systems of logic with primitive predicate-valued operators on predicate transformers that send monotone predicate transformers to their least and greatest fixedpoints, predicates being quasiordered by inclusion. It consists of an account of some aspects of their basic proof theory (natural deduction), accompanied by an envisagement of an application from typed functional pro gramming. In tomparison to classical least fixedpoint logits, which have received much attention in the research literature, as they have been found to be interesting both mathematitally (for example, in finite model theory) and from the point of view of practical utility (most remarkably in the verification of transition systems), the general interest in intuitionistic least and greatest fixedpoint logits seems to have been modest. This is somewhat surprising in the view of the handily conjecturable significance of the deductive systems for intuitionistic least and greatest fixedpoint logits for typed functional programming, which we try to cast some light upon. The treatment of intuitionistic logics in this thesis is exclusively proof-theoretical. This is so in the first place because we adhere to the position that the philosophically accurate intuitive semantics of intuitionistic systems of logic is proof semantics, of which tenable natural deduction (N.D.) systems (or, which is essentia lly the same, typed lambda calculi), for instance, are formalizations, but also sinte it is exactly the availability of such formalizations that actually makes intuitionistic logics matter for typed functional programming.We describe eight proof-theoretically defendable extensions of the customary N. D. system for the full intuitionistic 1st-order predicate logit with least and greatest fixedpoint oper ators enjoying the strong normalization and uniqueness of normal forms properties as well as a number of translations between these and from these into the customary N. D. system for the full intuitionistic 2nd-order predicate logit that preserve reductions between proofs. Four of these systems are variants of systems that have appeared in the literature; four are, to our knowledge, new. The exposition is centered around a tube-shaped taxonomy of the systems developed guided by the translation relationships. We argue that all eight systems can be interpreted as terminating and determinist ic systems of typed functional programming with primitive formers of inductive and coinductive types and employed an media for program construction from judgements-as-specifications. In particular, we illustrate on toy examples a technique for program construction in which judgements are put to work as specifications in a specific simplistic way, employing our systems as media. We also provide a short survey of the related work, which we divide into two blocks: the related work on classical least fixed point logics and their applications, and the relating work on deductive systems for intuitionistic logics and their programming applications.