Повнота (логіка)
 | Ця стаття є сирим перекладом з іншої мови. Можливо, вона створена за допомогою машинного перекладу або перекладачем, який недостатньо володіє обома мовами. (січень 2018) |
Повнота (або неповнота) у математичній логіці та металогіці — характеристика формальної системи. Систему називають повною стосовно деякої властивості, якщо кожна формула системи з даною властивістю може бути доведена за допомогою цієї системи (тобто є однією з теорем системи). У протилежному випадку система називається неповною. Поняття повноти також використовується у інших значеннях, що можуть залежати від контексту, найчастіше стосовно семантичної валідності. З інтуїтивної точки зору, система є повною , якщо в її межах можна вивести кожну формулу, яка є істинною. Докази повноти було опубліковано в різні роки Куртом Геделем, Леоном Генкіном і Емілем Леоном Постом (див. історію тези Черча–Тюрінга).
Характеристика системи, обернена до повноти, називається правильність (soundness), або конзистентність: система є правильною стосовно деякої властивості (головним чином, семантичної чинності) тоді і тільки тоді, коли кожна з теорем системи має дану властивість.
Формальна мова - це виразно повна, якщо вона може висловити предмет, для якого вона призначена.
Основна стаття: Функціональна повнота
Набір логічних зв'язків, які пов'язані з формальною системою, є функціонально повними, якщо вони можуть висловити всю пропозиційну функцію.
Смислова завершеність є протилежною стійкістю для формальних систем. Формальна система є повною щодо «семантично повній», коли всі її тавтології є теоремами, тоді як формальна система є «звук», коли всі теореми тавтології (тобто, вони є семантично допустимі до формул: формули, справжні при будь-якій інтерпретації мовної системи, що узгоджується з правилами системи). Тобто,
⊨ S φ → ⊢ S φ.[1]
Наприклад, теорема про повноту Геделя визначає смислову завершеність в логіці першого порядку.
Формальна система S настійно повна або повна в сильному сенсі, якщо для будь-якого набору Γ приміщення, будь-яку формулу, яка семантично випливає з Γ похідне від Γ. Тобто
Γ ⊨ S φ → Γ ⊢ S φ .
Формальна система S є спростування-повною, якщо вона здатна вивести хибу з кожного набору формул, які ніколи не виконуються. Тобто,
Γ ⊨ S ⊥ → Γ ⊢ S ⊥ .[2]
Кожна настійно повна система теж спростування-повній. Інтуїтивно, сильна повнота означає, що, враховуючись формулою, наведеною Γ , можна обчислити всі семантичні наслідки φ на Γ , а спростування-повнота означає, що, враховуючи формулу набору Γ мені , можливо, щоб перевірити, чи φ є семантичний наслідок Γ. Приклади спростування-комплексної системи включають в себе: ВЛВ-резолюцію на Диз'юнкті Горна, накладенням на підрядне эквациональной логіки першого порядку, правило резолюції на пропозицію наборів.[3] останній не сильно повний: наприклад, { a } ⊨ a ∨ b тримає навіть у пропозиційну підмножину першого порядку логіки, але a ∨ b не може бути похідним від { a } резолюції. Однак, { a , ¬ ( a ∨ b ) } ⊢ ⊥ може бути похідним.
Формальна система S є синтаксично повною або дедуктивно повною або максимально повною, якщо за кожне речення (замкнену формула) φ мови системи або φ, або φ теорема С. Це також називається запереченням повноти, і сильніше, ніж смислова завершеність. В іншому сенсі, формальна система є синтаксично повною, якщо тільки немає недоказуємої пропозиції, то можуть бути додані без внесення невідповідністі. Числення висловлень і логіка першого порядку семантичні, але не синтаксично повні (наприклад, вислів пропозиційної логіки, що складається з однієї змінної висловлювання, а не теореми, як і його заперечення). Теорема Геделя про неповноту показує, що будь-яка рекурсивна система, як досить потужних, таких як арифметика Пеано, не може бути одночасно несуперечливою і синтаксично повною.
Основна стаття: допустиме правило[en]
У суперінтуіционістських і модальних логік, логіка є структурно повною, якщо кожне допустиме правило є виведеним.
- ↑ Hunter, Geoffrey, Metalogic: An Introduction to the Metatheory of Standard First-Order Logic, University of California Pres, 1971м
- ↑ David A. Duffy (1991). Principles of Automated Theorem Proving. Wiley. Here: sect. 2.2.3.1, p.33
- ↑ Stuart J. Russell, Peter Norvig (1995). Artificial Intelligence: A Modern Approach. Prentice Hall. Here: sect. 9.7, p.286
- Повнота у логіці // Філософський енциклопедичний словник / В. І. Шинкарук (гол. редкол.) та ін. — Київ : Інститут філософії імені Григорія Сковороди НАН України : Абрис, 2002. — С. 491. — 742 с. — 1000 екз. — ББК 87я2. — ISBN 966-531-128-X.