Математическая Логика, 01 лекция (от 24 сентября)
Материал из eSyr's wiki.
Предыдущая лекция | Следующая лекция
zakharov@mathcyb.cs.msu.su mathcyb.cs.msu.su/courses/ongoing.html
Лекция 1.
Содержание |
Что изучает логика
Логика обслуживает большое количество наук. Логика изучает законы окружающего мира. Предполагая, что в мире происходит то, что мы представляем, можно заметить, что в нём есть закономерности, какие-то конфигурации возможны, какие-то нет. То есть, возникают закономерности, причём событий разных. Тогда возникает предположение о том, что наряду с частными законами, касающимися физического, химического устройства нашего мира, есть такие законы, которые доминируют над ними всеми — законы причинно-следственной связи. Первая сторона логики.
Жизнь человека состоит из того, что он пытается предвидеть, что происходит в этом мире, на основании знаний о мире. Человек опирается на законы причино-следоственной связи. То есть, законы влияют на мышление человека. При этом, то, что думает человек о законах, не есть законы. Изучение понимания человека — вторая сторона логики.
Третья сторона — исследование отражения причинно-следственных законов в языках.
Отсюда видно, что дисциплины, заинтересованные в логике, достаточно своеобразны. Философия, математика, информатика. Мы будем изучать именно логику для информатики. Это достаточно специализированный курс, который правильнее назвать "прикладная логика".
Во второй половине курса будет краткий обзор тех направлений, которые интересны для математики. Но в основном для информатики оно интересно в плане законов преобразования информации, основанных на причинно-следственной. связи.
В первую очередь нас будет интересовать формальная логика.
Пример: каждый металл — проводник, ртуть — металл ↔ ртуть — проводник.
Были чудаки в то время, которые механическим способом пытались получать новые знания, были осмеиванны. Свифт в Гулливере осмеял эту мысль.
Вторая мысль: Если мы сумеем все эти законы математизированные составить настолько полно, что они полностью описывают все законы, то, построив механическое устройство, которое реализует их всех, мы получим универсальный решатель задач.
Три закона из разных областей, но они имеют общую форму: ∀R обладает свойством Q; С обладает свойством Q ↔ C обладает свойством Q. Такой закон в формальном виде есть закон формальной логики. Он выражает взаимосвязь между явлениями вне зависимости от их сути. И формальная логика изучает законы такого рода.
Можно представить эти законы в симольном виде: ∀(R(x) → Q(x)); R(c) ↔ Q(c). Закон в символьной логике.
Математическая логика изучает законы в символьном виде. Причём лектор будет подавать эти законы под соусом информатики.
Законы формальной логики есть законы преобразования знаний. Для получения новых знаний необязательно представлять суть знаний, достаточно представить форму, и тогда логика, работая с формами, сможет представить новые знания.
Можно ли считать, что логика — генератор информации? Нет. Знания мы получаем из жизненного опыта. Логика занимается преобразованием формальной информации. Законы формальной логики — инструменты преобразования информатики.
Основная задача формальной логики
Предположим, что есть база знаний, представленная в виде утверждений. У нас есть некое предположение (гипотеза, запрос к БЗ). Нужно выяснить, является ли предположение следствием фактов знаний. То есть, нам нужен инструмент, способный выводить новые знания на основе БЗ.
Какие приложения можно найти?
- Экспертные системы. Все следствия из того, что надиктовал уволенный за ненадобностью эксперт, можем получать из ЭС практически автоматически.
- Автоматизация научных исследований. Курс состоит из того, что сначала надиктовывается фактическая информация, а потом доказываем теоремы, то есть делаем выводы на основании фактов. Это можно делать автоматически. Если мы выразим все факты, то у нас будет ядро АНИ.
Что для этого нужно уметь?
- Разработать формальный язык представления знаний. Он должен быть таким, чтобы математика могла работать с его использованиеи как на формальном, так и на смысловом уровне.
- Reference implementation формальной логики
- Проверить корректность логических законов
- Проверить полноту системы формальных законов. То есть проверить, что коли всякое утверждение является следствием, то нужно проверить вывод. То есть, система должна уметь доказывать.
В каком порядке мы должны применять законы? Мы должны разработать алгоритм, который позволяет делать вывод законов на основании имеющихся. Этим мы будем заниматься в первой части курса.
Кроме факта наличия алгоритма неоходимо, чтобы он был оптимизирован. Этим будем заниматься во второй части курса.
Программирование
Вычисление программы — преобразование одних состояний в другие согласно алгоритму.
Логический вывод — последовательное постороение по законам формальной логики одних из других, исходя из БЗ.
Вывод налицо. Соответственно, хотелось бы автоматизировать связанные с этим задачи по аналогии с выполнением программы.
Существует ли такие иррациональные α и β, что αβ — рациональное? — пример простого неконструированного доказательства.
Разработкой языка для МЛ займёмся в третьей части курса.
Проверка правильности програм
Программист — человек, который тратит вторую половину жизни на то, чтобы исправить ошибки из первой половины.
Существует задача формальной проверки программ. Для этого нужно:
- Наличие языка для описание правильности программ
- Правила логического доказательства языка
- Алгоритм применения правил
История логики
Нельзя исключать влияние личности на создание различных отделов математики и логики.
Аристотель
Первый выявил законы формальной логики, «силогизмы». Написал труд о формальной логике. Открытие того, что законы носят формальный характер — заслуга философа.
Далее силогизмы расширялись, следовали различные проявления, разная интерпретация: греческие философы считали, что это законы идеального мира, христианские — божий промысел.
Логика так развивалась 2000 лет, пока её не занялись математики.
Лейбниц
Специалист широкого профиля.
Ему принадлежит несколько выводов, связанные с логикой. Один из них: «Как законы дифференциальных уравнений создают законы механики, механики позволяют строить механизмы, ... законы логики могут создавать мышление. Более того, можно строить механические устройства для ...»
Преобразование информации на основе двоичной системы счисления принадлежит Лейбницу.
Джордж Буль
Скромный математик. У него, как у любого истинно английского джентельмена было хобби, философия, законы мышления, он пытался нащупать формальную алгебру для их представления. И он нащупал булеву алгебру, о чём всех оповестил. И для философии, которая искала такой аппарат, получила интересный материал.
Готтлоб Фрегге
Законы Буля описывали довольно малую часть матлога, и он пытался придумать язык для формального её описания. Более того, он считал, что можно представить всю математику таким исключительным языком. Получалось у него плохо, он был немцем, пунктуальным. Тем не менее, он понял, что математическое доказательство это объект математики. Те мне менее, его идеи заразили многих математиков, и появились предпосылки для создания строгой науки, формальной логики, имеющей математические корни.
Давид Гильберт
Совершил значительную работу, завершил геометрию, конкретно, завершил работу Евклида по аксиматизации геометрии. В то время появились многие другие геометрии, и надо было понять, какая из аксиоматик правильная, в частности, показать, что из неё нельзя вывести две противоречивых вещи. Лобачевский долго пытался доказать от противного, но не смог. Завершил это Гильберт, проанализаровав геометрию Евклида, создал систему из 27—28 аксиом, и сказал, что она столь же не противоречива, сколь не противоречива арифетика, кроме того, любая другая альтернативная геометрия столь же не противоречива. Таким образом, формальная логика заработала, она начала решать практические задачи.
Так как к арифметике сводится всё-всё-всё, Гильберт задался вопросом: а нельзя ли создать аксиоматику для всей математику? Эта система должна быть выразительна настолько, что в ней можно представить любую область математики. Эта система должна была описывать не только числа и фигуры, но и теоремы, утвреждения, доказательства. Тогда бы мы получили математическое здание, внутри которого заключены все истины. Это вроде троллей, которые пытались затащить на небо зеркало, чтобы обсмеять Бога. Это была так называемая программа Гильберта — аксиоматизации математики.
Поскольку это была суперзадача, то многие математики заинтересовались этой программой.
Гильберт был очень темпераментный, но, тем не менее, оставил большой след в математике. Всем известна ОТО Эйнштейна, но он был хороший физик и плохой математик, и работал в паре с Гильбертом, который создавал для ОТО математический аппарат. Другое — квантовая физика, там тоже красивая математика. Математики из школы Гильберта и сам Гильберт занимались разработкой математического аппарата для квантовой физики.
Бертран Рассел
Философ, политик, граф, либерал.
Он разработал формальный язык. Кванторы — его изобретение. Он аксиоматизировал логику. Он заложил при помощи этих законов основы математики. Написал трёхтомник, в котором описал математику формально с нуля. Эта книжка подвела строгий математический базис под всеми основными математическими понятиями.
Действительно интересный человек, его жизнь — сплошной роман, приблизительно такой же, как жизнь Байрона. Ярый пацифист. Имел беседу с Ленином, в Ленине разочаровался, в социализме — нет. Прочитал лекции в Китае. Занимался пропагандой социализма, изгонялся из факультетов за вольнодумство. Неоднократно арестовывался. Блестящий философ, написал книгу "история западно-европейской философии", ставшую бестселлером (а сейчас «Гарри Поттер» — бестселлер). Написал письмо Кеннеди и Хрущёву, и оба ответили.
Начало 60-х годов, не было ни одной логической книжки.
Курт Гёдель
Разбил зеркало Гильберта, осколки разлетелись по всему миру, попали во всех математиков и у них изменилось зрение.
Показал, что нельзя построить ни конечную, ни сколько нибудь хорошую систему аксиом, охватывающую все свойства натуральных чисел. То есть, математика неохватываема.
Альфред Тарский
Объяснил, что такое истина, что такое истинное утверждение. Это важный вопрос, так как до этого занимались только тем, что такое доказуемое и нет.
Это был общительный математик, оставил много учеников, материалов. Оставил теорию игрушек.
Допустим, есть яблоко. Его можно разрезать на 5 частей так, что получится два такого же объёма без полостей. Если с полостями, то 4.
Жак Эрбран
Спустя три дня после начала восхождения в честь ... он сорвался и погиб
Герхард Генцен
Те математические законы, которые были, были неудобны. Они были хороши с точки зрения математики, но плохи с точки зрения работы с ними. Он предложил другие варианты доказательства, с которыми легче работать. Нашёл лазейку, которая позволит выйти из теории неаксиоматизации Геделя, используя трасинфинитную индукцию вместо математической и большие числа, можно провести полную аксиоматизацию.
Алан Колмероэ
Не очень значительный, но сделал то, что хотелось бы, чтобы происходило чаще.
Обратил внимание на то, что логический вывод спец. типа очень похож на вычисление и написал язык Пролог.
Михаил Захарьящев
Автор концепции курса, который лектор читает. Его область изучения — модальные логики.
Логические парадоксы
Движущая сила логики — парадоксы. Математики двигают её не просто так, а для решения задач. Математическую логику они развивали для получения инструментария доказательства утвреждений. Чтобы не сталкиваться с парадоксами.
Примеры парадоксов: парадоксы лжеца и др.
Парадоксы неизбежны, но формальный подход позволяет ограничить их влияние. Для этого нужны матмодели. Следовательно, нужна матлогика.
Если нравится решать логические задачи, то лектор рекомендует книгу Реймонд С. Смаллиан "Как же называется эта книга?"
