RomaNemkovych
Категоричність аксіоматичних теорій та їх повнота ред.
Словник скорочень ред.
ФАТ- формальна аксіоматична теорія
ч/в - числення висловлень
Властивості формальних систем ред.
Властивості формальних систем
- · Несуперечність
Теорія, в якій множина теорем покриває всі множини формул (всі формули є теоремами, «істинними висловлюваннями»), називається суперечливою. В іншому випадку теорія називається несуперечливою. З'ясування суперечливості теорії - одна з найважливіших і іноді найскладніших завдань формальної логіки. Після з'ясування суперечливості теорія, як правило, не має подальшого ні теоретичного, ні практичного застосування.
- · Повнота
Теорія називається повною, якщо в ній для будь-якої формули виводиться або сама або її заперечення. В іншому випадку, теорія містить недоведені твердження (твердження, які не можна ні довести, ні спростувати засобами самої теорії), і називається неповною.
Формальна аксіоматична теорія числення виловлень є повною відносно своєї моделі алгебри висловлень.
- · Незалежність аксіом
Окрема аксіоматична теорії вважається незалежною, якщо цю аксіому не можна вивести з інших аксіом. Залежна аксіома по суті надмірна, і її видалення з системи аксіом ніяк не відіб'ється на теорії. Вся система аксіом теорії називається незалежна, якщо кожна аксіома в ній незалежна.
- · Розв'язність
Теорія називається вирішуваною, якщо в ній поняття теореми ефективно, тобто існує ефективний процес (алгоритм), що дозволяє для будь-якої формули за злічене число кроків визначити, є вона теоремою чи ні.
Категоричність ФАТ ред.
Перед тим як давити означення категоричності аксіоматичної теорії потрібно дати означення проблеми несуперечності аксіоматичної теорії.
Несуперечність аксіоматичної теорії є однією з основних вимог, що пропоновані до системи аксіом певної теорії. Вона означає, що з даної системи
аксіом не можна логічним шляхом вивести два суперечливих один одному твердження.
З'ясування суперечливості теорії - одна з найважливіших і іноді найскладніших завдань формальної логіки. Після з'ясування суперечливості теорія, як правило, не має подальшого ні теоретичного, ні практичного застосування.
Формальну аксіоматичну теорію числення висловлень називають категоричною, якщо будь-які її дві моделі ізоморфні між собою, тобто між ними можна встановити взаємно однозначне відображеня.
Повнота ФАТ ред.
Проблема повноти формальної системи полягає в тому, що система аксіом припускає лише одну реалізацію виводу теореми.
Також розрізнюють повноту у широкому та вузькому розумінні.
Формальна аксіоматична теорія числення висловлень називають повною у вузькому розумінні якщо приєднання до системи аксіоми цієї теорії хоча б однієї формули веде дотого що вона не є теоремою.
Формальну аксіоматичну теорію називають повною у широкому розумінні або повною відносно своєї моделі якщо будь яку формула істинна в моделі є теоремою цієї моделі або якщо будь яку тотожно істинну формулу можна довести. Тоді або А, або ¬А є істинним і має виводитись у формальній теорії, тобто довільна формула А теорії або її заперечення А є теоремами формальної теорії.
Формальна аксіоматична теорія числення висловлень є повною відносно своєї моделі алгебри висловлень.
Числення висловлень – це формальна аксіоматична теорія повна у вузькому розумінні.