Символическая логика

Дисциплина символической логики была придумана задолго до своего появления Готфридом Вильгельмом фон Лейбницем, первые попытки которого не принесли значительных результатов.

Вопрос о создании символической логики как универсального научного языка рассматривал Лейбниц в 1666 году в работе «Искусство комбинаторики» (De arte combinatoria). Он думал о записи высказываний на специальном языке, чтобы затем по логическим законам вычислять истинность других. В середине XIX века появились первые работы по алгебраизации аристотелевой логики, сформировавшие первооснову исчисления высказываний (Буль, де Морган, Шрёдер).

Хотя в то время эта идея не получила большого распространения, она стала источником символической логики, разработанной Джорджем Булем, а затем развитой Альфредом Нортом Уайтхедом и Бертраном Расселом.

В конце 1880-х годов Дедекинд и Пеано применили эти инструменты в попытках аксиоматизации арифметики, при этом Пеано создал удобную систему обозначений, закрепившуюся и в современной математической логике. Он ввёл в математическую логику символы: ∈ — знак принадлежности множеству, ⊂ — знак включения, ⋃ — знак объединения, ∩ — знак пересечения множеств; разработал систему аксиом для арифметики натуральных чисел. Но главное, Пеано с помощью изобретённого им символического исчисления попытался исследовать основные математические понятия, что стало первым шагом практического применения математической логики к изучению основ математики. В своём пятитомном труде «Formulaire de Mathematiques» (1895—1905) Пеано показал, как с помощью символического исчисления можно аксиоматически построить математические дисциплины.

Первый учебник по символической логике для неспециалистов был написан Льюисом Кэрроллом, автором «Алисы в стране чудес», в 1896 году.^[2]

Леопольд Лёвенгейм^[3] и Туральф Сколем^[4] получили теорему Лёвенгейма — Скулема, согласно выводам которой, логика первого порядка не позволяет контролировать кардинальность бесконечных структур. Сколем заметил, что эта теорема применима к формализациям теории множеств первого порядка и поэтому из теоремы следует, что любая такая формализация имеет структуру счётного множества. Данный контринтуитивный факт стал известен как парадокс Скулема.

В своей докторской диссертации, Курт Гёдель доказал теорему о полноте, устанавливающую соответствие между синтаксисом и семантикой в логике первого порядка.^[5] С помощью теоремы о полноте Гёдель доказал теорему о компактности, продемонстрировав тем самым ограниченность логических следствий первого порядка. Результаты помогли утвердить логику первого порядка в качестве доминирующей логики, используемой математиками.

В 1931 году, Гёдель опубликовал работу «О формально неразрешимых Principia Mathematica и родственных систем», в которой доказал неполноту (в другом значении этого слова) всех достаточно сильных, эффективных теорий первого порядка. Этот результат, известный как теорема Гёделя о неполноте, устанавливает серьезные ограничения на аксиоматические основания математики и сильно подрывает программу Гильберта. Теорема неполноты свидетельствует о невозможности доказательства непротиворечивости арифметики в рамках любой формальной теории арифметики. Однако Давид Гильберт долгое время не признавал важности теоремы о неполноте.

Теорема неполноты Гёделя также указывает на то, что доказательство непротиворечивости любой достаточно сильной, эффективной системы аксиом не может быть получено ни в самой системе, если она непротиворечива, ни в какой-либо более слабой системе. Таким образом, возникает возможность существования доказательств непротиворечивости, которые не могут быть формализованы в рамках рассматриваемой системы. Генцен доказал непротиворечивость арифметики, используя финитистскую систему вместе с принципом трансфинитной индукции.^[6] Результат Генцена позволил ввести идеи устранимости сечений и порядковый анализ, которые стали ключевыми инструментами теории доказательств. Гёдель дал другое доказательство непротиворечивости, которое сводит непротиворечивость классической арифметики к непротиворечивости интуиционистской арифметики в высших типах.^[7]

Логика высказываний изучает свойства пропозиций в терминах их констант и ссылок на переменные, таких как A, B, C, ... и пяти операторов: И (AND), ИЛИ (OR), IMPLIES, EQUALS и НЕ (NOT). А также с помощью символов ${\displaystyle \land ,\lor ,\rightarrow ,\leftrightarrow }$  и ${\displaystyle \neg }$ .

