Полнота (логика)

Не путать с Complete (сложность) .

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

Другие свойства, связанные с полнотой

Основные статьи: Обоснованность и последовательность

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

Формы полноты

Выразительная полнота

Формальный язык если выразительно завершен, он может выразить предмет, для которого он предназначен.

Функциональная полнота

Основная статья: Функциональная полнота

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

Семантическая полнота

Семантическая полнота является противоположностью правильности . формальных систем Формальная система является полной относительно тавтологичности или «семантически полной», когда все ее тавтологии являются теоремами , тогда как формальная система является «здравой», когда все теоремы являются тавтологиями (то есть они являются семантически действительными формулами: формулами, которые истинны при каждом интерпретация языка системы, согласующаяся с правилами системы). То есть формальная система является семантически полной, если:

$\models _{\mathcal {S}}\varphi \ \to \ \vdash _{\mathcal {S}}\varphi .$

Например, теорема Гёделя о полноте устанавливает семантическую полноту логики первого порядка .

Сильная полнота

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

$\Gamma \models _{\mathcal {S}}\varphi \ \to \ \Gamma \vdash _{\mathcal {S}}\varphi .$

Опровержение-полнота

Формальная система S является полной по опровержению, если она способна вывести ложное из любого невыполнимого набора формул. То есть:

$\Gamma \models _{\mathcal {S}}\bot \to \ \Gamma \vdash _{\mathcal {S}}\bot .$

Любая сильно полная система полна и по опровержению. Интуитивно, сильная полнота означает, что для данного набора формул $\Gamma$, можно вычислить каждое семантическое последствие $\varphi$ из $\Gamma$, а полнота опровержения означает, что для данного набора формул $\Gamma$ и формула $\varphi$, можно проверить , $\varphi$ является семантическим следствием $\Gamma$.

Примеры систем с полным опровержением включают в себя: резолюцию SLD на предложениях Хорна , суперпозицию на эквациональной клаузальной логике первого порядка, резолюцию Робинсона на множествах предложений. Последний не является строго полным: например $\{a\}\models a\lor b$ справедливо даже в пропозициональном подмножестве логики первого порядка, но $a\lor b$ не может быть получено из $\{a\}$по резолюции. Однако, $\{a,\lnot (a\lor b)\}\vdash \bot$ можно вывести.

Синтаксическая полнота

Формальная система S является синтаксически полной , или дедуктивно полной , или максимально полной , если для каждого предложения (замкнутой формулы) φ языка системы либо φ, либо ¬φ является теоремой S . Это также называется полнотой отрицания и является более сильным, чем семантическая полнота. В другом смысле формальная система является синтаксически полной тогда и только тогда, когда к ней нельзя добавить ни одно недоказуемое предложение без внесения противоречия . Истинно-функциональная логика высказываний и логика предикатов первого порядка семантически полны, но не синтаксически полны (например, утверждение пропозициональной логики, состоящее из одной пропозициональной переменной A , не является теоремой, как и ее отрицание). Теорема Гёделя о неполноте показывает, что любая вычислимая достаточно мощная система, такая как арифметика Пеано , не может быть одновременно непротиворечивой и синтаксически полной.

Структурная

Основная статья: Допустимое правило

В суперинтуиционистской и модальной логике логика является структурно полной , если каждое допустимое правило выводимо.

Полнота модели

Основная статья: Полная теория модели

Теория является модельно полной тогда и только тогда, когда каждое вложение ее модели является элементарным вложением .