Get the latest tech news
Practical Foundations of Mathematics
Taylor Practical Foundations of Mathematics Practical Foundations of Mathematics Cambridge University Press INTRODUCTION I FIRST ORDER REASONING - - Introduction - 1.1 - Substitution - 1.2 - Denotation and Description - 1.3 - Functions and Relations - 1.4 - Direct Reasoning - 1.5 - Proof Boxes - 1.6 - Formal and Idiomatic Proof - 1.7 - Automated Deduction - 1.8 - Classical and Intuitionistic Logic - - Exercises I II TYPES AND INDUCTION - - Introduction - 2.1 - Constructing the Number Systems - 2.2 - Sets (Zermelo Type Theory) - 2.3 - Sums, Products and Function-Types - 2.4 - Propositions as Types - 2.5 - Induction and Recursion - 2.6 - Constructions with Well Founded Relations - 2.7 - Lists and Structural Induction - 2.8 - Higher Order Logic - - Exercises II III POSETS AND LATTICES - - Introduction - 3.1 - Posets and Monotone Functions - 3.2 - Meets, Joins and Lattices - 3.3 - Fixed Points and Partial Functions - 3.4 - Domains - 3.5 - Products and Function-Spaces - 3.6 - Adjunctions - 3.7 - Closure Conditions and Induction - 3.8 - Modalities and Galois Connections - 3.9 - Constructions with Closure Conditions - - Exercises III IV CARTESIAN CLOSED CATEGORIES - - Introduction - 4.1 - Categories - 4.2 - Actions and Sketches - 4.3 - Categories for Formal Languages - 4.4 - Functors - 4.5 - A Universal Property: Products - 4.6 - Algebraic Theories - 4.7 - Interpretation of the Lambda Calculus - 4.8 - Natural Transformations - - Exercises IV V LIMITS AND COLIMITS - - Introduction - 5.1 - Pullbacks and Equalisers - 5.2 - Subobjects - 5.3 - Partial and Conditional Programs - 5.4 - Coproducts and Pushouts - 5.5 - Extensive Categories - 5.6 - Kernels, Quotients and Coequalisers - 5.7 - Factorisation Systems - 5.8 - Regular Categories - - Exercises V VI STRUCTURAL RECURSION - - Introduction - 6.1 - Free Algebras for Free Theories - 6.2 - Well Formed Formulae - 6.3 - The General Recursion Theorem - 6.4 - Tail Recursion and Loop Programs - 6.5 - Unification - 6.6 - Finiteness - 6.7 - The Ordinals - - Exercises VI VII ADJUNCTIONS - - Introduction - 7.1 - Examples of Universal Constructions - 7.2 - Adjunctions - 7.3 - General Limits and Colimits - 7.4 - Finding Limits and Free Algebras - 7.5 - Monads - 7.6 - From Semantics to Syntax - 7.7 - Gluing and Completeness - - Exercises VII VIII ALGEBRA WITH DEPENDENT TYPES - - Introduction - 8.1 - The Language - 8.2 - The Category of Contexts - 8.3 - Display Categories and Equality Types - 8.4 - Interpretation - - Exercises VIII IX THE QUANTIFIERS - - Introduction - 9.1 - The Predicate Convention - 9.2 - Indexed and Fibred Categories - 9.3 - Sums and Existential Quantification - 9.4 - Dependent Products - 9.5 - Comprehension and Powerset - 9.6 - Universes - - Exercises IX BIBLIOGRAPHY INDEX.
Practical Foundations of Mathematics Introduction 1.1 Substitution 1.2 Denotation and Description 1.3 Functions and Relations 1.4 Direct Reasoning 1.5 Proof Boxes 1.6 Formal and Idiomatic Proof 1.7 Automated Deduction 1.8 Classical and Intuitionistic LogicExercises IIntroduction 2.1 Constructing the Number Systems 2.2 Sets (Zermelo Type Theory) 2.3 Sums, Products and Function-Types 2.4 Propositions as Types 2.5 Induction and Recursion 2.6 Constructions with Well Founded Relations 2.7 Lists and Structural Induction 2.8 Higher Order LogicExercises IIIntroduction 3.1 Posets and Monotone Functions 3.2 Meets, Joins and Lattices 3.3 Fixed Points and Partial Functions 3.4 Domains 3.5 Products and Function-Spaces 3.6 Adjunctions 3.7 Closure Conditions and Induction 3.8 Modalities and Galois Connections 3.9 Constructions with Closure ConditionsExercises IIIIntroduction 4.1 Categories 4.2 Actions and Sketches 4.3 Categories for Formal Languages 4.4 Functors 4.5 A Universal Property: Products 4.6 Algebraic Theories 4.7 Interpretation of the Lambda Calculus 4.8 Natural TransformationsExercises IVIntroduction 5.1 Pullbacks and Equalisers 5.2 Subobjects 5.3 Partial and Conditional Programs 5.4 Coproducts and Pushouts 5.5 Extensive Categories 5.6 Kernels, Quotients and Coequalisers 5.7 Factorisation Systems 5.8 Regular CategoriesExercises VIntroduction 6.1 Free Algebras for Free Theories 6.2 Well Formed Formulae 6.3 The General Recursion Theorem 6.4 Tail Recursion and Loop Programs 6.5 Unification 6.6 Finiteness 6.7 The OrdinalsExercises VIIntroduction 7.1 Examples of Universal Constructions 7.2 Adjunctions 7.3 General Limits and Colimits 7.4 Finding Limits and Free Algebras 7.5 Monads 7.6 From Semantics to Syntax 7.7 Gluing and CompletenessExercises VIIIntroduction 8.1 The Language 8.2 The Category of Contexts 8.3 Display Categories and Equality Types 8.4 InterpretationExercises VIIIIntroduction 9.1 The Predicate Convention 9.2 Indexed and Fibred Categories 9.3 Sums and Existential Quantification 9.4 Dependent Products 9.5 Comprehension and Powerset 9.6 UniversesExercises IX
Or read this on Hacker News