000 | a | ||
---|---|---|---|
999 |
_c32211 _d32211 |
||
008 | 231011b xxu||||| |||| 00| 0 eng d | ||
020 | _a9781108986908 | ||
082 |
_a511.3 _bBEL |
||
100 | _aBell, John L. | ||
245 | _aHigher-order logic and type theory | ||
260 |
_bCambridge University Press, _c2022 _aCambridge : |
||
300 |
_a79 p. ; _bill., _c23 cm |
||
365 |
_b17.00 _cGBP _d109.80 |
||
490 | _aCambridge elements. Elements in philosophy and logic | ||
504 | _aIncludes bibliographical references. | ||
520 | _aThis Element is an exposition of second- and higher-order logic and type theory. It begins with a presentation of the syntax and semantics of classical second-order logic, pointing up the contrasts with first-order logic. This leads to a discussion of higher-order logic based on the concept of a type. The second Section contains an account of the origins and nature of type theory, and its relationship to set theory. Section 3 introduces Local Set Theory (also known as higher-order intuitionistic logic), an important form of type theory based on intuitionistic logic. In Section 4 number of contemporary forms of type theory are described, all of which are based on the so-called 'doctrine of propositions as types'. We conclude with an Appendix in which the semantics for Local Set Theory - based on category theory - is outlined. | ||
650 | _aLogic | ||
650 | _aSymbolic and mathematical | ||
650 | _aSet theory | ||
650 | _aType theory | ||
942 |
_2ddc _cBK |