11.6: Модальні логіки

Last updated
Save as PDF

Page ID: 52814

\( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \) \( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)\(\newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\) \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\) \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\) \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\) \( \newcommand{\Span}{\mathrm{span}}\) \(\newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\) \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\) \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\) \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\) \( \newcommand{\Span}{\mathrm{span}}\)

Template:MathJaxZach

Розглянемо наступний приклад умовного речення:

Якщо Джеремі один в тій кімнаті, то він п'яний і голий і танцює на стільцях.

Це приклад умовного твердження, яке може бути матеріально істинним, але тим не менш вводить в оману, оскільки здається, що існує більш міцний зв'язок між попереднім і висновком, крім просто того, що або попередник є помилковим, або наслідком істинним. Тобто формулювання говорить про те, що претензія вірна не тільки в цьому конкретному світі (де це може бути тривіально правдою, тому що Джеремі не один у кімнаті), але й про те, що, крім того, висновок був би правдивим, якби попередник був правдою. Іншими словами, можна вважати, що твердження означає, що претензія вірна не тільки в цьому світі, але і в будь-якому «можливому» світі; або що це обов'язково вірно, на відміну від просто істинного в цьому конкретному світі.

Модальна логіка була розроблена, щоб зрозуміти такий вид необхідності. Один отримує модальну логіку пропозиції від звичайної логіки пропозиції шляхом додавання оператора коробки; тобто, якщо\(A\) є формулою, так і є\(\Box A\). Інтуїтивно\(\Box A\) стверджує,\(A\) що обов'язково вірно, або вірно в будь-якому можливому світі. \(\Diamond A\)зазвичай вважається абревіатурою для\(\lnot \Box \lnot A\), і може бути прочитана як стверджуючи, що\(A\) це, можливо, вірно. Звичайно, модальність також може бути додана до логіки предикатів.

Структури Кріпке можуть бути використані для надання семантики модальної логіки; насправді Кріпке вперше розробив цю семантику з урахуванням модальної логіки. Замість того, щоб обмежувати часткові порядки, загалом один має набір «можливих світів»\(P\), і бінарний зв'язок «доступності»\(\Atom{R}{x,y}\) між світами. Інтуїтивно\(\Atom{R}{p,q}\) стверджує, що світ\(q\) сумісний з\(p\); тобто, якщо ми «в» світі\(p\), ми повинні розважити можливість того, що світ міг би бути таким\(q\).

Модальну логіку іноді називають «інтенсивна» логіка, на відміну від «extensional». Призначена семантика для розширеної логіки, як класична логіка, стосуватиметься лише одного світу, «фактичного»; тоді як семантика для «інтенсивної» логіки спирається на більш досконалу онтологію. Окрім необхідності структурування, можна використовувати модальність для структурування інших мовних конструкцій, переосмислення\(\Box\) та\(\Diamond\) відповідно до програми. Наприклад:

У логіці\(\Box A\) доказовості читається «\(A\)є доказовим» і\(\Diamond A\)\(A\) читається «послідовно».
У епістемічній логіці можна прочитати\(\Box A\) як «Я знаю\(A\)» або «Я вірю»\(A\).
У тимчасовій логіці можна читати\(\Box A\) як «\(A\)завжди вірно» і\(\Diamond A\) як «\(A\)іноді вірно».

Хотілося б доповнити логіку правилами та аксіомами, що стосуються модальності. Наприклад, система\(\Log{S4}\) складається зі звичайних аксіом і правил пропозіційної логіки разом з наступними аксіомами:

\ [\ begin {вирівняний}
&\ Box (A\ lif B)\ lif (\ Box A\ lif\ Box B)\\
&\ Box A\ lif A\\
&\ Box A\ lif\ Box\ Box A\ end {вирівняний}\]

а також, як правило, «з\(A\) висновку»\(\Box A\). \(\Log{S5}\)додає наступну аксіому:

\[\Diamond A \lif \Box \Diamond A\nonumber\]

Варіації цих аксіом можуть бути придатними для різних застосувань; наприклад, S5 зазвичай приймається для характеристики поняття логічної необхідності. І приємно те, що зазвичай можна знайти семантику, для якої система доказування є надійною і повною, обмежуючи відношення доступності в структурах Кріпке природним чином. Наприклад,\(\Log{S4}\) відповідає класу структур Кріпке, в яких відношення доступності є рефлексивним і перехідним. \(\Log{S5}\)відповідає класу кріпкевських структур, в яких відношення доступності є універсальним, тобто, що кожен світ доступний з будь-якого іншого; так\(\Box A\) тримається тоді і тільки тоді, коли він\(A\) тримається в кожному світі.