В математической логике и металогике формальная система называется полной относительно определенного свойства, если каждая формула , обладающая этим свойством, может быть выведена с использованием этой системы, т. е. является одной из ее теорем ; в противном случае система называется неполной . Термин «полная» также используется без уточнения, с различными значениями в зависимости от контекста, в основном относящимися к свойству семантической валидности . Интуитивно система называется полной в этом конкретном смысле, если она может вывести каждую формулу, которая является истинной.
Свойство, обратное полноте, называется обоснованностью : система обоснована относительно некоторого свойства (в основном семантической обоснованности), если каждая из ее теорем обладает этим свойством.
Формальный язык является выразительно полным , если он может выразить предмет, для которого он предназначен.
Набор логических связок , связанных с формальной системой, является функционально полным , если он может выразить все пропозициональные функции .
Семантическая полнота — это противоположность обоснованности для формальных систем. Формальная система является полной относительно тавтологичности или «семантически полной», когда все ее тавтологии являются теоремами , тогда как формальная система является «обоснованной», когда все теоремы являются тавтологиями (то есть они являются семантически допустимыми формулами: формулами, которые истинны при любой интерпретации языка системы, которая согласуется с правилами системы). То есть формальная система является семантически полной, если:
Например, теорема Гёделя о полноте устанавливает семантическую полноту для логики первого порядка .
Формальная система S является строго полной или полной в сильном смысле , если для каждого набора посылок Γ любая формула, которая семантически следует из Γ, выводима из Γ. То есть:
Формальная система S является опровержение-полной, если она способна вывести ложь из любого невыполнимого набора формул. То есть:
Каждая сильно полная система также является полной по опровержению. Интуитивно, сильная полнота означает, что при заданном наборе формул можно вычислить каждое семантическое следствие , в то время как полнота опровержения означает, что при заданном наборе формул и формуле можно проверить , является ли семантическим следствием .
Примерами систем, полных опровержения, являются: разрешение SLD на хорновских предложениях , суперпозиция на эквациональной клаузальной логике первого порядка, разрешение Робинсона на множествах предложений. [3] Последнее не является строго полным: например, выполняется даже в пропозициональном подмножестве логики первого порядка, но не может быть выведено из него с помощью разрешения. Однако может быть выведено.
Формальная система S является синтаксически полной или дедуктивно полной или максимально полной , если для каждого предложения (закрытой формулы) φ языка системы либо φ, либо ¬φ является теоремой S. Это также называется полнотой отрицания и сильнее семантической полноты. В другом смысле формальная система является синтаксически полной тогда и только тогда, когда к ней нельзя добавить ни одного недоказуемого предложения, не внося несоответствия . Истинностно -функциональная пропозициональная логика и логика предикатов первого порядка являются семантически полными, но не синтаксически полными (например, утверждение пропозициональной логики, состоящее из одной пропозициональной переменной A , не является теоремой, как и ее отрицание). Теорема Гёделя о неполноте показывает, что любая вычислимая система, которая является достаточно мощной, такая как арифметика Пеано , не может быть одновременно непротиворечивой и синтаксически полной.
В суперинтуиционистской и модальной логиках логика структурно полна, если каждое допустимое правило выводимо.
Теория является модельно полной тогда и только тогда, когда каждое вложение ее моделей является элементарным вложением .
