ФЭНДОМ


Математическая логика (теоретическая логика, символическая логика) — раздел математики, изучающий доказательства и вопросы оснований математики. «Предмет современной математической логики разнообразен.»[1] Согласно определению П. С. Порецкого, «математическая логика есть логика по предмету, математика по методу». Согласно определению Н. И. Кондакова, «математическая логика — вторая, после традиционной логики, ступень в развитии формальной логики, применяющая математические методы и специальный аппарат символов и исследующая мышление с помощью исчислений (формализованных языков)[2] Это определение соответствует определению С. К. Клини: математическая логика — это «логика, развиваемая с помощью математических методов».[3] Так же А. А. Марков определяет современную логику «точной наукой, применяющей математические методы».[4] Все эти определения не противоречат, но дополняют друг друга.

Применение в логике математических методов становится возможным тогда, когда суждения формулируются на некотором точном языке. Такие точные языки имеют две стороны: синтаксис и семантику. Синтаксисом называется совокупность правил построения объектов языка (обычно называемых формулами). Семантикой называется совокупность соглашений, описывающих наше понимание формул (или некоторых из них) и позволяющих считать одни формулы верными, а другие — нет.

Важную роль в математической логике играют понятия дедуктивной теории и исчисления. Исчислением называется совокупность правил вывода, позволяющих считать некоторые формулы выводимыми. Правила вывода подразделяются на два класса. Одни из них непосредственно квалифицируют некоторые формулы как выводимые. Такие правила вывода принято называть аксиомами. Другие же позволяют считать выводимыми формулы $ A $, синтаксически связанные некоторым заранее определённым способом с конечными наборами $ A_1, \ldots A_n $ выводимых формул. Широко применяемым правилом второго типа является правило modus ponens: если выводимы формулы $ A $ и $ (A\to B) $, то выводима и формула $ B $.

Отношение исчислений к семантике выражается понятиями семантической пригодности и семантической полноты исчисления. Исчисление И называется семантически пригодным для языка Я, если любая выводимая в И формула языка Я является верной. Аналогично, исчисление И называется семантически полным в языке Я, если любая верная формула языка Я выводима в И.

Многие из рассматриваемых в математической логике языков обладают семантически полными и семантически пригодными исчислениями. В частности, известен результат К. Гёделя о том, что так называемое классическое исчисление предикатов является семантически полным и семантически пригодным для языка классической логики предикатов первого порядка. С другой стороны, имеется немало языков, для которых построение семантически полного и семантически пригодного исчисления невозможно. В этой области классическим результатом является теорема Гёделя о неполноте, утверждающая невозможность семантически полного и семантически пригодного исчисления для языка формальной арифметики.

Стоит отметить, что на практике множество элементарных логических операций является обязательной частью набора инструкций всех современных микропроцессоров и соответственно входит в языки программирования. Это является одним из важнейших практических приложений методов математической логики, изучаемых в современных учебниках информатики. И если в школьные учебники информатики включено изучение булевой алгебры и логических элементов и функций, то в вузовские учебники информатики В. А. Каймина вошло изучение принципов логического программирования вместе с элементами исчисления предикатов и принципов логического вывода.

Использование логического подхода В. А. Каймина к исследованиям в области искусственого интеллекта и логическому проектированию баз знаний и экспертных систем в 80-х годах ХХ века открыло путь к подготовке студентов и школьников к проектированию и эксплуатации интеллектуальных информационных систем.

Особый интерес к математической логике представляют технологии доказательного программирования В. А. Каймина, предполагающая разработку алгоритмов и программ с доказательствами правильности алгоритмов. Особенность технологий доказательного программирования состоит в необходимость написания не только алгоритмов и программ, но и написания вместе с ними доказательств отсутствия в них ошибок. Что всегда считалось чисто математической деятельностью.

См. также Править

Примечания Править

  1. С. И. Адян, Математическая энциклопедия, М.: «Советская энциклопедия», т.3, с. 568, 571.
  2. Н. И. Кондаков, Логический словарь-справочник, М.: «Наука», 1975, с. 259.
  3. С. К. Клини, Математическая логика, М., 1973, с.12.
  4. А. А. Марков, Большая советская энциклопедия, Изд. 3, Предмет и метод современной логики.

Литература Править

  • Марков А. А.. Элементы математической логики. М.: Изд-во МГУ, 1984.
  • Новиков П. С. Элементы математической логики. 2-ое изд. М.: Наука, 1973. — 400 с.
  • Столл Р. Р. Множества. Логика. Аксиоматические теории. М.: Просвещение, 1968. — 232 с.
  • Стяжкин Н. И. Формирование математической логики. М.: Наука, 1967. 508 с.
  • Шенфилд Дж. Математическая логика. М.: Наука, 1975.
  • В. А. Каймин. Информатика. Учебник. 5-ое издание. М.. ИНФРА-М. С.244 с ил. ISBN 5-16-002584-7
  • В. А. Каймин. Основы доказательного программмирования. М., МИЭМ, 1986.
  • В. А. Каймин. Интерпретатор языка Пролог. В учебнике информатики В. А. Каймина. с.256-369.

Ссылки Править


Эта страница использует содержимое раздела Википедии на русском языке. Оригинальная статья находится по адресу: Математическая логика. Список первоначальных авторов статьи можно посмотреть в истории правок. Так же, как и в этом проекте, тексты, размещённые в Википедии, доступны на условиях GNU FDL.