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