Mathematical logic and computation / Jeremy Avigad, Carnegie Mellon University.

Format:

Book

Author/Creator:

Avigad, Jeremy, author.

Language:

English

Subjects (All):

Logic, Symbolic and mathematical.

Physical Description:

1 online resource (xii, 513 pages) : digital, PDF file(s).

Edition:

1st ed.

Place of Publication:

Cambridge, United Kingdom ; Boca Raton : Cambridge University Press, 2023.

Summary:

This new book on mathematical logic by Jeremy Avigad gives a thorough introduction to the fundamental results and methods of the subject from the syntactic point of view, emphasizing logic as the study of formal languages and systems and their proper use. Topics include proof theory, model theory, the theory of computability, and axiomatic foundations, with special emphasis given to aspects of mathematical logic that are fundamental to computer science, including deductive systems, constructive logic, the simply typed lambda calculus, and type-theoretic foundations. Clear and engaging, with plentiful examples and exercises, it is an excellent introduction to the subject for graduate students and advanced undergraduates who are interested in logic in mathematics, computer science, and philosophy, and an invaluable reference for any practicing logician's bookshelf.

Contents:

Cover

Half-title page

Title page

Copyright page

Contents

Preface

Acknowledgments

1 Fundamentals

1.1 Languages and Structures

1.2 Inductively Defined Sets

1.3 Terms and Formulas

1.4 Trees

1.5 Structural Recursion

1.6 Bound Variables

Bibliographical Notes

2 Propositional Logic

2.1 The Language of Propositional Logic

2.2 Axiomatic Systems

2.3 The Provability Relation

2.4 Natural Deduction

2.5 Some Propositional Validities

2.6 Normal Forms for Classical Logic

2.7 Translations Between Logics

2.8 Other Deductive Systems

3 Semantics of Propositional Logic

3.1 Classical Logic

3.2 Algebraic Semantics for Classical Logic

3.3 Intuitionistic Logic

3.4 Algebraic Semantics for Intuitionistic Logic

3.5 Variations

4 First-Order Logic

4.1 The Language of First-Order Logic

4.2 Quantifiers

4.3 Equality

4.4 Equational and Quantifier-Free Logic

4.5 Normal Forms for Classical Logic

4.6 Translations Between Logics

4.7 Definite Descriptions

4.8 Sorts and Undefined Terms

5 Semantics of First-Order Logic

5.1 Classical Logic

5.2 Equational and Quantifier-Free Logic

5.3 Intuitionistic Logic

5.4 Algebraic Semantics

5.5 Definability

5.6 Some Model Theory

6 Cut Elimination

6.1 An Intuitionistic Sequent Calculus

6.2 Classical Sequent Calculi

6.3 Cut-Free Completeness of Classical Logic

6.4 Cut Elimination for Classical Logic

6.5 Cut Elimination for Intuitionistic Logic

6.6 Equality

6.7 Variations on Cut Elimination

6.8 Cut-Free Completeness of Intuitionistic Logic

7 Properties of First-Order Logic

7.1 Herbrand's Theorem

7.2 Explicit Definability and the Disjunction Property.

7.3 Interpolation Theorems

7.4 Indefinite Descriptions

7.5 Skolemization in Classical Theories

8 Primitive Recursion

8.1 The Primitive Recursive Functions

8.2 Some Primitive Recursive Functions and Relations

8.3 Finite Sets and Sequences

8.4 Other Recursion Principles

8.5 Recursion along Well-Founded Relations

8.6 Diagonalization and Reflection

9 Primitive Recursive Arithmetic

9.1 A Quantifier-Free Axiomatization

9.2 Bootstrapping PRA

9.3 Finite Sets and Sequences

9.4 First-Order PRA

9.5 Equational PRA

10 First-Order Arithmetic

10.1 Peano Arithmetic and Heyting Arithmetic

10.2 The Arithmetic Hierarchy

10.3 Subsystems of First-Order Arithmetic

10.4 Interpreting PRA

10.5 Truth and Reflection

10.6 Conservation Results via Cut Elimination

10.7 Conservation Results via Model Theory

11 Computability

11.1 The Computable Functions

11.2 Computability and Arithmetic Definability

11.3 Undecidability and the Halting Problem

11.4 Computably Enumerable Sets

11.5 The Recursion Theorem

11.6 Turing Machines

11.7 The Lambda Calculus

11.8 Relativized Computation

11.9 Computability and Infinite Binary Trees

12 Undecidability and Incompleteness

12.1 Computability and Representability

12.2 Incompleteness via Undecidability

12.3 Incompleteness via Self-Reference

12.4 The Second Incompleteness Theorem

12.5 Some Decidable Theories

13 Finite Types

13.1 The Simply Typed Lambda Calculus

13.2 Strong Normalization

13.3 Confluence

13.4 Combinatory Logic

13.5 Equational Theories

13.6 First-Order Theories and Models

13.7 Primitive Recursive Functionals

13.8 Propositions as Types.

Bibliographical Notes

14 Arithmetic and Computation

14.1 Realizability

14.2 Metamathematical Applications

14.3 Modified Realizability

14.4 Finite-Type Arithmetic

14.5 The Dialectica Interpretation

15 Second-Order Logic and Arithmetic

15.1 Second-Order Logic

15.2 Semantics of Second-Order Logic

15.3 Cut Elimination

15.4 Second-Order Arithmetic

15.5 The Analytic Hierarchy

15.6 The Second-Order Typed Lambda Calculus

15.7 Higher-Order Logic and Arithmetic

16 Subsystems of Second-Order Arithmetic

16.1 Arithmetic Comprehension

16.2 Recursive Comprehension

16.3 Formalizing Analysis

16.4 Weak Kőnig's Lemma

16.5 ∏ [(1/1)] Comprehension and Inductive Definitions

16.6 Arithmetic Transfinite Recursion

17 Foundations

17.1 Simple Type Theory

17.2 Mathematics in Simple Type Theory

17.3 Set Theory

17.4 Mathematics in Set Theory

17.5 Dependent Type Theory

17.6 Inductive Types

17.7 Mathematics in Dependent Type Theory

Appendix A Background

A.1 Naive Set Theory

A.2 Orders and Equivalence Relations

A.3 Cardinality and Zorn's Lemma

A.4 Topology

A.5 Category Theory

References

Notation

Typographical conventions

Symbols

Index.

Notes:

Title from publisher's bibliographic system (viewed on 09 Sep 2022).

ISBN:

1-108-80076-9

1-108-77875-5

OCLC:

1350687966