Рівносильні перетворення формул

Означення 13.1. Дві формули F і H логіки предикаті називаються рівносильними на множині М, якщо при будь-якій підстановці в ці формули замість предикатних змінних довільних конкретних предикатів, визначених на М, формули перетворюються в рівносильні предикати. Якщо дві формули рівносильні на довільних множинах, то їх називають просто рівносильними. Рівносильність формул позначається так: F @ H.

Наведемо приклад двох нерівносильних формул. Покажемо, що . Дійсно, підставимо замість предикатних змінних Р(х) і Q(x) конкретні предикати А(х) і В(х), визначені на множині N, де А(х) є ” х - парне”, а В(х) є ” х - непарне”. Тоді ліва формула перетвориться в висловлення (нульмісний предикат) “кожне натуральне число або парне, або непарне”, яке істинне. Права формула перетворюється в висловлення (нульмісный предикат) “або кожне натуральне число парне, або кожне натуральне число непарне”, яке хибне.

Зрозуміло, що формули F і H рівносильні тоді й тільки тоді, коли формула F↔H є тавтологією: ╞ .

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

Означення 13.2. Зведеною формою для формули логіки предикатів називається така рівносильна їй формула, в якій із логічних операцій алгебри висловлень є лише операції Ø, Ù, Ú, причому знак заперечення відноситься лише до предикатних змінних і висловлень.

Теорема 13.1. Для кожної формули логіки предикатів існує рівносильна їй зведена формула.

Дана теорема доводиться методом математичної індукції за числом логічних зв’язок у формулі (включаючи квантори загальності й існування).

Означення 13.3. Пренексною нормальною формою формули логіки предикатів називається така її зведена форма, в якій всі квантори стоять на її початку, а область дії кожного з них поширюється до кінця формули, тобто це формула вигляду де К_i -один із кванторів або (i=1,..., n), т≤п, причому формула F не містить кванторів і є зведеною формулою. Зазначимо, що квантори в формулі взагалі можуть бути відсутніми.

Теорема 13.2. Для кожної формули логіки предикатів існує пренексна нормальна форма.