√лавна€    Ex Libris     ниги    ∆урналы    —татьи    —ерии     аталог    Wanted    «агрузка    ’удЋит    —правка    ѕоиск по индексам    ѕоиск    ‘орум   
blank
јвторизаци€

       
blank
ѕоиск по указател€м

blank
blank
blank
 расота
blank
Szabo M. E. Ч Algebra of proofs
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.


язык: en

–убрика: ћатематика/

—татус предметного указател€: √отов указатель с номерами страниц

ed2k: ed2k stats

√од издани€: 1978

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

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

ќперации: ѕоложить на полку | —копировать ссылку дл€ форума | —копировать ID
blank
ѕредметный указатель
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
blank
–еклама
blank
blank
HR
@Mail.ru
       © Ёлектронна€ библиотека попечительского совета мехмата ћ√”, 2004-2023
Ёлектронна€ библиотека мехмата ћ√” | Valid HTML 4.01! | Valid CSS! ќ проекте