Szabo M. E. — Algebra of proofs :: Электронная библиотека попечительского совета мехмата МГУ

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

Авторизация

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

Szabo M. E. — Algebra of proofs

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

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

Название: Algebra of proofs

Автор: Szabo M. E.

Аннотация:

The book itself contains a wealth of technical detail that includes
many dozens of claims whose proofs are not worked out in detail. I'm
writing to ask whether anyone has any knowledge about the degree to
which this work was refereed and/or whether the results have been
verified independently. I'm appealing especially to those who work in
categorical logic or those interested in automatic proof verification
in category theory, both of which groups, it would seem, should be
interested in Szabo's work.

Язык:

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

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

ed2k: ed2k stats

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

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

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

Операции: Положить на полку | Скопировать ссылку для форума | Скопировать ID

Предметный указатель

Active formula      20
Adjoint functor      10
Adjunction      10 97
Adjunction, counit of an      10 97
Adjunction, unit of an      10 97
Admissible (rule of inference)      29
Algebra, boolean      148
Algebra, Heyting      148
Algebra, quantifier      201
Algorithm, cut elimination      20 229—243
Algorithm, normalization      244—277
AND      2
Antecedent      17
Antecedent symbol      20
Application (of a rule of inference)      29
arrow      4 12
Arrow, De Morgan      147—151
Arrow, finitarily representable      211
Arrow, identity      4 5 13 20 220
Arrowgram      5
Atomic formula      16 203
Axiom      19 206—207 219—220 224
Bicartesian category      54
Bicartesian, closed      145
Bicartesian, closed, distributive      70 145
Biclosed, monoidal, category      178—179
Bifunctor      8
Binary tree      18
Boolean algebra      148
Boolean algebra, $\omega$ -complete      202
Bound variable      202
Branch of a tree      18 205
Branch, length of a      18
Branch, maximal      18
Cartesian category      40
Cartesian, closed      128
Category      1 4 5
Category, bicartesian      54
Category, bicartesian, closed      145
Category, cartesian      40
Category, cartesian, closed      128
Category, closed      92 107
Category, cocomplete      192
Category, complete      192
Category, discrete      5
Category, distributive bicartesian      70 145
Category, equivalent      9
Category, I-cocomplete      192
Category, I-complete      192
Category, large      5
Category, monoidal      20 21 22
Category, monoidal, biclosed      178—179
Category, monoidal, closed      93
Category, monoidal, of finite sets      199
Category, opposite      7
Category, quantifier-complete      201
Category, residuated      163—164
Category, sequential      12—14
Category, simple      5
Category, small      5
Category, structured      1 21 40 54 70 92 93 107 127 145 163—164 178—179 190 201
Category, symmetric monoidal      31
Category, symmetric monoidal, closed      107
Church — Rosser property      1 3 277
Church — Rosser Theorem      see "Theorem"
class      5
Classifier, subobject      193 195
Closed category      92 107
Closed, cartesian      128
Closed, monoidal      93
Closed, symmetric monoida      107
Cocomplete category      192
Codomain      4
Coequalizer      191
Coherence      20 22 29 32 35 36
Colimit      191
Commutative diagram      6
Complete category      192
Complete category, quantifier      189
Completeness theorem      see "Theorem"
Component (of a natural transformation)      2
composition      4
Composition of natural transformations      7
Composition, generalized      12
Composition, internal      103
Computability theorem      see "Theorem"
Concatenation      11
Conclusion (of a rule of inference)      29
Conjunction      1 195
Conjunction symbol      202
Conjunction, generalized      189 204
Constant functor      6
Contravariant functor      7
Coproduct      22 192 193 200 201
Coproduct, finite      22 192 193
Counit (of an adjunction)      20 97
Counter-examples      32 36 40 54 71 108 118 129 139 149 152 179 214
Cut      19
Cut elimination      60
Cut elimination algorithm      20 229—243
Cut Elimination Theorem      see "Theorem"
Cut formula      20
Cut, degree of a      211 212
Cut-free derivation      19 229
De Morgan arrows      147—151
Deductive system, labelled      17 206—207 219—223
Deductive system, unlabelled      17 204—205 224—228
Degree of a cut      211 212
Degree of a derivation      212 242 243
Degree of a formula      211
Derivable sequent      19 206
Derivation      18—19 205—206
Derivation, cut-free      19 229
Derivation, degree of a      212 242 243
Derivation, height of a      19
Derivation, normal      29 36 50 67—68 86 101 114 136—137 160—161 172 184 217—218 277
Derivation, width of a      19
Diagram      6
Diagram, commutative      6 7
Discrete category      5
Disjunction      1 195
Disjunction symbol      202
Disjunction, generalized      189 204
Distributive bicartesian category      70 145
Distributivity      57—60
Domain      4
Dots      35
Double Negation      156
Eigenvariable      213 214
Elementary topos      194
Embedding      6
Embedding, faithful      see "Embedding"
Equalizer      191
Equivalence relation on $Der(bccl\Delta(X))$       45 61 99 157
Equivalence relation on $Der(bccl\tilde{\Delta}(X))$       41 55 95 153
Equivalence relation on $Der(bc\Delta(X))$       45 61
Equivalence relation on $Der(bc\tilde{\Delta}(X))$       41 55
Equivalence relation on $Der(ccl\Delta(X))$       45 99 133
Equivalence relation on $Der(ccl\tilde{\Delta}(X))$       41 95 130
Equivalence relation on $Der(c\Delta(X))$       45
Equivalence relation on $Der(c\tilde{\Delta}(X))$       41
Equivalence relation on $Der(dbc\Delta(X))$       45
Equivalence relation on $Der(dbc\tilde{\Delta}(X))$       41 72
Equivalence relation on $Der(mbcl\Delta(X))$       27 99 171 183
Equivalence relation on $Der(mbcl\tilde{\Delta}(X))$       24 95 167 181
Equivalence relation on $Der(mcl\Delta(X))$       27 99
Equivalence relation on $Der(mcl\tilde{\Delta}(X))$       24 95
Equivalence relation on $Der(m\Delta(X))$       27
Equivalence relation on $Der(m\tilde{\Delta}(X))$       24
Equivalence relation on $Der(r\Delta(X))$       27 171

