Как оценить (присвоить значения истинности) формуле в модальной логике (модель Крипке)

Полный новичок здесь, и раздражен на этом. Я могу перевести утверждения естественного языка в формулы модальной логики, но их оценка в модели Крипке кажется неуловимой, поскольку я просто не знаю, как применить теорию на практике.

Может ли кто-нибудь быть любезным объяснить мне шаг за шагом , как использовать формулу (p & q -> (p -> q)) -> [] (p -> q) , чтобы присвоить значения истинности каждой переменной в каждом мире в модели Крипке?

Спасибо

Ответы (1)

Модели Крипке можно использовать для доказательства того, что формула недействительна .

Пересматривая ваш пример, это означает показать, что антецедент: (p & q → (p → q)) истинен в w («актуальном» мире), а консеквент r □(p → q) нет, т . е. (p → q) ложно в некотором мире w', доступном из w (т.е. таком, что wRw' ).

Если q ложно в w (записано: w ⊮ q ), мы имеем, что p & q ложно в w , и, следовательно, (p & q → (p → q)) истинно.

И если p истинно, мы имеем, что (p → q) ложно в w .

Если отношение «доступности» R рефлексивно , то есть wRw , мы имеем, что (p → q) не истинно в каждом w' таком, что wRw' , и это означает, что □(p → q) ложно.


Если вместо этого вам нужно «оценить» истинностное значение формулы в конкретном мире с присвоением истинностных значений атомам , например

ш ⊩ {р, д}

в этом случае мы просто применяем семантические спецификации.

Ясно, что w ⊩ p & q и w ⊩ p → q , а значит, w ⊩ (p & q → (p → q)) и так далее.

Отношение доступности необходимо для оценки модального оператора ; у нас так:

w ⊩ □p тогда и только тогда , когда w' ⊩ p для всех w' таких, что wRw' .

Моя искренняя благодарность!!. Еще пара (наивных) вопросов: 1. Почему мы должны принимать в качестве «(нашего) актуального мира» мир, где q ложно, а p истинно, как это канонически имеет место в модели S5 (где мир s1 имеет эти значения)? Делаем ли мы сами по себе, или это делается произвольно? В моем примере с RL и p, и q, безусловно, истинны, значит ли это, что я должен взять мир, в котором p и q истинны, как мой «исходный мир», а затем посмотреть, какие миры доступны из этого мира?
_продолжение_2. Правильно ли я понимаю, что каждый мир имеет только определенный вид отношений доступности к определенному набору других миров? То есть имеет ли мир {p,q} (оба значения положительные) другие доступные миры, чем, скажем, мир {p}, и мы должны принимать во внимание только непосредственно доступные миры? Конкретно, в этом случае {p,q} я не могу произвольно решить, что мой мир имеет, скажем, «рефлексивное» отношение к другому миру, когда в модели это не так?
продолжение 3. Что мы делаем, когда сам антецедент содержит модальные операторы, как в []p & [] q -> [] (p -> q)? Мы обычно переводим формулы в FOL через стандартный перевод? Как нам это сделать в мире {p,q}?
Вы сказали: Отношение доступности необходимо для оценки модального оператора □; мы имеем, что: w ⊩ □p тогда и только тогда, когда w' ⊩ p для всех w' таких, что wRw'. А когда это не тот случай, когда отношение рефлексивно? Я думал (просто чтобы показать вам, насколько слаба моя хватка), что некоторые миры могут иметь такое отношение, а некоторые нет? И я должен проверить, какие отношения существуют в каждом случае?