Continuity, proof systems and the theory of transfinite computations

Abstract

We use domains with totality, density and co-density to define transfinite proof-systems, generalising omega-logic and in some sense, the beta-logic of Girard. We prove a cut elimination theorem for these logical systems. The main application is the developement of E-logic, a transfinite proof systems for recursion in the functional ^3E.