Барвайс Д. — Справочная книга по математической логике. Часть 4. Теория доказательств и конструктивная математика :: Электронная библиотека попечительского совета мехмата МГУ

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

Авторизация

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

Барвайс Д. — Справочная книга по математической логике. Часть 4. Теория доказательств и конструктивная математика

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

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

Название: Справочная книга по математической логике. Часть 4. Теория доказательств и конструктивная математика

Автор: Барвайс Д.

Аннотация:

Настоящее издание состоит из четырех книг: «Теория моделей», «Теория множеств», «Теория рекурсии», «Теория доказательств и конструктивная математика». В оригинале оно составляло один том, который при переводе для удобства был разбит на четыре книги, соответствующие четырем частям исходной книги. Русский перевод каждой части дополнен статьей советских авторов, отражающей дополнительные аспекты, не нашедшие отражения в основном тексте издания.
Издание в целом рассчитано на всех математиков, начиная со студентов университетов, интересующихся развитием современной математики и логики.

Язык:

Рубрика: Математика/Справочники/

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

ed2k: ed2k stats

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

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

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

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

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

Tonoc (topos)      241 255
Автономные прогрессии теорий (autonomous progressions of theories)      137 156
Аксиома выбора интуиционистская (intuitionistic axiom of choice)      173 174
Аксиомы Цермело — Френкеля для теории множеств (Zermelo — Fraenkel axioms for set theory)      29 39
Алгебраические системы конечного типа (finite type structures)      106
Алгебраические системы конечного типа максимальные (maximal finite type structures)      111
Алгебраические системы конечного типа минимальные (minimal finite type structures)      111
Алгоритм предельного перехода      328
Аппликативная система (applicative system)      281
Аппроксимации теорема в $\lambda$ -исчислении (approximation theorem of $\lambda$ -calculus)      312
Аппроксимация термов в $\lambda$ -исчислении (approximation of terms in $\lambda$ -calculus)      312
Арифметика второго порядка интуиционистская (intuitionistic second order arithmetic)      170
Арифметика конечных типов (number theory of finite types)      122
Арифметика Пеано (Peano arithmetic)      28 39 48—53 320
Арифметика первого порядка интуиционистская (intuitionistic first order arithmetic)      169
Арифметическая схема свертывания (arithmetic comprehension scheme)      125 126
Бар-индукция (bar induction)      130 141 144 198
Бар-рекурсия (bar recursion)      219
Бар-теорема (bar-theorem)      198
БГК-разъяснение (BHK-explanation)      163 169
Беззаконные последовательности (lawless sequences)      206—208
Бесконечный вывод (Infinite derivation)      67
Бесконечный терм (infinite term)      147
Бёма деревья (Bohm trees)      305
Бёма теорема (Bohm’s theorem)      306
Бинумерация (binumeratlon)      26
Больцано — Вейерштрасса теорема (Bolzano — Weierstrass Theorem)      230
Вложенность дерева в дерево      344
Внутренность $\lambda$ -алгебры (interior of $\lambda$ -algebra)      287
Вполне перечислимое множество (listable set)      329
Вполне упорядочения арифметики $\mathbf Z$ (well-orderings of $\mathbf Z$ )      133 146
Вполне упорядочения доказуемо рекурсивные (provably recursive well-orderings)      132
Вполне упорядочения естественные (natural well-orderings)      65
Вполне упорядочения разветвленного анализа (well-orderings of ramified analysis)      147
Вывод (derivation, deduction)      343
Генератор вещественного числа (real number generator)      180
Генераторы точек (point generators)      190
Генценовские правила для логики первого порядка (Gentzen-style rules for first-order logic)      58
Гёделевская функциональная интерпретация (Dialecticain tcrpretation, Godel's functional interpretation)      151 220—228 368
Гнездности кванторов глубина      81
Гомоморфизм $\lambda$ -алгебр (homomor-phisra of $\lambda$ -algebra)      287
Двоичное разложение (binary expansion)      185
Декартово замкнутая категория (cartesian closed category)      244
Допустимая система термов      333
Идеальные утверждения (ideal statements)      11
Индекс      см. «Код»
Индикаторные функции (indicator functions)      326
Индукция по необеспеченным последовательностям (induction over unsecured sequences)      197
Индукция трансфинитная (transfinite induction)      65 129 199
Интенсиональные непрерывные функционалы (intensional continuous functionals)      216
Интерпретация $\lambda$ -термов (interpretation of $\lambda$ -terms)      285
Интерпретация отсутствием контрпримера (no-counterexample interpretation)      56
Интерпретация языка в топосе (interpretation of a language in a topos)      263
Интуиционизм (intuitionism)      160
Исчисление предикатов интуиционистское (intuitionistic predicate calculus)      167
Исчисление равенств (equation calculus)      86
Исчисление разбиений (partition calculus)      318
Каноническое дерево вывода      341
Категория определимых типов и определимых тотальных функций (category of definable types and definable total functions)      253
Кванторные операторы (quantification operators)      123
Классификатор подобъектов (sub-object classifier)      255
Код (code)      14 17—32
Код бесконечного вывода (code for infinite derivation)      73
Комбинаторная алгебра (combinato-ry algebra)      281
Конечные пределы (finite limits)      245
Конечные произведения (finite products)      243
Конечные типы (finite types)      214
Консервативное расширение (conservative extension)      120
Конструктивизация глобальная (global constructivisation)      229
Конструктивизация локальная (local constructivisation)      229
Конструктивизм (constructivism)      160
Конструктивизм наивный (naive constructivism)      161
Корректная теория (sound theory)      15 32
Кортеж      373
Кортеж n-нормальный      375
Кортеж вполне нормальный      376
Кортеж непродолжимый      374
Кортеж нормальный      376
Кортеж правильный      375
Кортеж продолжимый      374
Кортеж регулярный      373
Кортеж, продолжение      373
Критические функции на ординалах (critical functions of ordinals)      133
Лемма о диагонализации (diagonalization lemma)      15
Лемма об обращении (inversion lemma)      60 68 75
Логический функтор (logical functor)      272
Ложность теоремы Кантора — Бендиксона в HYP (Cantor — Bendixon theorem is false in HYP)      142
Локально корректная фигура      341
Мажоранта формулы      358
Метрическое пространство интуиционистское (intuitionstic metric space)      190
Метрическое пространство конструктивное      328
Модуль непрерывности (modulus of continuity)      78
Модуль сходимости      328
Мономорфизм (monomorphism, monic)      245
Направление конструктивное в математике      367
Наследственно гиперарифметические операции (hereditary hyperarithmetic operations)      139
Наследственно непрерывный функционал (hereditary continuous functional)      139
Наследственно рекурсивные операции (hereditary recrursive operations)      138 215
Наследственно эффективные операции (hereditary effective operations)      216
Натуральные числа (natural numbers)      см. «Арифметика Пеано»
Негативный перевод (negative (or double negation) translation)      149 172
Непрерывная функция (continuous function)      187
Нормализация бесконечных термов (normalization of infinite terms)      147
Нормальный натуральный вывод      353
Нумерация (numeration)      26
Нумерическая представимость (numeralwise representatibility)      26
Обобщенная непрерывность (generalized continuity)      206
Общезначимость интуиционистская (intuitionistic validity)      212
Объект натуральных чисел (natural number object)      273
Ограниченная индукция (restricted induction)      119 155
Окрестностная функция (neighbourhood function)      196
Операторы рекурсии (recursion operators)      121 124
Операции, заданные законом (law-like operations)      215
Определение истинности (truth definition)      31 32
Определимый тип (definable type)      251
Ординальные обозначения (ordinal notations)      155
Отделенность (apartness)      182
Отрицательная формула (negative formula)      172
Отрицательный перевод      см. «Негативный перевод»
Перевод в формально интуиционистские системы (translation into formally intuitionislic systems)      149
Перечислительные системы (enumerative systems)      138

Полнота интуиционистской логики (completeness of intuitionistic logic)      213
Полнота множества вещественных чисел (completeness of the reals)      186
Полнота семантическая (semantic completeness)      42
Полнота синтаксическая (syntactic completeness)      42
Почти отрицательная формула (almost negative formula)      175
ПР-формула (PR-formula)      31
Правило Маркова (Markov’s rule)      225
Правило прогрессивности (progression rule)      66
Правило сечения (cut rule)      59
Пред- $\lambda$ -алгебра (pre- $\lambda$ -algebra)      285
Предикативность (predicativity)      136 156
Представляющая функции (representing function)      20
Примитивно рекурсивная формула (primitive recursive formula)      31
Примитивно рекурсивная функция (primitive recursive function)      19
Примитивно рекурсивный функционал (primitive recursive functional)      72
Принцип Маркова (Markow’s principle)      см. «Схема Маркова»
Принцип рефлексии в теории доказательств (proof-theoretic reflection principle)      33 80
Принцип рефлексии глобальный (global reflection principle)      33
Принцип рефлексии локальный (local reflection principle)      33
Принцип рефлексии равномерный (uniform reflection principle)      33
Программа Гильберта (Hilbert’s program)      9—13
Прослеживаемое множество      329
Процедура поиска вывода (proof search procedure)      84—87 91—
Прямота (directness)      90— 98
Прямоугольник неделимый      379
Равномерно непрерывная функции (uniformly continuons function)      187
Разветвление аналитические множества (ramified analytic sets)      135
Разветвленные прогрессии теорий (ramified progressions of theories)      136 156
Разветвленный анализ (ramified analysis)      136
Разрешимый терм $\lambda$ -исчисления (solvable term of $\lambda$ -calculus)      303
Ранг сечений (cut rank)      59
Реализуемость (readability)      174— 179 206
Реальные утверждения (real statements)      11
Регулятор сходимости в себе      367
Редекс (redex)      288
Рекурсивно перечислимое множество (recursively enumerable set)      30
Рекурсивное множество (recursive set)      30
Рекурсивное расширение (recursive extension)      64
Рекурсивный анализ классический (classical recursive analysis)      162 178
Рекурсивный анализ конструктивный (constructive recursive analysis)      160 177
Рекурсивный функционал конечного типа (recursive functional of finite type)      140
Релятивизация понятий к универсумам (relativization of notions to universes)      111
Рефлексивная теория (reflexive theory)      39
Свободно становящиеся последовательности (choice sequences)      193
Свободно становящиеся последовательности, элиминация (elimination of choice sequences)      199—204
Сегмент неделимый      378
Системы обозначений для ординалов (systems of notation for ordinals),      см. «Ординальные обозначения»
Слабый контрпример (weak counterexample)      183
Сложность (complexity)      85
Сравнимость вполне упорядочений (comparability of well-orderings)      132 142
Стандартное представление (standard representation)      190
Схема Маркова (Markov's scheme)      177 208—211 213 347 349 355 366
Схема непрерывности (continuity scheme)      194
Схема свертывания для иерархии, основанной на операторе скачка (jump hierarchy comprehension scheme)      134
Схема трансфинитной индукции (transfinite induction scheme)      129 (см. также «Индукция»)
Схемы в теориях конечного типа (schemata in finite type theories)      120
Схемы второго порядка (second order schemata)      125
Схемы выбора (choice schemata)      121 123 125
Схемы свертывания (comprehension schemata)      121 125't
Счетные функционалы (countable functionals)      217
Тезис Чёрча расширенный (extended Church's thesis)      176
Теорема Poccepa (Rosser’s theorem)      29
Теорема Poccepa формализованная (formalized Rosser’s theorem)      289
Теорема Poccepa Чёрча — Poccepa (Church — Rosser theorem)      289
Теорема Poccepa Эрбрана (Herbrand’s theorem)      63 84—99 331—340
Теорема Брауэра о неподвижной точке (Brouwer’s fixed point theorem)      189 231 367
Теорема Вейерштрасса о приближении многочленами (Weierstrass' approximation theorem)      233
Теорема Гильберта — Бернайса о полноте (Hilbert — Bernays completeness theorem)      49
Теорема Карри о нормализации (normalization theorem of Curry)      291
Теорема Кента (Kent's theorem)      43
Теорема Лёба (Lob’s theorem)      33 36
Теорема Лёба формализованная (formalized Lotfs theorem)      43 46
Теорема о веере (fan theorem)      199 205
Теорема о консервативности (conservation theorem)      47
Теорема о неподвижной точке (fixed point theorem)      44
Теорема о неподвижной точке в $\lambda$ -исчислении (fixed point theorem of $\lambda$ -calculus)      287
Теорема о неподвижной точке де Йонга (de Jongh’s fixed point theorem)      45
Теорема о неполноте вторая (second incompleteness theorem)      13 16 34 50
Теорема о неполноте вторая формализованная (formalized second incompleteness theorem)      17
Теорема о неполноте первая (first incompleteness theorem)      13 15 34 49
Теорема о неполноте первая формализованная (formalized first incompleteness theorem)      40
Теорема о рефлексивности (reflexiveness theorem)      188 231
Теорема о среднем значении (intermediate value theorem)      188 231
Теорема о существенной неограниченности (esstential unboundedness theorem)      38
Теорема о характеризации для гёделевской интерпретации (characterisation theorem for Dialectica interpretation)      224
Теорема о характеризации для реализуемости (characterisation theorem for realibility)      176
Теорема об относительной непротиворечивости (relative consistency theorem)      47
Теорема об устранении сечения (cut-elimination theorem)      62 70 76 88
Теорема об устранении сечения для бесконечно длинных формул (cut-elimination theorem for infinitely long formulas)      145
Теорема Париса — Харингтона (Paris — Harrington theorem)      320
Теорема Ролля (Rolle’s theorem)      234
Теории индуктивных определений (theories of inductive definitions)      156
Типовые символы (type symbols)      117
Точная верхняя грань (least upper bound)      188
Универсальный (декартов) квадрат (pullback)      244
Универсум $\exists^N$ -замкнутый ( $\exists^N$ -closed universe)      108
Универсум N-замкнутый (N-closed universe)      108
Универсум декартово замкнутый (cartesian closed iniverse)      105
Универсум множеств и функций (universe of sets and functions)      104 105
Уравнитель (equalizer)      244
Условие Коши      369
Условия выводимости (derivability conditions)      15 27 28
Финитизм (flnitism)      160 165
Формула боковая (side formula)      59 334
Формула главная (main formula)      59
Формула малая (minor formula)      59 334
Формула ограниченная (bounded formula)      321
Формула однокванторная (one-quantifier formula)      337
Формула Эйлера — Пуанкаре — Хопфа      368
Фундированность упорядочений (wellfoundedness of orderings)      128
Функция конструктивная      367
Частичные элементы (partial elements)      246—252
Частичный морфизм (partial map)      261
Экстенсиональность в конечных типах (extensionability in finite types)      119
Экстенсиональность, устранение (elimination of exten-sionality)      217
Экстенсиональные непрерывные функционалы (extensional continuous functional)      217
Элементарный анализ (интуиционистский) (intuitionistic elementary analysis)      170
Эрбрановская дизъюнкция (Herbrand disjunction)      332 333
Эрбрановская нормальная форма (Herbrand normal form)      77
Эффективно неотделимые множества (effectively inseparable sets)      30
Эффективный оператор      329
Язык высшего порядка (higher order language)      247

О проекте