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

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

Monomorphism      193
Monotone relation      229 244
Natural isomorphism      8
Natural sink      191
Natural source      191
Natural transformation      7
Natural transformation, component of a      7
Natural transformation, generalized      97 140
negation operator      147
Node      18
Normal derivations of $bccl\Delta(X)$       50 67—68 86 136—137 160?16I
Normal derivations of $bc\Delta(X)$       50 67—68
Normal derivations of $ccl\Delta(X)$       50 136—137
Normal derivations of $c\Delta(X)$       50
Normal derivations of $dbc\Delta(X)$       50 67—68 86
Normal derivations of $mbcl\Delta(X)$       29 101 172 184
Normal derivations of $mcl\Delta(X)$       29 101
Normal derivations of $m\Delta(X)$       29
Normal derivations of $r\Delta(X)$       29 101 172
Normal derivations of $smcl\Delta(X)$       29 36 101 114
Normal derivations of $sm\Delta(X)$       29 36
Normal derivations of $\Delta^{*}(X)$       50 67—68 86 136—137 160—161 217—218
Normalization algorithm      244—277
Normalization theorem      see "Theorem"
Object      4 12
Object, coproduct      23
Object, Heyting-algebra      196—197
Object, initial      22
Object, isomorphic - s      9
Object, product      23
Object, terminal      22
Only if      2
Operational (rule of inference)      2 224
Opposite category      7
Opposite pre-ordered set      7
OR      2
Ordered tree      18 205
Passive formula      20
Pre-ordered set      4 6 7 11
Pre-ordered set, free      11
Pre-ordered sets, homomorphism of      6 7
Premiss (of a rule of inference)      29
PRODUCT      22 192 193
Product functor, infinite      see "Universal quantifier"
Product object      23
Product, finite      22 40 54
Proof $\natural$ , $\Rightarrow$ , $\Leftarrow$       163
Proof I, $\natural$ , $\Rightarrow$       92 107
Proof I, $\natural$ , $\Rightarrow$ , $\Leftarrow$       178
Proof T, $\wedge$       32
Proof T, $\wedge$ , $\perp$ ,       54 70
Proof T, $\wedge$ , $\perp$ , , $\Rightarrow$       145
Proof T, $\wedge$ , $\perp$ , $\vee$ , $\Rightarrow$ , $\forall$ , $\exists$       189
Proof T, $\wedge$ , $\Rightarrow$       128
Proof theory of -I, $\natural$       21 31
Proof, formal      see "Derivation"
Proof, pure variable      213
Pullback      192 193
Pure variable proof      213
Pushout      192 193
Quantifie      189 200
Quantifier algebra      190 201
Quantifier completeness      189
Quantifier symbols      202
Quantifier, existential      200
Quantifier, universal      200
Quantifier-complete category      201
Rank      211 212 214 217 242 243
Rank, left      242 243
Rank, right      242 243
Rank, weighted      243
Reducibility relation      1 3 244—277
Reducibility relation on $Der(bccl\Delta(X))$       50 68 87 137
Reducibility relation on $Der(bc\Delta(X))$       50 68
Reducibility relation on $Der(ccl\Delta(X))$       50
Reducibility relation on $Der(c\Delta(X))$       50
Reducibility relation on $Der(dbc\Delta(X))$       50 68 87
Reducibility relation on $Der(mbcl\Delta(X))$       29 101 172 184
Reducibility relation on $Der(mcl\Delta(X))$       29 101
Reducibility relation on $Der(m\Delta(X))$       29
Reducibility relation on $Der(r(\Delta(X))$       29 101 172
Reducibility relation on $Der(smcl\Delta(X))$       29 36 101 114
Reducibility relation on $Der(sm\Delta(X))$       36
Reducibility relation on $Der(\Delta^{*}(X))$       50 68 87 137 217—218
Reflexive relation      4
Relation symbols      202
Relation, monotone      229 244
Relation, reducibility      244—277
Relation, reflexive      4
Relation, transitive      4 229 244
Residuated category      163 164
Restrictions on $Der(\delta^{*}(X))$       212
Restrictions on $Der(\delta^{*}(X))$ (A2)      220
Restrictions on $Der(\delta^{*}(X))$ (R1)      156—157 213

Restrictions on $Der(\delta^{*}(X))$ (R14)      254—155
Restrictions on $Der(\delta^{*}(X))$ (R15)      225
Restrictions on $Der(\delta^{*}(X))$ (R16)      225
Restrictions on $Der(\delta^{*}(X))$ (R17)      225
Restrictions on $Der(\delta^{*}(X))$ (R18)      205 208 213
Restrictions on $Der(\delta^{*}(X))$ (R21)      205 209 213
Restrictions on $Der(\delta^{*}(X))$ eigenvariables      213
Right rank      211 212 242 243
Rule of inference      19 220—221 224—225
Rule of inference, admissible      19
Rule of inference, application of a      19
Rule of inference, application of a structural      20
Rule of inference, conclusion of a      19
Rule of inference, finitary      217
Rule of inference, instance of a      19
Rule of inference, operational      3 224 225
Rule of inference, premiss of a      19
Rule of inference, quantificational      204—205
Rule of inference, structural      3 20 224
Sequence of formulas      20
Sequence, finite      11
Sequent      16 202—204 219 224 229
Sequent, antecedent of a      17
Sequent, derivable      19 206
Sequent, labelled      16
Sequent, succedent of a      17
Sequent, unlabelled      16
Sequential category      12—14
Set      5
Set, pre-ordered      4 6 7 11
Set-valued functor      8 10
Set-valued sheaf      197
Sheaf      197 198—199
Simple category      5
Sink      191
Site      198
Small category      5
Source      191
Stability (under intersections)      298
Strictness (of an initial object)      25 145
Structural (rule of inference)      2 20 224
Structured category      1 21 40 54 70 92 93 107 128 145 163—164 178 179 190 201
Subcategory      15
Subderivation      20
Subformula      20
Sublanguage      20
Subobject      194
Subobject classifier      193 195
Substitution      12 15 16
Subsystem, deductiv      19 20
Succedent      17
Succedent symbol      20
symbols      16 202
Symbols, antecedent      20
Symbols, succedent      20
Symmetric monoidal      31
Symmetric monoidal closed      107
System, labelled deductive      17 206—207 219—223
System, unlabelled deductive      17 204—205 224—228
Tensor product      23 92 93
Terminal object      22
Terms      15 202—203
Theorem, Church — Rosser      3 29 36 50 69 89 106 110 118 122 143 162 176 186 218 277
Theorem, coherence, for mCat      29
Theorem, coherence, for smCat      35 36
Theorem, completeness      27 34 45 61 77 99 110 133 157 171 183 211
Theorem, computability      29 38 52 69 91 106 127 143 164 177 205
Theorem, cut elimination      28 35 47 63 78 100 111 134 158 172 183 211 217 243
Theorem, normalization      29 36 50 68 87 101 114 137 161 172 184 211 218 277
Topos, elementary      194
Topos, Grothendieck      199
Transformation      see "Natural transformation"
Transitive relation      4 229
Transitivity, generalized      12
TREE      17 18 205
Tree, binary      18
Tree, branch of a      18 205
Tree, finite      18
Tree, height of a      18 205
Tree, ordered      18 205
Tree, width of a      18 205
TRUE      1 20 195
True, symbol for      202
Unit of a tensor product      23 163
Unit of an adjunction      10 97
Universal quantifier      200
Universal quantifier symbol      202
Unlabelled deductive system      17 204—205 224—228
Unlabelled sequent      16
Variable, bound      202
Variable, free      202
Weighted rank      243
Width of a derivation      19
Width of a tree      18 205
Word problem      11—12

1 2

О проекте