Главная    Ex Libris    Книги    Журналы    Статьи    Серии    Каталог    Wanted    Загрузка    ХудЛит    Справка    Поиск по индексам    Поиск    Форум   
blank
Авторизация

       
blank
Поиск по указателям

blank
blank
blank
Красота
blank
Andrews P.B. — An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof
Andrews P.B. — An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof



Обсудите книгу на научном форуме



Нашли опечатку?
Выделите ее мышкой и нажмите Ctrl+Enter


Название: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof

Автор: Andrews P.B.

Аннотация:

This introduction to mathematical logic starts with propositional calculus and first-order logic. Topics covered include syntax, semantics, soundness, completeness, independence, normal forms, vertical paths through negation normal formulas, compactness, Smullyan's Unifying Principle, natural deduction, cut-elimination, semantic tableaux, Skolemization, Herbrand's Theorem, unification, duality, interpolation, and definability. The last three chapters of the book provide an introduction to type theory (higher-order logic). It is shown how various mathematical concepts can be formalized in this very expressive formal language. This expressive notation facilitates proofs of the classical incompleteness and undecidability theorems which are very elegant and easy to understand. The discussion of semantics makes clear the important distinction between standard and nonstandard models which is so important in understanding puzzling phenomena such as the incompleteness theorems and Skolem's Paradox about countable models of set theory. Some of the numerous exercises require giving formal proofs. A computer program called ETPS which is available from the web facilitates doing and checking such exercises. Audience: This volume will be of interest to mathematicians, computer scientists, and philosophers in universities, as well as to computer scientists in industry who wish to use higher-order logic for hardware and software specification and verification.


Язык: en

Рубрика: Математика/

Статус предметного указателя: Готов указатель с номерами страниц

ed2k: ed2k stats

Год издания: 1986

Количество страниц: 318

Добавлена в каталог: 24.04.2014

