Please note: In order to keep Hive up to date and provide users with the best features, we are no longer able to fully support Internet Explorer. The site is still available to you, however some sections of the site may appear broken. We would encourage you to move to a more modern browser like Firefox, Edge or Chrome in order to experience the site fully.

Proofs and Computations, Hardback Book

Hardback

Description

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 Goedel's theorems.

Part II studies and classifies provable recursion in classical systems, from fragments of Peano arithmetic up to 11-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 11-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.

Information

  • Format:Hardback
  • Pages:480 pages, 8 Line drawings, unspecified
  • Publisher:Cambridge University Press
  • Publication Date:
  • Category:
  • ISBN:9780521517690

£71.99

 
Free Home Delivery

on all orders

 
Pick up orders

from local bookshops

Information

  • Format:Hardback
  • Pages:480 pages, 8 Line drawings, unspecified
  • Publisher:Cambridge University Press
  • Publication Date:
  • Category:
  • ISBN:9780521517690