# Logic and Computation

Share this page *Edited by *
*Wilfried Sieg*

This volume contains the proceedings of the Workshop on Logic and Computation, held in July 1987 at Carnegie-Mellon University. The focus of the workshop was the refined interaction between mathematics and computation theory, one of the most fascinating and potentially fruitful developments in logic. The
importance of this interaction lies not only in the emergence of the computer
as a powerful tool in mathematics research, but also in the various attempts to
carry out significant parts of mathematics in computationally informative ways.

The proceedings pursue three complementary aims: to develop parts of mathematics under minimal set-theoretic assumptions; to provide formal frameworks suitable for computer implementation; and to extract, from formal proofs, mathematical and computational information. Aimed at logicians, mathematicians, and computer scientists, this volume is rich in results and replete with mathematical, logical, and computational problems.

# Table of Contents

## Logic and Computation

- Contents vii8 free
- Preface ix10 free
- Some theories conservative over intuitionistic arithmetic 116 free
- Ramsey interpreted: A parametric version of Ramsey's theorem 1732
- Notions of closed subsets of a complete separable metric space in weak subsystems of second order arithmetic 3954
- A note on polynomial time computable arithmetic 5166
- Axiomatizations and conservation results for fragments of bounded arithmetic 5772
- A smash-based hierarchy between PTIME and PSPACE 85100
- Polymorphic typed lambda-calculi in a type-free axiomatic framework 101116
- Polynomial time computable arithmetic 137152
- Metaprogramming in SIL 157172
- W K Lo and orderings of countable abelian groups 177192
- Marriage theorems and reverse mathematics 181196
- Computationally based set existence principles 197212
- Hierarchy results for mixed-time 213228
- Polynomial time equivalence types 221236
- Program development through proof transformation 251266
- Some models of Scott's theory LC F based on a notion of rate of convergence 263278
- Sharply bounded arithmetic and the function a -1 281296
- Radon-nikodym theorem is equivalent to arithmetical comprehension 289304