000			02417nam a22003858i 4500
001			CR9781139031905
003			UkCbUP
005			20200124160234.0
006			m|||||o||d||||||||
007			cr||||||||||||
008			110223s2012||||enk o ||1 0|eng|d
020			_a9781139031905 (ebook)
020			_z9780521517690 (hardback)
040			_aUkCbUP _beng _erda _cUkCbUP
050		4	_aQA9.54 _b.S39 2012
082	0	4	_a511.352 _223
100	1		_aSchwichtenberg, Helmut, _d1942- _eauthor.
245	1	0	_aProofs and computations / _cHelmut Schwichtenberg, Stanley S. Wainer.
246	3		_aProofs & Computations
264		1	_aCambridge : _bCambridge University Press, _c2012.
300			_a1 online resource (xiii, 465 pages) : _bdigital, PDF file(s).
336			_atext _btxt _2rdacontent
337			_acomputer _bc _2rdamedia
338			_aonline resource _bcr _2rdacarrier
490	1		_aPerspectives in logic
500			_aTitle from publisher's bibliographic system (viewed on 05 Oct 2015).
520			_aDriven 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.
650		0	_aComputable functions.
650		0	_aProof theory.
700	1		_aWainer, S. S., _eauthor.
710	2		_aAssociation for Symbolic Logic, _eissuing body.
776	0	8	_iPrint version: _z9780521517690
830		0	_aPerspectives in logic.
856	4	0	_uhttps://doi.org/10.1017/CBO9781139031905
999			_c517946 _d517944