Proofs and Computations

AvHelmut Schwichtenberg,Stanley S. Wainer

Inbunden, Engelska, 2011

1 078 kr

Beställningsvara. Skickas inom 5-8 vardagar. Fri frakt över 249 kr.

Beskrivning

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 Gödel'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.

Produktinformation

Utgivningsdatum:2011-12-15
Mått:160 x 236 x 30 mm
Vikt:860 g
Format:Inbunden
Språk:Engelska
Serie:Perspectives in Logic
Antal sidor:480
Förlag:Cambridge University Press
ISBN:9780521517690

Utforska kategorier

Matematikens grunder inom Naturvetenskap och teknik

Mer om författaren

Helmut Schwichtenberg is an Emeritus Professor of Mathematics at Ludwig-Maximilians-Universität München. He has recently developed the 'proof-assistant' MINLOG, a computer-implemented logic system for proof/program development and extraction of computational content. Stanley S. Wainer is an Emeritus Professor of Mathematics at the University of Leeds and a past-President of the British Logic Colloquium.

Recensioner i media

"Written by two leading practitioners in the area of formal logic, the book provides a panoramic view of the topic. This reference volume is a must for the bookshelf of every practitioner of formal logic and computer science." Prahladavaradan Sampath, Computing Reviews

Innehållsförteckning

Preface; Preliminaries; Part I. Basic Proof Theory and Computability: 1. Logic; 2. Recursion theory; 3. Godel's theorems; Part II. Provable Recursion in Classical Systems: 4. The provably recursive functions of arithmetic; 5. Accessible recursive functions, ID

Betyg & recensioner

5/5

5/5
Ett mästerverk inom metamatematiska monografier, en bok som kommer att stå sig som ett standardverk i många årtionden framöver. Lämplig även för den utan större tidigare kunskaper inom metalogiken, men kompletteras då med fördel med något annat standardverk, exempelvis Mendelsons "Introduction to Mathematical Logic".
Fredrik S
27 maj 2013