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

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

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

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

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

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

${\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 \Гамма}$${\displaystyle \varphi}$${\displaystyle \Гамма}$${\displaystyle \Гамма}$${\displaystyle \varphi}$${\displaystyle \varphi}$${\displaystyle \Гамма}$

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

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

Синтаксическая полнота может также относиться к другому не связанному понятию, также называемому полнотой Поста или полнотой Гильберта-Поста . В этом смысле формальная система является синтаксически полной тогда и только тогда, когда к ней нельзя добавить недоказуемое предложение, не внося несоответствия . Истинностно-функциональная пропозициональная логика и логика предикатов первого порядка являются семантически полными, но не синтаксически полными (например, утверждение пропозициональной логики, состоящее из единственной пропозициональной переменной A , не является теоремой, как и ее отрицание). ^{[ необходима цитата ]}

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

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