Since their inception, the Perspectives in Logic and Lecture Notes in Logic series have published seminal works by leading logicians. Many of the original books in the series have been unavailable for years, but they are now in print once again. Logicism, as put forward by Bertrand Russell, was predicated on a belief that all of mathematics can be deduced from a very small number of fundamental logical principles. In this volume, the twenty-third publication in the Lecture Notes in Logic series, Paul C. Gilmore revisits logicism in light of recent advances in mathematical logic and theoretical computer science. Gilmore addresses the need for languages which can be understood by both humans and computers and, using Intensional Type Theory (ITT), provides a unified basis for mathematics and computer science. This yields much simpler foundations for recursion theory and the semantics of computer programs than those currently provided by category theory.
Author(s): Paul C. Gilmore
Series: Lecture Notes in Logic 23
Publisher: Cambridge University Press
Year: 2017
Language: English
Pages: 249
Contents......Page 6
PREFACE......Page 10
1.1. Language and Logic......Page 20
1.2. Types, Terms, and Formulas......Page 21
1.3. Logical Connectives......Page 24
1.3.1. Choice of connectives......Page 25
1.4. Valuations......Page 26
1.4.1. Domains, valuations, and models......Page 28
1.5. The Lambda Abstraction Operator......Page 30
1.5.1. Syntax for quantification......Page 31
1.5.2. Semantics for abstraction terms......Page 32
1.5.3. Free and bound variables......Page 34
1.5.4. Substitutions and contractions......Page 35
1.6. Syntax and Semantics for EL......Page 38
1.7. Elementary Proof Theory......Page 39
1.7.1. Semantic rules for EL......Page 41
1.7.2. Derivation of a sequent......Page 42
1.7.3. Terminology for and properties of derivations......Page 43
1.7.4. Reusing derivations......Page 45
1.7.5. An alternative proof theory......Page 46
1.7.6. Derivations as binary trees of sequents......Page 47
1.7.7. Other formulations of first order logic......Page 50
1.8. Consistency of EL......Page 51
1.9. Completeness of EL......Page 52
1.9.1. A systematic search for a derivation......Page 54
1.9.2. A descending chain defines a counter-example......Page 56
2.1. The Type Theory TT......Page 62
2.1.1. The terms of TT......Page 63
2.2.1. Typing strings of characters......Page 65
2.2.2. Type expressions and their ranges......Page 66
2.2.3. String assignments and unification......Page 67
2.2.4. Polytyping TT......Page 70
2.3. Lambda Contractions......Page 74
2.4. The Proof Theory......Page 79
2.5. Intensional and Extensional Identity......Page 80
2.5.1. Extensional and intensional predicates......Page 82
2.5.2. Identity and string identity......Page 84
2.6.1. An extensional semantics for TT......Page 85
2.6.2. An intensional semantics for TT......Page 87
3.1.1. Motivation for secondary typing......Page 90
3.1.2. Secondary typing......Page 93
3.1.3. The normal form of a term of ITT......Page 94
3.2.1. A polytyping algorithm for ITT......Page 95
3.3.1. Domains and valuations......Page 98
3.3.3. Sequents and counter-examples......Page 103
3.4. Proof Theory for ITT......Page 104
3.4.2. Derivable rules for identity......Page 105
3.4.4. Properties of derivations......Page 106
3.5. Completeness of ITT......Page 107
3.5.1. A counter-example that is an intensional model......Page 109
3.6. SITT......Page 112
3.6.1. Types and Terms of SITT......Page 113
3.6.2. Lambda contractions......Page 114
3.6.5. Russell’s set......Page 115
4.1. Introduction......Page 118
4.2. Least and Greatest Predicate Operators......Page 120
4.3. Monotonic Recursion Generators......Page 122
4.3.1. Properties of monotonic recursion generators......Page 123
4.4.1. A zero and successor......Page 125
4.4.2. Nil and ordered pair......Page 126
4.4.3. Projections of ordered pair......Page 128
4.4.4. A recursion generator for the S-sequence......Page 129
4.4.5. Understanding Gt(RN)......Page 130
4.5. Continuous Recursion Generators......Page 134
4.6.2. Positive and e-positive occurrences of variables......Page 135
4.6.3. Monotonicity and continuity......Page 137
4.7.1. Horn sequents......Page 141
4.7.2. Simultaneous Horn sequents......Page 142
4.8. Definition by Iteration......Page 146
4.8.1. Defining Lt(RG) by iteration......Page 147
4.8.2. Defining Gt(RG) by iteration......Page 149
4.9.1. Characters and strings......Page 150
4.9.2. Lists......Page 151
4.9.3. Universal quantification......Page 152
5.1. Introduction......Page 156
5.1.1. A functional notation from choice terms......Page 157
5.2. Introducing Choice Terms......Page 159
5.2.1. The Relation >ε on terms of ITTε......Page 160
5.3. Proof Theory for ITTε......Page 162
5.4. Consistency and Completeness......Page 164
5.4.1. Completeness of ITTε......Page 166
5.5. Function Terms......Page 167
5.6. Partial Functions and Dependent Types......Page 168
6.1. Intuitionist/Constructive Mathematics......Page 170
6.2. A sequent calculus formulation ITTG of ITT......Page 171
6.3. An intuitionist formulation HITTG of ITTG......Page 173
6.3.1. Derivability in ITTG and HITTG......Page 174
6.4. Semantic Tree Formulation HITT of HITTG......Page 178
6.4.1. Properties of HITT derivations......Page 181
6.4.2. Equivalence of HITT and HITTG......Page 183
6.5.1. Forests of semantic trees......Page 186
6.6. Recursions in HITT......Page 189
7.1. Introduction......Page 190
7.2. Self-Applied Logic......Page 191
7.3.1. Abelian semi-groups......Page 192
7.3.2. Definitions......Page 193
7.3.4. Derivation of (SG)......Page 194
7.4. Set Theory and Logic......Page 198
7.4.1. A set theory formalized in ITT......Page 199
7.4.2. Cantor’s diagonal argument in ITT......Page 200
7.5. Why Is Mathematics Applicable?......Page 202
8.1. Introduction......Page 204
8.2. Definition, Derivation, and Computation......Page 208
8.3.1. Primitive Syntax......Page 210
8.3.2. Expressions......Page 211
8.3.3. Expression semantics......Page 212
8.3.4. Command semantics......Page 215
8.3.5. Example theorem......Page 220
8.4. Recursive Domains......Page 222
8.4.2. Finite functions and domain constructors......Page 223
8.4.3. Domain constructors......Page 224
8.4.4. Solving domain equations: an example......Page 229
8.5. Logical Support for Specification Languages......Page 232
References......Page 234
Index......Page 244
