Авторизация
Поиск по указателям
Suppes P.(ed.) — Handbook of Proof Theory.Studies in logic the foundations of mathematics.Volume 137.
Обсудите книгу на научном форуме Нашли опечатку?
Название: Handbook of Proof Theory.Studies in logic the foundations of mathematics.Volume 137.Автор: Suppes P.(ed.) Аннотация: This volume contains articles covering a broad spectrum of proof theory, with an emphasis on its mathematical aspects. The articles should not only be interesting to specialists of proof theory, but should also be accessible to a diverse audience, including logicians, mathematicians, computer scientists and philosophers. Many of the central topics of proof theory have been included in a self-contained expository of articles, covered in great detail and depth.
The chapters are arranged so that the two introductory articles come first; these are then followed by articles from core classical areas of proof theory; the handbook concludes with articles that deal with topics closely related to computer science.
Язык: Рубрика: Математика /Статус предметного указателя: Готов указатель с номерами страниц ed2k: ed2k stats Год издания: 1998Количество страниц: 821Добавлена в каталог: 05.03.2014Операции: Положить на полку |
Скопировать ссылку для форума | Скопировать ID
Предметный указатель
Finite type symbols 429 First incompleteness theorem 120 First-order logic 29 341 Fitting, M. 643 651 652 680 Fixed point 269 399 Fixed point combinator, Y 763 764 Fixed point theorem 484 521 Fixed-point term 308 Fontet, M. 681 Forcing relation 478 Forester, M.B. 762 777 Formal proof 2 Formula, first-order 26 31 642 Formula, propositional 3 701 Formulas as types 47 68—70 459 500 751 FORTRAN 754 Foundation axiom 216 217 Foundation Lemma 323 Foundation Theorem 324 Fourman, M.P. 448 464 Fraenkel, A.A. 577 582 586 688 718 774 Fragment 80 Frame 515 see "Veltman "Visser Free access 722 Free cut 16 43 46 112 Free cut elimination 42 109 111 112 Free cut free 16 43 Free variable 27 69 703 734 Free variable normal form 33 Free variable, FV 409 Free-cut elimination 16 Free-cut Elimination Theorem 16 44 46 47 65 109 Free-cut free consistency 138 Freely substitutable 27 Frege proof 591 Frege rule 591 Frege system 5—10 591 see "Substitution Frege system, bounded depth 599 Frege, G. 3—5 9 30 31 75 403 549 553 554 570 590—607 617—626 630 631 633 634 685—687 689 694 695 714 718 727 750 777 779 780 Freiman, C.V. 775 Freyd, P.J. 421 463 Friedman, H.M. 153 190 204 205 266 268 279 333 334 372 376 377 382 385 386 399 402 419 421 422 445 458 461 464 465 513 571 581 628 632 721 766 777 Friedrich, W. 340 366 402 Frolov, I.T. 680 Full Type Structure 430 Function 715 738 Function comprehension 717 Function symbol 26 Function type 429 714 Functional 343 Functional model 356 Functional of finite type 356 Gabbay, D. 543 Gaifman, H. 88 98 144 Gallaire, H. 680 Gallier, J.H. 394 397 398 402 465 767 777 Galois, E. 767 Gandy, R.O. 286 636 Gavrilenko, Yu.V. 459 465 577 632 Generalized Continuity (GC) 427 439 Generalized Continuity (GC), Rule (GCR) 428 Gentzen's Hauptsatz see "Cut elimination" Gentzen's Theorem 240 Gentzen, G. 10 16 36 37 44 47 66 75 123 126 144 167 169 187 190 205 230 231 233 240 241 338 342 361 380 382 384—386 392 398 461 552—554 564 571—574 600 632 686 688 723 777 Gerber, H. 391 402 Gertz, E. 74 Geuvers, J.H. 690 782 Ginsberg, M.L. 643 680 Girard interpretation 393 see Girard, J.-Y. 47 57 68—70 75 80 126 144 153 164 190 193 205 249 334 340 393—400 402 459 465 554 632 657 658 675 679 680 689 690 692 695 721 723 724 778 779 782 Gleit, Z. 484 543 Glivenko, V.I. 552 Globally essentially reflexive 505 Goal 649 Goal, empty 649 Goal, form 661 Goedel 94 Goedel Diagonal Lemma 119 Goedel Fixpoint Lemma 119 Goedel number 92 114 Goedel — Bernays (GB) set theory 589 Goedel, K. 30 66 75 80 92—94 100 102 108 112—116 118—123 126 128 137 138 142 143 145—147 190 193 210 241 333 337—343 346 347 350 362 365 366 399 401—405 458 461 465 476 481 484 488 497—500 502 505 506 508 509 543 560 578 580 581 583 586 627 628 631 632 686—689 699 718 733 766 778 779 784 Goerdt, A. 605 633 Goldfarb, W. 76 484 543 Good representation 261 Good, D. 690 778 Goodman, N.D. 441 465 Goodstein sequence 191 Goodstein, R.L. 191 192 Gordon, M. 690 691 709 717 778 Gottlob, G. 402 Grayson, R.J. 422 434 441 457 465 Griffin, T.G. 708 709 778 Griffith, J.E. 775 Griffor, E. 400 403 Groebner proof system 604 Groebner, W. 604 631 Groote, J.F. 465 Grothendieck topos 719 Grothendieck, A. 695 719 744 768 Ground clause 62 Ground literal 62 Ground resolution 62 Group 758 Grundy, J. 779 Grzegorczyk hierarchy 174 Grzegorczyk, A. 174 189 204 205 207 460 553 633 Guaspari, D. 495 496 507 528 543 544 546 Guenthener, F. 543 Gunter, C.A. 765 775 778 Gunter, E. 759 778 Gutierrez, C. 74 Guttag, J. 691 757 778 781 Guttman, J.D. 691 777 Hajek, P. 80 143 145 147 190 205 333 372 403 497 507 521 528 543 563 574 589 619 633 Hajos calculus 601 Hajos, G. 601 603 633 Haken, A. 605 611 616 633 Hallnaes, L. 655 680 Hardy functions 158 249 Hardy hierarchy 152 158 242 Hardy, G.H. 152 153 158 186 190 205 242 249 Harel, D. 498 543 Harnik, V. 434 460 465 Harper, R. 745 748 766 776 778 782 Harrington, L. 122 126 146 191 205 372 376 Harrison, J. 779 Harrop formula 66 Harrop, R. 66 75 Hartmanis, J. 686 779 Hartung, V. 386 401 Hastad, J. 618 633 Hayden, M. 766 780 head 649 714 Height 168 178 486 Height, Kripke model 478 Heine, E. 371 Helmink, L. 692 779 Henkin, L. 30 75 145 506 Henschen, L. 25 75 Henson, C.W. 628 631 Henzinger, T.A. 766 774 779 783 Herbrand disjunction 574 Herbrand function 50 Herbrand proof 52 Herbrand structure 645 Herbrand universe 643 Herbrand variant 574 Herbrand's theorem 48—56 Herbrand, J. 48—52 54 55 59 61 62 75 132 137 145 338 372 382 384—386 555 573 574 577 589 628 632 634 640 643 645 653 654 659 679 686 688 Herbrandization 50 Hereditarily Effective Operations (HEO) 357 431 Hereditarily extensional recursive (HRE) 390 Hereditarily majorize see "Majorize" Hereditarily Recursive Operations (HRO) 357 430 Heyting arithmetic see "Arithmetic" Heyting's semantics 724 751 Heyting, A. 65 147 341 367 401 403 404 408 441 446 448 450 457 465 467 488 544 545 636 701 721 724 726 741 751 774 780 Hickey, J.J. 691 692 722 764—766 779 780 783 Hierarchy theorem 173 Higher-order logic, intuitionistic 445 Higman, G. 461 Hilbert style system 29 553 729 Hilbert — Bernays — Loeb derivability conditions 117 Hilbert's program 338 339 Hilbert, D. 3 10 18 21 27 29 31 37 76 117 145 210 338 339 345 403 476 481 506 543 552—555 564 573 574 585 590 600 601 603 630 633 685 686 688 701 704 717 721—723 729 779 Hilpinen, R. 680 Hinata, S. 339 Hindley, J.R. 76 359 403 464 546 755 774 779 Hintikka, J. 36 76 472 Hirschberg, D. 782 Ho, P.-H. 766 779 Hoare, C.A.R. 756 760—762 776 778 779 Hodges, W. 403 681 Hodgson, B.R. 100 106 145 Hoesli, B. 675 680 Homomorphism 606 Honest 160 Honesty theorem 163 Honsell, F. 778 Hoogland, E. 541 Hopcroft, J.E. 779 Horn clause 25 63—64 Horn, A. 25 26 63 64 75 636 640 Horning, J. 691 778 Howard ordinal see "Bachmann — Howard ordinal" Howard, W.A. 47 68 76 126 145 164 193 196 199 205 206 338—340 351 360 366 367 369 370 373 385 386 391 392 403 436 465 500 751 Howe, D.J. 691 745 759 762 767 773 775 776 779 Huet, G. 471 691 692 721 773 776 779 Hughes, G.E. 478 543 Hwang, L.J. 775 Hyland, J.M.E. 451 457 461 465 466 636 780 Hyperarithmetic set 380 Hyperarithmetical Quantifier Theorem 229 Hyperjump 270 Hyperresolution 22 Hypothetical judgement 699 Idempotency 415 Identity axiom 656 see Identity-free derivation 657 Iemhoff, R. 541 Igarashi, S. 690 780 Ignatiev, K.N. 494 529 543 Ignjatovic, A. 101 103 110 138 144 629 633 ILM frame see "Veltman frame" Impagliazzo, R. 599 604 607 618 621 630 631 633 635 Implication, logical 28 32 Implication, tautological 4 Implicationally complete 591 Implicit definition 58 Impredicative polymorphism 393 Impredicative systems 266 Impredicative systems, table of 332 Incompleteness 118—122 241 Independence of Premise (IP) 347 352 418 432 Induced model 502 Induction 232 272 Induction axiom 46 178 Induction axiom, IND 83 110 Induction axiom, length (LIND) 101 110 Induction axiom, polynomial (PIND) 101 110 Induction Lemma 234 Induction rule 45 176 200 735 737 Induction rule, IND 46 110 Induction rule, PIND 46 110 Induction, 154 Induction, transfinite 187 200 210 211 380 417 Induction, transfinite, TI 224 238 261 286 Induction, type 1 (Res) 378 Inductive cut see "Cut in a model" Inductive definition 269 285 387 391 399 see Inductive extension 677 Inductive norm 269 Inductive set 276 Inductive type 764 Inductively definable 269 Infinitary Logic 17 165 361 Infinite height 486 Infinity, axiom of 217 280 Inhabited 705 Initial 739 Initial sequent 32 Input argument 665 Input resolution 24 Input variables 665 Instance 49 591 648 703 Intensional 113 114 116 121 Intensional Continuous Functionals (ICF) 433 Intensional equality 350 Intensional in Q 118 Interactive proof 550 Interpolability 529 Interpolant 56 612 Interpolation theorem 56—58 612 Interpretability logic 514 Interpretable 503 Interpretation 502 see Interpretation (structure) 27 Interpretation, cointerpretation 503 528 Interpretation, faithful 503 528 Interpretation, feasible 514 Interpretation, weak 503 528 Introduction rule 47 Intuitionistic logic 64—70 341 411 Intuitionistic logic, natural deduction 48 Inversion lemma 167 256 302 Inversion theorem 13 Irreducible 358 Irrelevance of proofs 723 Isomorphic 451 Iterated admissibility 291 Iterated admissibility, ItAd 291 Iterated admissibility, RltAd 292 Iterated closure 304 Iterated comprehension 276 Iterated consistency 486 490 Iterated hyperjumps 270 Iterated inductive definitions 203 270 271 273 392 see Iterated reflection 495 Ito, T. 776 Jackson, P.B. 709 711 745 767 776 780 Jaeger, G. 268 291 334 384—386 402 472 473 640 655 672 675 680 Jagadeesan, r. 74 Jankov, V.A. 466 Japaridze (Dzhaparidze), G.K. 486 487 489 494 495 503 512 522 528—530 535 539—543 Java 754 Jeffrey, R.C. 533 542 Jenks, R.D. 767 780 Jeroslow, R.G. 495 Johannsen, J. 633 Johnson, D.S. 133 145 Johnson, S.D. 690 775 776 Johnstone, P.T. 451 457 465 Joja, A. 469 Jonasson, A. 74 Joosten, J. 541 Jouannaud, J.-P. 358 401 Joyal, A. 466 721 780 judgment 729 Jumelet, M. 488 544
Реклама
function 
-induction 
|
|
О проекте