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

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

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

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

Формы полноты [ править ]

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

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

Функциональная полнота [ править ]

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

Семантическая полнота [ править ]

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

${\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 . Это также называется полнотой отрицания и сильнее семантической полноты. С другой стороны, формальная система синтаксически завершена тогда и только тогда, когда к ней нельзя добавить недоказуемое предложение без внесения несогласованности. Истинно-функциональная логика высказываний и логика предикатов первого порядкаявляются семантически полными, но не синтаксически полными (например, утверждение логики высказываний, состоящее из единственной пропозициональной переменной A , не является теоремой, равно как и ее отрицание). Теорема Гёделя о неполноте показывает, что любая достаточно мощная рекурсивная система, такая как арифметика Пеано , не может быть одновременно непротиворечивой и синтаксически полной.

Структурная завершенность [ править ]

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

Ссылки [ править ]