Основні поняття та визначення

Числення предикатів

В даному курсі лекцій опис формальної теорії числення предикатів носить конспективний характер, зокрема, багато складні докази опущені. У той же час, основна увага приділена прагматичним аспектам теорії, які можуть принести велику користь інженеру-програмісту. Нагадаємо ще раз найбільш важливі аспекти обчислення предикатів.

Предикат - оповідної пропозицію, що містить предметні змінні, визначені на відповідних множинах. При заміні змінних конкретними значеннями (елементами) цих множин пропозицію звертається в висловлювання, тобто приймає значення "істинно" або "хибно". Позначення предиката, що містить п змінних (n-місного предиката): Р (х _1, х _2,..., х _n), при цьому передбачається, що х ₁ Î М _1, х ₂ Î М _2,..., х _n Î М _n.

За допомогою логічних зв'язок (і дужок) предикати можуть об'єднуватися в різноманітні логічні формули - предикатні формули. Дослідження предикатних формул і способів встановлення їх істинності є основним предметом логіки предикатів. Логіка предикатів разом з вхідною в неї логікою висловлень є основою логічного мови математики. З її допомогою вдається формалізувати і точно дослідити основні методи побудови математичних теорій. Логіка предикатів є важливим засобом побудови розвинених логічних мов і формальних систем (формальних теорій).

Логіка предикатів, як і логіка висловлювань, може бути побудована у вигляді алгебри логіки предикатів і числення предикатів. Тут, як і у випадку логіки висловлювань, для знайомства з основними поняттями логіки предикатів скористаємося мовою алгебри, а не числень. Такий вибір обумовлений рядом причин:

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

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

n - місцевий предикат - це функція Р (х _1, х _2,..., х _n) від п змінних, що приймають значення з деяких заданих предметних областей, так що х ₁ Î М _1, х ₂ Î М _2,., х _n Î М _n, а функція Р приймає два логічних значення - "істинно" або "хибно" (позначення: {І, Л}, {1, 0}). Таким чином, предикат Р (х _1, х _2,..., х _n) є функцією типу Р: М ₁ x М ₂ x ... x М _n? B, де безлічі М _1, М _2,..., М _n називаються предметними областями предиката; х _1, х _2,..., х _n - предметними змінними предиката; В - двійкове (бінарне) безліч: В = {І, Л} або {1,0}. Якщо предикатні змінні приймають значення на одному безлічі, то Р: М ^n? В.

Відповідності між предикатами, відносинами і функціями:

1. Для будь-яких М і п існує взаємно однозначна відповідність між n-місцевими відносинами і п - місцевими предикатами Р (х _1, х _2,..., х _n), Р: М ^n? В:

- кожному n - місцевому відношенню R відповідає предикат Р (х _1, х _2,..., х _n) такий, що Р (a _1, a _2,..., a _n) = 1, якщо і тільки якщо (a _1, a _2,..., a _n) Î R;

- всякий предикат Р (х _1, х _2,..., х _n) визначає відношення R таке, що (a _1, a _2,..., a _n) Î R, якщо і тільки якщо Р (a _1, a х _2,..., a _n) = 1.

При цьому R задає область істинності предиката Р.

2. Усякої функції f (х _1, х _2,..., х _n), f: М ⁿ? М, відповідає предикат Р (х _1, х _2,..., х _n, х _{n +1),} Р: М ^{n +1?} В, такий, що Р (a _1, a _2,..., a _n, a _{n +1}) = 1, якщо і тільки якщо f (a _1, a х _2,..., a _n) = a _{n +1.}

Поняття предиката ширше поняття функції, тому зворотне відповідність (від (n +1) - місцевого предиката до n - місцевої функції) можливо не завжди, а тільки для таких предикатів Р ' для яких виконується умова, пов'язане з вимогою однозначності функції.

Дата добавления: 2014-11-08