Металогика (Bymglkintg)

Метало́гика — изучение метатеории логики. В то время, как логика представляет собой исследование способов применения логических систем для рассуждения, доказательств и опровержений, металогика исследует свойства самих логических систем.

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

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

Краткий обзор

Формальный язык

Формальный язык (ФЯ) — организованная совокупность элементов, основная особенность которых в том, что они могут быть точно определены в терминах их формы и местоположения (вхождения). В этом случае язык поддается определению без какого-либо обращения к содержательным значениям его выражений, то есть он может быть фиксирован прежде чем для него назначена какая-либо интерпретация (определен некоторый смысл). Логика первого порядка выразима на таком формальном языке. Формальная грамматика определяет, какие элементы и последовательности элементов являются формулами этого языка.

Формальный язык может быть определен как множество А строк (конечных последовательностей) символов некоторого фиксированного алфавита О+. Некоторые авторы, включая Карнапа, определяют язык как упорядоченную пару. Карнап требует при этом, чтобы каждый символ из О+ встречался в А не менее чем в одной строке.

Правила формирования

Правила формирования (называемые также формальной грамматикой) — точное описание правильно сформированных строк формального языка. Эти правила задают множество строк над алфавитом, которое состоит из правильно построенных формул (п.п.ф.). Однако правила не описывают семантику формул (то, что они означают).

Формальные системы

Формальная система (называемая также логическим исчислением или логической системой) состоит из формального языка вместе с аппаратом дедукции (дедуктивной системой). Дедуктивный аппарат может состоять из правил преобразования (называемых также правилами вывода) или набора аксиом, но может включать оба эти компонента. Формальная система используется для вывода некоторого выражения из (одного или более) других выражений.

Формальная система также может быть определена как упорядоченная тройка, где d — отношение непосредственной выводимости. Это отношение понимается в том смысле, что элементарные (исходные, атомарные) предложения формальной системы берутся как непосредственно выводимые из пустого множества предложений. Непосредственная выводимость — отношение между предложением и конечным, возможно пустым, множеством предложений. Аксиомы записаны таким способом, что каждый первый компонент отношения d является предложением (формулой), а каждый второй компонент есть конечное (под)множество предложений.

Можно определять формальную систему, используя только отношение d. Этим способом мы можем опускать О± в определениях интерпретируемых формального языка и формальной системы. Однако этот метод, вероятно, труднее понять и работать с ним. [3]

Формальные доказательства

Формальное доказательство — последовательность правильно построенных формул ФЯ, последняя из которых рассматривается как теорема формальной системы. Теорема — синтаксическое следствие всех предыдущих п.п.ф. этого доказательства. Чтобы квалифицировать п.п.ф-лу как часть доказательства, она должна быть результатом применения некоторого правила дедуктивного аппарата к предыдущим п.п.ф. доказательства.

Интерпретации

Интерпретация формальной системы заключается в присвоении значений символам, и истинностных значений — предложениям формальной системы. Изучением интерпретаций занимается Формальная семантика. Построение интерпретации близко к процессу построения модели.

Важные разграничения в металогике

Метаязык — язык-объект

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

Синтаксис — семантика

В металогике 'синтаксис' рассматривает ФЯ или формальные системы без учета их интерпретации, тогда как 'семантика' связывается с интерпретациями ФЯ. Термин 'синтаксический' охватывает немного более широкий контекст чем термин 'теоретико-доказательный', так как может быть применен к свойствам ФЯ безотносительно к любой дедуктивной системе, а также к формальным системам. 'Семантический' синонимичен с термином 'теоретико-модельный'.

Использование — упоминание

В металогике, слова «использование» и «упоминание» — в формах существительного и глагола — идентифицируют важное различие, а именно: различие между использованием слова (или фразы) и упоминанием о нём. Обычно для обозначения того, что выражение упоминается, а не используется, применяют кавычки, курсив, или записывают выражение в отдельной строке. Использование кавычек дает нам имя (название) выражения, например: «Металогика» — название этой статьи. Эта статья — о металогике.

Тип — маркер

Различие тип — маркер отделяет абстрактное понятие от объектов, являющихся частными случаями (примерами, экземплярами) этого понятия. Например, конкретный велосипед в вашем гараже — частный случай (экземпляр) типа сущности, известной как «велосипед». Примем во внимание, что велосипед в вашем гараже находится в конкретном месте в конкретное время, и эти обстоятельства неприменимы для «велосипеда» в предложении: «велосипед стал более популярным недавно». Это различие используется, чтобы прояснить значения символов ФЯ.

История

Вопросы металогической направленности возникали уже во времена Аристотеля. Однако только с появлением ФЯ в конце 19-го и в начале 20-го столетия исследования по основаниям логики начали расширяться. В 1904 Д.Гильберт заметил, что в исследованиях по основаниям математики существенно используются логические понятия, и поэтому требуется одновременное согласованное рассмотрение металогических и метаматематических принципов . В современной трактовке металогика и метаматематика в значительной степени перекрываются, и обе эти дисциплины существенно связаны с математической логикой.

Результаты, полученные в металогике

Результаты металогики в значительной степени состоят из формальных доказательств, демонстрирующих непротиворечивость, полноту и разрешимость конкретных формальных систем. Главные результаты металогики включают:

• Доказательство несчетности множества всех подмножеств множества натуральных чисел (теорема Кантора, 1891)
• Теорема Лёвенгейма — Скулема (1920)
• Доказательство непротиворечивости пропозициональной логики (Эмиль Пост, 1920)
• Доказательство семантической полноты пропозициональной логики (П.Бернайс, 1918), [4] (Э.Пост, 1920) [2]
• Доказательство синтаксической полноты пропозициональной логики (Эмиль Пост, 1920) [2]
• Доказательство разрешимости пропозициональной логики (Эмиль Пост, 1920) [2]
• Доказательство непротиворечивости первопорядковой одноместной логики предикатов (Л. Левенгейм, 1915)
• Доказательство семантической полноты первопорядковой одноместной логики предикатов (Л. Левенгейм, 1915)
• Доказательство разрешимости первопорядковой одноместной логики предикатов (Л.Левенгейм, 1915)
• Доказательство непротиворечивости первопорядковой логики предикатов (Д.Гильберт и В.Акерманн, 1928)
• Доказательство семантической полноты первопорядковой логики предикатов (теорема полноты Гёделя, 1930)
• Доказательство неразрешимости первопорядковой логики предикатов (теорема Чёрча, 1936)
• Первая теорема неполноты Геделя, 1931
• Вторая теорема неполноты Геделя, 1931
• Теорема Тарского о невыразимости истины (Гедель и Тарский, 1936)

Литература

• Металогика // Большая советская энциклопедия : [в 30 т.] / гл. ред. А. М. Прохоров. — 3-е изд. — М. : Советская энциклопедия, 1969—1978.
• Под редакцией А.А. Ивина. Металогика // Философия: Энциклопедический словарь. — Гардарики (рус.). — М., 2004.
• Hunter, Geoffrey, Metalogic: An Introduction to the Metatheory of Standard First-Order Logic, University of California Press, 1971