Повнота (логіка)

Повнота (або неповнота) у математичній логіці та металогіці — характеристика формальної системи. Систему називають повною стосовно деякої властивості, якщо кожна формула системи з даною властивістю може бути доведена за допомогою цієї системи (тобто є однією з теорем системи). У протилежному випадку система називається неповною. Поняття повноти також використовується у інших значеннях, що можуть залежати від контексту, найчастіше стосовно семантичної валідності. З інтуїтивної точки зору, система є повною , якщо в її межах можна вивести кожну формулу, яка є істинною. Докази повноти було опубліковано в різні роки Куртом Геделем, Леоном Генкіном і Емілем Леоном Постом (див. історію тези Черча–Тюрінга).

Інші властивості, пов'язані з повнотою

Характеристика системи, обернена до повноти, називається правильність (soundness), або конзистентність: система є правильною стосовно деякої властивості (головним чином, семантичної чинності) тоді і тільки тоді, коли кожна з теорем системи має дану властивість.

Форми повноти

Виразні повноти

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

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

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

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

Смислова завершеність

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

       ⊨ S φ   →   ⊢ S φ.[1]

Наприклад, теорема про повноту Геделя визначає смислову завершеність в логіці першого порядку.

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

Формальна система S настійно повна або повна в сильному сенсі, якщо для будь-якого набору Γ приміщення, будь-яку формулу, яка семантично випливає з Γ похідне від Γ. Тобто

       Γ ⊨ S φ   →   Γ ⊢ S φ .

Спростування повноти

Формальна система S є спростування-повною, якщо вона здатна вивести хибу з кожного набору формул, які ніколи не виконуються. Тобто,

      Γ ⊨ S ⊥ →   Γ ⊢ S ⊥ .[2]

Кожна настійно повна система теж спростування-повній. Інтуїтивно, сильна повнота означає, що, враховуючись формулою, наведеною Γ , можна обчислити всі семантичні наслідки φ на Γ , а спростування-повнота означає, що, враховуючи формулу набору Γ мені , можливо, щоб перевірити, чи φ є семантичний наслідок Γ. Приклади спростування-комплексної системи включають в себе: ВЛВ-резолюцію на Диз'юнкті Горна, накладенням на підрядне эквациональной логіки першого порядку, правило резолюції на пропозицію наборів.[3] останній не сильно повний: наприклад, { a } ⊨ a ∨ b тримає навіть у пропозиційну підмножину першого порядку логіки, але a ∨ b не може бути похідним від { a } резолюції. Однак, { a , ¬ ( a ∨ b ) } ⊢ ⊥ може бути похідним.

Синтаксична завершеність

Формальна система S є синтаксично повною або дедуктивно повною або максимально повною, якщо за кожне речення (замкнену формула) φ мови системи або φ, або φ теорема С. Це також називається запереченням повноти, і сильніше, ніж смислова завершеність. В іншому сенсі, формальна система є синтаксично повною, якщо тільки немає недоказуємої пропозиції, то можуть бути додані без внесення невідповідністі. Числення висловлень і логіка першого порядку семантичні, але не синтаксично повні (наприклад, вислів пропозиційної логіки, що складається з однієї змінної висловлювання, а не теореми, як і його заперечення). Теорема Геделя про неповноту показує, що будь-яка рекурсивна система, як досить потужних, таких як арифметика Пеано, не може бути одночасно несуперечливою і синтаксично повною.

Структурна повнота

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

У суперінтуіционістських і модальних логік, логіка є структурно повною, якщо кожне допустиме правило є виведеним.

Примітки
  1. Hunter, Geoffrey, Metalogic: An Introduction to the Metatheory of Standard First-Order Logic, University of California Pres, 1971м
  2. David A. Duffy (1991). Principles of Automated Theorem Proving. Wiley. Here: sect. 2.2.3.1, p.33
  3. Stuart J. Russell, Peter Norvig (1995). Artificial Intelligence: A Modern Approach. Prentice Hall. Here: sect. 9.7, p.286

Література
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.