М.: РоссПЭН, 1999. — 318 с.
Сборник содержит основные труды выдающегося отечественного логика
профессора В.А.Смирнова по теории логического вывода, в том числе
основополагающую монографию «Формальный вывод и логические
исчисления».
В приложении имеется полная библиография работ В.А.Смирнова.
Книга предназначена для логиков, философов и всех интересующихся проблемами логической науки. Содержание
Некоторые логические идеи В.А.Смирнова.
Формальный вывод и логические исчисления предисловие.
Классическая логика предикатов и ее формализация гильбертовского типа.
Язык логики предикатов первого порядка.
Семантика классической логики предикатов первого порядка.
Формализация и аксиоматизация.
Логистические системы гильбертовского типа с понятием формального доказательства. Формализация свойства универсальной общезначимости.
Формализация гильбертовского типа отношения логического следования классической логики предикатов.
Формы выводов и теоремы дедукции для логистических систем гильбертовского типа.
Предварительные замечания.
Вывод как линейная последовательность формул.
Вывод с анализом.
Логистические системы с выводом в виде дерева.
Теорема дедукции для импликативных логистических систем.
Теорема дедукции для логистических систем с правилом обобщения.
Дополнительные замечания.
Производные правила вывода для логистических систем гильбертовского типа.
Субординатный вывод.
Системы натурального вывода первого типа.
Критические замечания о различиях между исчислениями гильбертовского типа и системами натурального вывода.
Системы натурального вывода как логистические системы с субординатным выводом.
Модификация понятия вывода в виде леса деревьев.
Натуральные исчисления с субординатным выводом в виде леса последовательностей.
Система записи субординатного вывода по методу Яськовского–Фитча.
Субординатный вывод в нотации Яськовского–Куайна.
Краткое заключение.
Классические секвенциальные исчисления предикатов.
Секвенции. Правила введения и удаления логических знаков.
Классическое секвенциальное логистическое исчисление.
Теорема Эрбрана–Генцена.
Интерполяционная теорема Крейга.
Теорема Бета.
Сингулярное классическое секвенциальное логистическое исчисление.
Секвенциальные исчисления без сокращений.
Секвенциальное логистическое исчисление без сокращений. Разрешимость проблемы разрешения для SLC.
Упрощенная разрешающая процедура для SLC.
Сводимость доказуемости формулы в сколемовской нормальной форме к доказуемости некоторой секвенции из SLC.
Сводима ли проблема разрешения для разрешимых классов SLC к проблеме разрешения для SLC?
Методы установления разрешимости проблемы разрешения для пропозициональных логик.
Абсолютное исчисление предикатов.
Классификация сингулярных секвенциальных исчислений по наличию или отсутствию логических фигур заключения группы IV.
Система SLA.
Абсолютное исчисление предикатов в виде секвенциального натурального исчисления.
Абсолютное исчисление предикатов в форме натурального исчисления.
Абсолютное исчисление предикатов гильбертовского типа.
Проблема разрешения для пропозициональной части SLA, система SLA+.
Исчисления и системы натурального вывода второго типа.
Предварительные замечания.
Определенные и неопределенные дескрипции.
Классическое исчисление гильбертовского типа.
Секвенциальные натуральные исчисления второго типа.
Классическое натуральное исчисление второго типа.
Возможно ли интуиционистское натуральное исчисление предикатов второго типа?
Исчисления DC и DI. Элиминация неопределенных дескрипций для интуиционистского и классического натуральных исчислений.
Правило в формулировке Е. Слупецкого.
Комментарии.
Формальный вывод, теоремы дедукции и теории импликации.
Вывод из списка посылок; релевантные логики и их расширения.
Системы сильной и строгой импликаций с понятием вывода из списка посылок.
Импликативные системы с понятием вывода из последовательности посылок.
Поиск доказательств в натуральном интуиционистском исчислении предикатов.
Представление логических систем с сильной и релевантной импликациями в секвенциальной форме.
Формулировка логистических систем гильбертовского типа с понятием вывода, введенным индукцией по двум переменным.
Подсистемы сильной и релевантной импликации, содержащиеся и интуиционистской логике высказываний.
Системы сильной и релевантной импликаций с законом снятия двойного отрицания.
Об одной системе паранепротиворечивой логики.
Теорема об устранимости сечения для абсолютного исчисления предикатов Генцена без утончений.
Секвенциальная формулировка логики Даммета.
On Decidability of Decision Problem for Sequential Calculus of Predicates without Contractions.
Библиография научных трудов В.А.Смирнова.
В приложении имеется полная библиография работ В.А.Смирнова.
Книга предназначена для логиков, философов и всех интересующихся проблемами логической науки. Содержание
Некоторые логические идеи В.А.Смирнова.
Формальный вывод и логические исчисления предисловие.
Классическая логика предикатов и ее формализация гильбертовского типа.
Язык логики предикатов первого порядка.
Семантика классической логики предикатов первого порядка.
Формализация и аксиоматизация.
Логистические системы гильбертовского типа с понятием формального доказательства. Формализация свойства универсальной общезначимости.
Формализация гильбертовского типа отношения логического следования классической логики предикатов.
Формы выводов и теоремы дедукции для логистических систем гильбертовского типа.
Предварительные замечания.
Вывод как линейная последовательность формул.
Вывод с анализом.
Логистические системы с выводом в виде дерева.
Теорема дедукции для импликативных логистических систем.
Теорема дедукции для логистических систем с правилом обобщения.
Дополнительные замечания.
Производные правила вывода для логистических систем гильбертовского типа.
Субординатный вывод.
Системы натурального вывода первого типа.
Критические замечания о различиях между исчислениями гильбертовского типа и системами натурального вывода.
Системы натурального вывода как логистические системы с субординатным выводом.
Модификация понятия вывода в виде леса деревьев.
Натуральные исчисления с субординатным выводом в виде леса последовательностей.
Система записи субординатного вывода по методу Яськовского–Фитча.
Субординатный вывод в нотации Яськовского–Куайна.
Краткое заключение.
Классические секвенциальные исчисления предикатов.
Секвенции. Правила введения и удаления логических знаков.
Классическое секвенциальное логистическое исчисление.
Теорема Эрбрана–Генцена.
Интерполяционная теорема Крейга.
Теорема Бета.
Сингулярное классическое секвенциальное логистическое исчисление.
Секвенциальные исчисления без сокращений.
Секвенциальное логистическое исчисление без сокращений. Разрешимость проблемы разрешения для SLC.
Упрощенная разрешающая процедура для SLC.
Сводимость доказуемости формулы в сколемовской нормальной форме к доказуемости некоторой секвенции из SLC.
Сводима ли проблема разрешения для разрешимых классов SLC к проблеме разрешения для SLC?
Методы установления разрешимости проблемы разрешения для пропозициональных логик.
Абсолютное исчисление предикатов.
Классификация сингулярных секвенциальных исчислений по наличию или отсутствию логических фигур заключения группы IV.
Система SLA.
Абсолютное исчисление предикатов в виде секвенциального натурального исчисления.
Абсолютное исчисление предикатов в форме натурального исчисления.
Абсолютное исчисление предикатов гильбертовского типа.
Проблема разрешения для пропозициональной части SLA, система SLA+.
Исчисления и системы натурального вывода второго типа.
Предварительные замечания.
Определенные и неопределенные дескрипции.
Классическое исчисление гильбертовского типа.
Секвенциальные натуральные исчисления второго типа.
Классическое натуральное исчисление второго типа.
Возможно ли интуиционистское натуральное исчисление предикатов второго типа?
Исчисления DC и DI. Элиминация неопределенных дескрипций для интуиционистского и классического натуральных исчислений.
Правило в формулировке Е. Слупецкого.
Комментарии.
Формальный вывод, теоремы дедукции и теории импликации.
Вывод из списка посылок; релевантные логики и их расширения.
Системы сильной и строгой импликаций с понятием вывода из списка посылок.
Импликативные системы с понятием вывода из последовательности посылок.
Поиск доказательств в натуральном интуиционистском исчислении предикатов.
Представление логических систем с сильной и релевантной импликациями в секвенциальной форме.
Формулировка логистических систем гильбертовского типа с понятием вывода, введенным индукцией по двум переменным.
Подсистемы сильной и релевантной импликации, содержащиеся и интуиционистской логике высказываний.
Системы сильной и релевантной импликаций с законом снятия двойного отрицания.
Об одной системе паранепротиворечивой логики.
Теорема об устранимости сечения для абсолютного исчисления предикатов Генцена без утончений.
Секвенциальная формулировка логики Даммета.
On Decidability of Decision Problem for Sequential Calculus of Predicates without Contractions.
Библиография научных трудов В.А.Смирнова.