Driven by the question, 'What is the computational content of a
(formal) proof?', this book studies fundamental interactions
between proof theory and computability. It provides a unique
self-contained text for advanced students and researchers in
mathematical logic and computer science. Part I covers basic proof
theory, computability and Godel's theorems. Part II studies and
classifies provable recursion in classical systems, from fragments
of Peano arithmetic up to PI11-CA0. Ordinal analysis and the
(Schwichtenberg-Wainer) subrecursive hierarchies play a central
role and are used in proving the 'modified finite Ramsey' and
'extended Kruskal' independence results for PA and PI11-CA0. Part
III develops the theoretical underpinnings of the first author's
proof assistant MINLOG. Three chapters cover higher-type
computability via information systems, a constructive theory TCF of
computable functionals, realizability, Dialectica interpretation,
computationally significant quantifiers and connectives and
polytime complexity in a two-sorted, higher-type arithmetic with
linear logic.
General
Is the information for this product incomplete, wrong or inappropriate?
Let us know about it.
Does this product have an incorrect or missing image?
Send us a new image.
Is this product missing categories?
Add more categories.
Review This Product
No reviews yet - be the first to create one!