Полнота (логика) - Completeness (logic)

Не путать с Полный (сложность).

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

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

Основные статьи: Разумность и Последовательность

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

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

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

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

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

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

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

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

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

${\displaystyle \models _{\mathcal {S}}\varphi \ \to \ \vdash _{\mathcal {S}}\varphi .}$^[1]

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

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

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

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

Полнота опровержения

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

${\displaystyle \Gamma \models _{\mathcal {S}}\bot \to \ \Gamma \vdash _{\mathcal {S}}\bot .}$^[2]

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

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

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

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

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

Основная статья: допустимая норма

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

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

1. Хантер, Джеффри, Metalogic: Введение в метатеорию стандартной логики первого порядка, Калифорнийский университет Pres, 1971
2. Дэвид А. Даффи (1991). Принципы автоматизированного доказательства теорем. Вайли. Здесь: разд. 2.2.3.1, стр.33
3. Стюарт Дж. Рассел, Питер Норвиг (1995). Искусственный интеллект: современный подход. Прентис Холл. Здесь: разд. 9.7, стр.286