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

Не путать с 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 , не является теоремой, как и ее отрицание). Теорема Гёделя о неполноте показывает, что любая вычислимая достаточно мощная система, такая как арифметика Пеано , не может быть одновременно непротиворечивой и синтаксически полной.

Структурная завершенность

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

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

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

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

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