Операции: Положить на полку | Скопировать ссылку для форума | Скопировать ID
blank
Предметный указатель
$C_{\gamma0\gamma\gamma}$      184 211
$F_{0}$      160 163
$Inf^{III}$      257
$Inf^{II}$      202
$Inf^{I}$      202
$R_{\sigma\sigma\sigma(\sigma\sigma\sigma)}$      222
$S^{n}\mathbf{A}_{\sigma}$      209
$S_{n}$      247
$S_{\sigma\sigma}$      203 207
$T_{0}$      160 163
$\aleph_{0}$      87
$\alpha\beta$ Rule      56 57 168 169
$\bar{\sigma}$      232
$\chi$      210
$\Delta$      256 257
$\imath$      160 182
$\in$      47 157
$\iota$      160 162 182—184
$\lambda$      159 162 168 220
$\lambda$-conversion      159 168
$\mathbb{N}$      122 203
$\mathbf{D}^{d}$      146
$\mathbf{S}$      7 49
$\mathbf{\d{S}}$      49 165
$\mathcal{Q}^{n}_{0}$      260
$\mathcal{Q}^{\infty}_{0}$      203
$\mathcal{Q}^{\sigma}$      209
$\mathcal{Q}_{0\alpha\alpha}$      160 162
$\mathcal{Q}_{0}$      161—164
$\mathcal{R}$-derivation      128 129
$\mathcal{R}$-refutation      129
$\mathscr{A}$      250
$\mathscr{C}(\mathbf{A})$      32
$\mathscr{E}$      72
$\mathscr{F}$      45
$\mathscr{F}^{=}$      100—107
$\mathscr{F}^{\omega}$      154—156
$\mathscr{F}_{H}$      137
$\mathscr{F}_{t}$      128 149
$\mathscr{G}$      52 65 112 124
$\mathscr{G}\ell$      236
$\mathscr{H}$      57 109
$\mathscr{L}$      86 193
$\mathscr{N}$      108 258
$\mathscr{PRF}$      228
$\mathscr{PRR}$      228
$\mathscr{PR}$      229
$\mathscr{P}$      3 4 11 12
$\mathscr{P}(S)$      95 180
$\mathscr{S}_{1}$      126 127
$\mathscr{S}_{2}$      126 127
$\mathscr{V}$      17 76 77 134 175 186
$\mu$      218 220 234
$\omega$-complete      248 250 255
$\omega$-consistent      248 249 255
$\omega$-order logic      154
$\pi$      159 163
$\Sigma$      203 232
$\Sigma^{1}$      181
Aanderaa      138
Abbreviation      6 46 47 163
Abelian group      52 70 124
Abstract consistency class      89 90 128 129 149 150
Abstraction      159
AC      184
Addition      247
Adjacent      95
advice      68—70
Agree off      76
Algorithm      227
Alphabetic change of bound variable      110 168 169
Anderson      41
Andrews      127 132 137 138 160 186 197 200 265
Antiprenex      127
Antisignum      232
Appel      95
Arithmetic modulo      2 36
assertion      109
ASSIGNMENT      17 75 185
Association to the left      6 158 163
Associative      35 37
atomic      46
Axiom      3 6 10 11 156 164 202 203 207 216 242 243
Axiom of Choice      2 156 161 184 190 193 199 200 202
Axiom of infinity      156 190 201—203 207 209 216
Axiom schemata      51 156
Axiomatic set theory      95 100 157
Below      118
Bernays      202
Beth      117 152
Beth's definability theorem      152 153
Bledsoe      41
Bound      48 164
Bounded maximization      234
Bounded minimization      234 235
Bounded quantification      233
Brackets      6 47 163
Branch      118
C-instance      133
Cantor      184
Cantor's theorem      95 184 198
Card      87 193
cardinal number      201
Cardinality      87 193
cases      110
Categorical      257
cH-instance      135
Characteristic function      210
Choice function      218
choose      65
Church      27 53 160 227
Church's Theorem      53
Church's thesis      227 239 244 246 247 261 262
class      88
Clause      40
Closed      48 119 164
Closed under subsets      88
Coloring      95
Commutative      34
Compactness      37—40 95 96 100 198
Complementary      33
Complete induction      8
Completeness      22 30 93 94 100 193 248
composition      10 225
Compound Herbrand instance      135
Compound instance      133
Comprehension principle      156 157 159 179
Computable      246 247
Concatenation      4 7 236
Conjunction      48 159 160
Conjunction Elimination      119 129
Conjunction Introduction      113
Conjunctive normal form      28 29
Conjuncts      32
Connectives      27
Consequence      100
Conservative extension      86 124
Consis      252
Consistency      20 21 37—39 52 85 86 93 190 195 239 248 259 263
Constant      46 155
Continuum Hypothesis      156
Contradiction      17
Contradictory      18 77
Contrapositive law      68
Countable      87 97 190 193
Countable model      190
Counter-model      77
Craig      150
Craig — Lyndon Interpolation Theorem      150
Cut      41 128 129 139
Cut-elimination      116 138
Cut-free      116
Cwff      48 164
Davis      250
De Morgan's laws      31 33 34 48 61 68
Decidable      261
Decision problem      22 53 239
ded      109
Deduction rule      109
Deduction Theorem      15 59 178
Definable      152 239 264
Defines explicitly      152
Defines implicitly      152
Definition by cases      235
denote      46 185 186
Denton      138
Derivable      11
Derived rule of inference      13
description      160 162 165 181—184
Designate      25
Disagreement set      140
Disjoint      41
Disjunction      4 28 48 159
Disjunction Elimination      119
Disjunction Rules      113 128
Disjunctive component      112 128
Disjunctive normal form      28 29 32
Disjunctively valid      39
Distributive      29 34
divides      235
Domain      47 75 185
Dot      6 47 163
Double-Negation Elimination      119
Downward dyadic tree      118
Dreben      138
Duality      143—148
e      201 236
EDGE      95
Effectively computable      227
Elementarily equivalent      104
Elementary theory      52
Elementary wff      46
Elusive      266 267
Empty clause      40
Empty disjunction      128
Equality      100—107 155 160 166 181 210
Equality-interpretation      104
Equipollent      201
EQUIVALENCE      18 28 40 86 160
Essentially existential      123
Essentially incomplete      248 260
Essentially universal      123
Euclid      235
Excess literal      41
Exclusive disjunction      18
Existential closure      79
Existential constant      123
Existential generalization      62 110 113 179
Existential instantiation      65 119
Existential Rule      64 179
EXP      228
expand      109
expansion      86 193
Explicit definition      152 229 232
Expression      138
Extension      86
Extensionality      156 159 165
Extensionally complete      193
extent      236
f      27 35 36 128 149
FALSE      17 187
Falsehood      17 160
finite      7 38 39 203
Finite character      88 90
Finite intersection property      40
Finite model      190
Finite type theory      154
First-order logic      45 155
First-order theory      52
Formal theory      2
Formation rule      4 45 155
Formation sequence      9
Formula      4
Formulation      45
Four color theorem      95
Fourth-order logic      154 156
Frame      185
free      20 48 57 164
Free for      49 164
Free on      79
Frugal      87 195
Full conjunctive normal form      28
Full disjunctive normal form      28
Functional form      124
Functional variable      45
gen      51 57 172
General model      186
General recursive      225 235
Generalization      51 156
Gentzen      112 116 138
Gentzen's Hauptsatz      116
Gleason      228
Goedel      93 94 236 249 252
Goedel numbering      239—246
Goedel — Rosser Theorem      256 263 265
Goedel's completeness theorem      94
Goedel's incompleteness theorem      248 249 253
Goedel's second incompleteness theorem      250 252 255
Graph theory      95
Ground resolution      40—44
Haken      95
Henkin      93 150 160 190 222 253 254
Henkin's Completeness Theorem      197
Henkin's theorem      195 198 199
Herbrand      116 124 127 132
Herbrand expansion      138
Herbrand functor      124
Herbrand property      138
Herbrand universe      135
Herbrand's theorem      135—138
Higher-order logic      154—156
hilbert      238
Hilbert's program      238
Hilbert-style system      137
Hintikka      117
Huet      142
HYP      57 109 119
Hypothesis      11 57 109 165
Hypothesis Rule      109
i      155 162
Identity relation      104 185
if      19
IF-THEN-ELSE      184
Image      180
Implication      18 19
Improper symbol      4 45 155 162
INCLUDE      122
Inclusive disjunction      18
incomplete      239
Inconsistent      20 190
Independence      24—27 83 84
Indirect proof      68 108 109
Individual      155 185
Individual variable      45 155
Induction      5 8 9 17 96 202
Induction on the construction of a wff      5 17 46 162
Induction theorem      205
Infin      216 217
Infinitesimal      97
Initial function      225
1 2
blank
Реклама
blank
blank
HR
@Mail.ru
       © Электронная библиотека попечительского совета мехмата МГУ, 2004-2020
Электронная библиотека мехмата МГУ | Valid HTML 4.01! | Valid CSS! О проекте