Металогика

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

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

Обзор

Официальный язык

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

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

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

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

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

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

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

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

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

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

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

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

Важные различия

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

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

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

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

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

В металогике слова «использовать» и «упоминать», как в форме существительного, так и в форме глагола, приобретают технический смысл, чтобы выявить важное различие. ^[2] Различие между использованием и упоминанием (иногда называемое различием «слова как слова» ) — это различие между использованием слова (или фразы) и его упоминанием . Обычно указывается, что выражение упоминается, а не используется, заключая его в кавычки, печатая курсивом или помещая само выражение в строку. Заключение выражения в кавычки дает нам имя выражения, например:

«Металогика» — название этой статьи.

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

Тип – токен

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

История

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

Результаты

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

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

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

См. также

Ссылки

^ Гарри Генслер, Введение в логику , Routledge, 2001, стр. 336.
^ Перейти обратно: ^а ^б ^с ^д ^и Хантер, Джеффри , Металогика: введение в метатеорию стандартной логики первого порядка , University of California Press, 1973.
^ Перейти обратно: ^а ^б Рудольф Карнап (1958) Введение в символическую логику и ее приложения , с. 102.
^ Смит, Робин (2022), «Логика Аристотеля» , в Залте, Эдвард Н.; Нодельман, Ури (ред.), Стэнфордская энциклопедия философии (изд. зимой 2022 г.), Лаборатория метафизических исследований, Стэнфордский университет , получено 28 августа 2023 г.
^ Хао Ван, Размышления о Курте Гёделе

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

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

[1] Гарри Генслер, Введение в логику , Routledge, 2001, стр. 336.

[metalogic-2] Перейти обратно: ^а ^б ^с ^д ^и Хантер, Джеффри , Металогика: введение в метатеорию стандартной логики первого порядка , University of California Press, 1973.

[itslaia-3] Перейти обратно: ^а ^б Рудольф Карнап (1958) Введение в символическую логику и ее приложения , с. 102.

[4] Смит, Робин (2022), «Логика Аристотеля» , в Залте, Эдвард Н.; Нодельман, Ури (ред.), Стэнфордская энциклопедия философии (изд. зимой 2022 г.), Лаборатория метафизических исследований, Стэнфордский университет , получено 28 августа 2023 г.

[reflections-5] Хао Ван, Размышления о Курте Гёделе

[1]

[2]

[3]

[4]

[5]