Metalogic - Metalogic

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

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

Обзор

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

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

Формальный язык можно формально определить как набор A строк (конечных последовательностей) на фиксированном алфавите α. Некоторые авторы, в том числе Рудольф Карнап , определяют язык как упорядоченную пару <α, A >. Карнап также требует , чтобы каждый элемент & alpha ; должен происходить , по меньшей мере , одной строки в A .

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

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

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

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

Формальная система может быть формально определена как упорядоченные тройной <а, , д>, где d представляет собой отношение прямого выводимости. Это отношение понимается в комплексном смысле , так что примитивные предложения формальной системы принимаются , как непосредственно выводима из пустого множества предложений. Прямая выводимость - это отношение между предложением и конечным, возможно, пустым набором предложений. Аксиомы выбираются таким образом, что каждый член, занимающий первое место в d, является членом, а каждый член, занимающий второе место, является конечным подмножеством . ${\ displaystyle {\ mathcal {I}}}$${\ displaystyle {\ mathcal {D}}}$${\ displaystyle {\ mathcal {D}}}$${\ displaystyle {\ mathcal {D}}}$${\ displaystyle {\ mathcal {I}}}$${\ displaystyle {\ mathcal {I}}}$

Формальная система также может быть определена только с соотношением д. Таким образом, можно опустить и α в определениях интерпретируемого формального языка и интерпретируемой формальной системы . Однако этот метод сложнее понять и использовать. ${\ displaystyle {\ mathcal {D}}}$${\ displaystyle {\ mathcal {I}}}$

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

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

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

Интерпретация формальной системы является присвоение значений к символам и истинностные значения в предложениях формальной системы. Изучение интерпретаций называется формальной семантикой . Интерпретация - синоним построения модели .

Важные отличия

Метаязык – объектный язык

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

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

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

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

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

«Metalogic» - это название этой статьи.

Эта статья о металогике.

Тип – токен

Типа маркеров различия есть различие в металогики, которая отделяет абстрактное понятие от объектов , которые являются частными случаями концепции. Например, конкретный велосипед в вашем гараже является лексемой типа вещей , известных как «велосипед» . В то время как велосипед в вашем гараже находится в определенном месте в определенное время, это не относится к «велосипеду», используемому в предложении: « Велосипед в последнее время стал более популярным». Это различие используется , чтобы разъяснить смысл символов на формальных языках .

История

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

Полученные результаты

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

Основные результаты в металогике включают:

• Доказательство несчетности из набора мощности из натуральных чисел ( теорема Кантора 1891)
• Теорема Левенхайма – Сколема ( Леопольд Левенгейм, 1915 г. и Торальф Сколем, 1919 г.)
• Доказательство непротиворечивости истинностно-функциональной логики высказываний ( Эмиль Пост, 1920)
• Доказательство семантической полноты истинностно-функциональной логики высказываний ( Пол Бернейс, 1918), (Эмиль Пост, 1920)
• Доказательство синтаксической полноты истинностно-функциональной логики высказываний (Эмиль Пост, 1920)
• Доказательство разрешимости истинностно-функциональной логики высказываний (Эмиль Пост, 1920)
• Доказательство непротиворечивости монадической логики предикатов первого порядка ( Леопольд Левенхайм, 1915)
• Доказательство семантической полноты монадической логики предикатов первого порядка (Леопольд Левенхайм, 1915)
• Доказательство разрешимости монадической логики предикатов первого порядка (Леопольд Левенхайм, 1915)
• Доказательство непротиворечивости логики предикатов первого порядка ( Дэвид Гильберт и Вильгельм Акерманн, 1928)
• Доказательство семантической полноты логики предикатов первого порядка ( теорема Гёделя о полноте 1930 г.)
• Доказательство теоремы покроя-элиминирования для секвенции исчисления ( генценовский «s Hauptsatz 1934)
• Доказательство неразрешимости логики предикатов первого порядка ( теорема Чёрча 1936 г.)
• Первая теорема Гёделя о неполноте 1931 г.
• Вторая теорема Гёделя о неполноте 1931 г.
• Теорема Тарского о неопределенности (Гедель и Тарский в 1930-е годы)

Смотрите также

• Металогическое программирование
• Метаматематика

Рекомендации

Внешние ссылки

• СМИ, связанные с Metalogic на Викискладе?
• Драгалин, А.Г. (2001) [1994], «Мета-логика» , Энциклопедия математики , EMS Press