Соответствующими логическими операциями являются конъюнкция, дизъюнкция, импликация, эквивалентность и отрицание. Все эти операции, кроме НЕ, являются бинарными. Смысл этих операций описывается таблицами истинностных значений.

Логика первого порядка является расширением логики высказываний, в которой вводятся переменные, пропозиции или предикаты. Переменные обычно обозначаются строчными буквами x, y, z и т.д., а предикаты — прописными, например P(x) или Q(y,z). Кроме того, используются кванторы, которые описывают всеобщность ( квантор всеобщности ${\displaystyle \forall }$  ) и существование ( квантор существования ${\displaystyle \exists }$  ).

В языке программирования Пролог применяется логика первого порядка, поэтому он также поддерживает символическую логику и, соответственно, возможность программной обработки.

Программы на языке Пролог описывают отношения с помощью пунктов. Проще говоря, Пролог ограничен формулами Хорна, который является тьюринг-полным подмножеством предикатов логики первого порядка. И имеет два типа пунктов: факты и правила.

Правило имеет вид:

 Заголовок:- тело.

Оно гласит: «Заголовок истинен, если тело истинно». Тело правила состоит из предикатных высказываний, называемых целью правила. Встроенная в Пролог функция запятая (,/2) определяет конъюнкцию целей, а точка с запятой (;/2) — дизъюнкцию. Конъюнкция и дизъюнкция могут встречаться в теле правила, но не в заголовке [имени].

Предложения, в которых отсутствует часть тела, называются фактами. Например,

Том — кот:

кот(Том).

Факт работает как уменьшенная реляционная база данных. Так, в Пролог можно запросить имена всех котов по очереди:

?- кот(X). 
X = Том

Выполнение Пролог начинается с единственной цели, называемой запросом. Механизм рассуждений Пролог пытается найти отрицательное условие в соответствии с принципом разрешения.

Если отрицание не найдено, то из этого следует, что з��прос с его допустимыми значениями переменных будет подтверждён. Таким образом, реализуется соответствующая логическая цепочка в программе. В этом случае все сгенерированные значения переменных возвращаются пользователю, и запрос считается успешным. Функционально стратегию выполнения Пролог можно рассматривать как обобщение вызовов функций в типичных языках программирования (Java, C++, Pascal), но особенностью Пролог является то, что для одного и того же оператора, даже с одинаковыми аргументами, может существовать несколько альтернативных заголовков. В этом случае Пролог создает точку выбора, которая объединяет различные альтернативные варианты. Затем Prolog начинает выполнять возможные варианты с самого начала. При выполнении конкретного варианта — в зависимости от так называемого термина отсечения — пытаются быть выполнены и следующие варианты точки выбора (предложения) или принимается только один вариант. Если один запрос в предложении не выполняется, то значения переменных, присвоенные ему, отменяются, и выполнение возвращается к предыдущей точке выбора и продолжается со следующего варианта, если таковой остался. Такая операция отмены и повторного выполнения называется обратной загрузкой.

Например, все люди смертны, и в частности, утверждается, что Сократ — человек:

 смертный(Х):- человек(Х). 
 человек(Сократ).

Следующий запрос возвращает информацию о том, что Сократ смертен, потому что он является человеком:

?- смертный (Сократ).
Да.

• Бродский И. Н. Элементарное введение в символическую логику. — Издательство Ленинградского университета, 1972. — 63 с.

• А. С. Карпенко. Логика символическая // Новая философская энциклопедия : в 4 т. / пред. науч.-ред. совета В. С. Стёпин. — 2-е изд., испр. и доп. — М.: Мысль, 2010. — 2816 с.

• Alfred Tarski: Introduction to Logic and to the Methodology of Deductive Sciences (2nd ed.): Logical Constants (1946)
• A.H. Basson and D.J. O'Connor: Introduction to Symbolic Logic (3rd ed.): Chapter  Introductory: . Symbolic Logic and Classical Logic (1959)
• E.J. Lemmon: Beginning Logic: Chapter: The Propositional Calculus: The Nature of Logic (1965)
• Irving M. Copi: Symbolic Logic (4th ed.): Introduction: Logic and Language: Symbolic Logic (1973)
• D.J. O'Connor and Betty Powell: Elementary Logic: The Logic of Statements (1980)
• Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems: Declarative sentences (2000)

• Математическая логика
• Символический анализ (Symbolinen analyysi)
• Символический анализ данных (Symbolic data analysis)