28. Алетичні модальні логіки. Системи t, b, s4, s5.

Основними модальними операторами алетичної (загальної) модальної логіки є оператори  – "необхідно" та  – "можливо". Вони пов'язані таким чином: Р = Р та Р = Р.

в системі S5 кожна суперпозиція модальностей еквівалентна модальності без суперпозицій. Це означає, що для предиката Р маємо 6 таких різних предикатів: Р, Р, Р, Р, Р, Р.

У системі S4 існує 14 різних модальностей: Р, Р, Р, Р, Р, Р, Р та 7 дуальних модальностей, коли замість Р беремо Р. Алфавіт мови складається з множини Ps предикатних символiв, символів пропозиційних композицій ,  та символу  модальної композиції (модального оператора) "необхідно".

Множина формул Fm визначається індуктивно: 1) Кожний PPs є формулою. Такi формули атомарні.2) Нехай  та  – формули. Тодi ,   – формули.

Символ  трактується як скорочення для 

Система Т. Множина аксіом складається з аксіом системи К та аксіом, що задаються схемою

Ах) . Правила виведення ті самі, що й для системи К.

Система B (брауерівська). Множина аксіом складається з аксіом системи T та аксіом, що задаються схемою

АхВ)  Правила виведення ті самі, що й для системи К.

Система S4. Множина аксіом складається з аксіом системи T та аксіом, що задаються схемою

АхS4)  Правила виведення ті самі, що й для системи К.

Система S5. Множина аксіом складається з аксіом системи T та аксіом, що задаються схемою

АхS5) . Правила виведення ті самі, що й для системи К.

Той факт, що формула  є теоремою систем К, Т, В, S4, S5, відповідно _K, _T, _B, _S4, _S5.

Моделлю можливих світів, або реляційною моделлю, назвемо трійку М = (S, , I).

Тут S – множина світів,  – бінарне відношення на S, I – відображення I : Ps  S{T, F} інтерпретації атомарних формул на світах.

28. Темпоральні логіки. Синтаксис мови, реляційна семантика.

. Основними модальностями часової, або темпоральної логіки, є модальності "завжди було", "колись було", "завжди буде", "колись буде". введемо такі модальні композиції (модальні оператори) темпоральної логіки: ¨_­ (завжди буде), ¨_¯ (завжди було), ²_­ (колись буде) та ²_¯ (колись було). Для темпоральних модальних систем можна вважати базовими оператори ¨_­ та ¨_¯. Тоді оператори ²_­ та ²_¯ є похідними часовими операторами, ці оператори визначатимуться так:

²_­Р означає ب_­ØР,

²_¯Р означає ب_¯ØР.

Алфавіт мови складається з множини _Ps предикатних символiв, символів пропозиційних композицій Ø, Ú та символів ¨_­, ¨_¯ відповідних часових операторів.

Множина формул Fm визначається індуктивно: 1) Кожний PÎPs є формулою. Такi формули атомарні.2) Нехай  та  – формули. Тодi ,  ¨_­ ¨_¯ – формули. Символи ²_­ та ²_¯ – це скорочення для¨_­ та ¨_¯_. . Аксіомами системи К_t є аксіоми пропозиційної логіки і аксіоми, що задаються такими схемами:

АхNr_­) ¨_­(Y®¨_­®¨_­Y

АхNr_¯) ¨_¯(Y®¨_¯®¨_¯Y

АхТ_­) ¨_­²_¯ 

АхТ_¯) ¨_¯²_­ 

28. Епістемічні логіки. Логіка знання з n експертами. Деотичні логіки.

Розділ модальної логіки, в якому досліджуються міркування з такими модальностями, як "відомо", "вірно", "доведено", "спростовано", називавється епістемічною логікою.

Основними модальностями епістемічної логіки є К та В, які відповідають знанню та опінії, вірі.

КQ можна трактувати так: "відомо, що Q".

ВQ можна трактувати так: "вірую, що Q".

Алфавіт мови пропозиційної епістемічної логіки з одним експертом складається з множини Ps предикатних символiв, символів пропозиційних композицій Ø, Ú та символу К модального оператора знання.

Множина формул Fе визначається індуктивно: 1) Кожний PÎPs є формулою. Такi формули атомарні.2) Нехай  та  – формули. Тодi ,  К – формули.

Розділ модальної логіки, в якому вивчаються міркування з термінами "обов'язково", "дозволено", "заборонено", називається деонтичною логікою. Предметом такої логіки є нормативні міркування.

В мінімальному (стандартному) варіанті деонтичної логіки маємо базовий деонтичний оператор О – "обов'язково". Похідні деонтичні оператори визначаються так (тут Q – предикат):

1) Оператор Р – "дозволено": РQ означає ØОØQ ;

2) Оператор F – "заборонено": FQ означає ОØQ ;

3) Оператор I – "байдуже": IQ означає РQ & PØQ .

Такі аксіоми задаються схемами:

АхDNr) О(Y®О®ОY

АхD¨) OР.

Правило виведення ПО має вигляд

ПО) О