Equivalence relation on $Der(r\tilde{\Delta}(X))$       24 95 167
Equivalence relation on $Der(smcl\Delta(X))$       27 34 99 110
Equivalence relation on $Der(smcl\tilde{\Delta}(X))$       24 33 95 108
Equivalence relation on $Der(sm\Delta(X))$       27 34
Equivalence relation on $Der(sm\tilde{\Delta}(X))$       24 33
Equivalence relation on $Der(\Delta^{*}(X))$       45 61 99 157 208—211
Equivalence relation on $Der(\tilde{\Delta}(X))$       41 55 95 153
Equivalence relation on L*(X)      208
Equivalence relation on Mon(A)      294
Equivalent categories      9
Examples of bicartesian categories      54 71 149 152 189 195—199 201—202
Examples of bicartesian categories, closed      149—152 189 190 195—199 201—202
Examples of Boolean algebras      150—151
Examples of cartesian categories      40 54 71 129 149—152 189 190 195—199 201—202
Examples of cartesian categories, closed      129 149—152 189 190 195—199 201—202
Examples of distributive bicartesian      71 149—152 189 190 195—199 201—202
Examples of elementary topoi      189 190 197—199
Examples of Grothendieck topoi      189 197—199
Examples of Heyting algebras      149—150 190 195 197
Examples of monoidal categories      22—23 40 54 71 93—94 107 115—122 129 149—152 179—180 189—190 195—199 201—202
Examples of monoidal categories, biclosed      107 115—122 129 149—152 179—180 189 190 195—199 201—202
Examples of monoidal categories, closed      93—94 107 115—122 129 149—152 179—180 189—190 195—199 201—202
Examples of monoidal, quantifier-complete      189 197—199 201—202
Examples of monoidal, residuated      107 115—122 129 149—152 164—166 179—180 189—190 195—199 201—202
Examples of monoidal, sequential      15—16 28 35 46 62 78 99 110 133 157 172 183 211
Examples of sheaves      197—198
Examples of symmetric monoidal categories      32 40 54 71 107 115—122 129 149—152 189 190 191—202 195—199
Examples of symmetric monoidal categories, closed      107 115—122 129 149—152 189 190 195—199 201—202
Existential quantifier      200
Existential quantifier symbol      202
Export-import law      92
External horn functor      92
Faithful functor      6
FALSE      1 20 195
False, Symbol for      202
Finitarily representable arrow      211
Finitary formula      203
Finite coproduct      22 192 193
Finite product      22 40 54
Finite sequences      11
Finite sets, category of      199
Finite tree      18
Forgetful functor      11
Formal proof      see "Derivation"
Formula      16 202—204
Formula, active      20
Formula, atomic      16
Formula, cut      20
Formula, degree of a      211
Formula, finitary      203
Formula, passive      20
Formulas, sequence of      20
Free bicartesian category      55—56
Free bicartesian category, closed      152—153
Free cartesian category      40—42
Free cartesian category, closed      130—131
Free cartesian, distributive bicartesian      71—73
Free monoid      11
Free monoidal category      24—25
Free monoidal category, biclosed      181—182
Free object functor      12
Free pre-ordered set      11
Free quantifier-complete category      206—207
Free quantifier-complete, residuated      166—168
Free quantifier-complete, symmetric monoidal      33
Free quantifier-complete, symmetric monoidal, closed      108—109
Free variable      202
Full functor      6
Full subcategory      15
Function symbols      202
functor      4 6 14—15
Functor, bi      8
Functor, constant      6
Functor, contravariant      7
Functor, external horn      92
Functor, faithful      6
Functor, forgetful      11
Functor, free monoid      12
Functor, free object      11 12
Functor, full      6
Functor, Horn      8
Functor, identity      8
Functor, internal horn      92 93
Functor, set-valued      8
Functors, adjoint      10
Generalized composition      12
Generalized conjunction      189
Generalized disjunction      189
Generalized natural transformation      97 140
Generalized transitivity      12
Grothendieck topos      199
Height of a derivation      19
Height of a tree      18 205
Heyting algebra      148
Heyting algebra object      196—197
Heyting algebra, $\omega$ -complete      202
Heyting algebra, external      92
Heyting algebra, internal      92 93
Homomorphism of categories      see "Functor"
Homomorphism of pre-ordered sets      6 7
Horn functor      8
Identity arrow      4 5 13 20 220
Identity functor      8
if ... then      2
Immediate reduction      277
Implication      1 195
Implication symbol      202
Inference, operational rules of      3 224 225
Inference, rules of      19 220 221 224 225
Inference, structural rules of      3 20 224
Infinitary conjunction symbol      202
Infinitary disjunction symbol      202
Infinite coproduct functor      see "Existential quantifier"
Infinite product functor      see "Universal quantifier"
Initial object      22
Internal composition      103
Internal Heyting algebra      196—197
Internal horn functor      92
Interpretation of $Der(bccl\Delta(X))$       44 61 76 132
Interpretation of $Der(bc\Delta(X))$       44 61
Interpretation of $Der(ccl\Delta(X))$       44 132
Interpretation of $Der(c\Delta(X))$       44
Interpretation of $Der(dbc\Delta(X))$       44 61 76
Interpretation of $Der(mbcl\Delta(X))$       26 98 170
Interpretation of $Der(mcl\Delta(X))$       26 98
Interpretation of $Der(m\Delta(X))$       26
Interpretation of $Der(r\Delta(X))$       26 98 170
Interpretation of $Der(smcl\Delta(X))$       26 34 98 110
Interpretation of $Der(sm\Delta(X))$       26 34
Interpretation of $Der(\Delta^{*}(X))$       44 61 76 132 208
Isomorphic objects      9
Isomorphism      8
Isomorphism, natural      8
Label      17 206 219
Labelled deductive system      17 206—207 219 223
Labelled sequent      16
Language      16 202—204
Large category      5
Left rank      211 212 242 243
Length of a branch      18 205
LIMIT      191
Maximal branch of a tree      18
MIX      243
Monoid, free      11
Monoidal categories, coherence in      20
Monoidal category      20 21 22
Monoidal category, biclosed      178—179
Monoidal category, closed      93
Monoidal category, closed, symmetric      107
Monoidal category, symmetric      31

1 2

О проекте