Категоричність аксіоматичних теорій та їх повнота

Словник скорочень

ФАТ- формальна аксіоматична теорія

ч/в - числення висловлень

Властивості формальних систем

· Несуперечність

Теорія, в якій множина теорем покриває всі множини формул (всі формули є теоремами, «істинними висловлюваннями»), називається суперечливою. В іншому випадку теорія називається несуперечливою. З'ясування суперечливості теорії - одна з найважливіших і іноді найскладніших завдань формальної логіки. Після з'ясування суперечливості теорія, як правило, не має подальшого ні теоретичного, ні практичного застосування.

· Повнота

Теорія називається повною, якщо в ній для будь-якої формули виводиться або сама або її заперечення. В іншому випадку, теорія містить недоведені твердження (твердження, які не можна ні довести, ні спростувати засобами самої теорії), і називається неповною.

Формальна аксіоматична теорія числення виловлень є повною відносно своєї моделі алгебри висловлень.

· Незалежність аксіом

Окрема аксіоматична теорії вважається незалежною, якщо цю аксіому не можна вивести з інших аксіом. Залежна аксіома по суті надмірна, і її видалення з системи аксіом ніяк не відіб'ється на теорії. Вся система аксіом теорії називається незалежна, якщо кожна аксіома в ній незалежна.

· Розв'язність

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

Категоричність ФАТ

Перед тим як давити означення категоричності аксіоматичної теорії потрібно дати означення проблеми несуперечності аксіоматичної теорії.

Несуперечність аксіоматичної теорії є однією з основних вимог, що пропоновані до системи аксіом певної теорії. Вона означає, що з даної системи

аксіом не можна логічним шляхом вивести два суперечливих один одному твердження.

З'ясування суперечливості теорії - одна з найважливіших і іноді найскладніших завдань формальної логіки. Після з'ясування суперечливості теорія, як правило, не має подальшого ні теоретичного, ні практичного застосування.

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

Повнота ФАТ

Проблема повноти формальної системи полягає в тому, що система аксіом припускає лише одну реалізацію виводу теореми.

Також розрізнюють повноту у широкому та вузькому розумінні.

Формальна аксіоматична теорія числення висловлень називають повною у вузькому розумінні якщо приєднання до системи аксіоми цієї теорії хоча б однієї формули веде дотого що вона не є теоремою.

Формальну аксіоматичну теорію називають повною у широкому розумінні або повною відносно своєї моделі якщо будь яку формула істинна в моделі є теоремою цієї моделі або якщо будь яку тотожно істинну формулу можна довести. Тоді або А, або ¬А є істинним і має виводитись у формальній теорії, тобто довільна формула А теорії або її заперечення А є теоремами формальної теорії.

Формальна аксіоматична теорія числення висловлень є повною відносно своєї моделі алгебри висловлень.

Числення висловлень – це формальна аксіоматична теорія повна у вузькому розумінні.