Докажите ◇(p ∨ q) → (◇p ∨ ◇q) и ◇(p ∧ q) → (◇p ∧ ◇q) в модальной логике K.

Я был бы очень признателен за краткое изложение доказательства одной из формул или обеих:

1) ◇(p ∨ q) → (◇p ∨ ◇q)

2) ◇(p ∧ q) → (◇p ∧ ◇q)

Мне разрешено использовать следующие процедуры доказательства модальной логики K:

1) Тавтологии пропозициональной логики ПК

2) Аксиома К: ◻(φ → ψ) → (◻φ → ◻ψ)

3) Modus ponens, правило отстранения: (p → q), p ⊢ q

4) гёделевский перевод G: если φ, то ◻φ

5) ◇φ = ¬◻¬φ

6) если φ → ψ и ψ → ϑ, то φ → ϑ

7) если φ → ψ, то ◻φ → ◻ψ

Мне удалось доказать (◇p ∨ ◇q) → ◇(p ∨ q) , но у меня проблемы с этими двумя формулами.

РЕДАКТИРОВАТЬ: Что я придумал до сих пор (в середине еще не хватает нескольких шагов):

  1. (¬p ∧ ¬q) → ¬p (тавтология ПК)

  2. (¬p ∧ ¬q) → ¬q (тавтология PC)

  3. ◻(¬p ∧ ¬q) → ◻¬p (если φ → ψ, то ◻φ → ◻ψ)

  4. ◻(¬p ∧ ¬q) → ◻¬q (если φ → ψ, то ◻φ → ◻ψ)

  5. (◻(¬p ∧ ¬q) → ◻¬p) → [(◻(¬p ∧ ¬q) → ◻¬q) → (◻(¬p ∧ ¬q) → (◻¬p ∧ ◻¬q) )] (тавтология ПК)

  6. (◻(¬p ∧ ¬q) → ◻¬q) → (◻(¬p ∧ ¬q) → (◻¬p ∧ ◻¬q)) (modus ponens (3, 5))

  7. ◻(¬p ∧ ¬q) → (◻¬p ∧ ◻¬q) (modus ponens (4, 6))

  8. пропущенные шаги

  9. (◻¬p ∧ ◻¬q) → ◻¬(p ∧ q) (ВОТ ЧТО Я ХОЧУ)

  10. [(◻¬p ∧ ◻¬q) → ◻¬(p ∧ q)] → [¬◻¬(p ∧ q) → ¬(◻¬p ∧ ◻¬q)] (тавтология ПК: (p → q ) → (¬q → ¬p))

  11. ¬◻¬(p ∧ q) → ¬(◻¬p ∧ ◻¬q) (modus ponens (9, 10))

  12. ◇(p ∧ q) → (◇p ∧ ◇q)

Честно говоря, я не знаю, как начать. В примере (◇p ∨ ◇q) → ◇(p ∨ q) я начал с ¬(p ∨ q) → ¬p и ¬(p ∨ q) → ¬q . 1) ◻¬(p ∨ q) → ◻¬p 2) ◻¬(p ∨ q) → ◻¬q 3) (◻¬(p ∨ q) → ◻¬p) → [(◻¬(p ∨ q ) → ◻¬q) → (◻¬(p ∨ q) → ◻¬(p ∧ q))] 4) ... modus ponens x 2 5) (◻¬(p ∨ q) → (◻¬p ∧ ◻¬q)) → ((¬◻¬p ∨ ¬◻¬q) → ¬◻¬(p ∨ q)) 6) (¬◻¬p ∨ ¬◻¬q) → ¬◻¬(p ∨ q) Однако я действительно не знаю, как доказать ◇(p ∨ q) → (◇p ∨ ◇q)
Вот подсказка. Предположим ◇(p ∨ q), затем предположим ¬(◇p ∨ ◇q) и получим противоречие. Если вы получаете противоречие, это означает, что если ◇(p ∨ q), то (◇p ∨ ◇q).
@EliranH Спасибо за ответ, но боюсь, что это не поможет. Я должен дать прямое доказательство, основанное на основных тавтологиях, таких как ¬(p ∨ q) → ¬p . Я могу, однако, неправильно понять ваш намек. Если это так, не могли бы вы уточнить, как применить ваши рассуждения.
@Keelan Я отредактировал свой исходный пост и добавил то, что придумал до сих пор, в середине еще не хватает нескольких шагов. Не могли бы вы просмотреть мое доказательство и помочь мне с пропущенными шагами?

Ответы (1)

Посмотрим, смогу ли я дать вам подсказку для стратегии, а не полное доказательство. Возьмем ваше второе предложение в качестве кандидата на доказательство:

◇(p ∧ q) → (◇p ∧ ◇q)

  1. Начните с доказательства ◇(p ∧ q) → ◇p, а также ◇(p ∧ q) → ◇q. Легко доказать их ◻ аналоги: (p ∧ q) → p является тавтологией PC, поэтому вы можете вывести ◻((p ∧ q) → p) и, следовательно, по K-аксиоме ◻(p ∧ q ) → ◻стр. Доказательство ◇ аналогов требует дополнительных шагов, потому что вам нужно использовать эквивалентность ◇φ и ¬◻¬φ и доказать противоположное. В общем, всегда так, что если φ → ψ, то ◇φ → ◇ψ, хотя это не нужно как отдельная аксиома внутри K, потому что ее можно вывести из других.

  2. Теперь, когда у нас есть ◇p и ◇q, нам нужно добраться до ◇p ∧ ◇q. Если бы нам позволили разобраться в правилах PC, это было бы легко, потому что это просто вводное правило для ∧. Но ваша проблема указывает на то, что мы можем использовать только тавтологии ПК, а не его правила. Полезный совет состоит в том, что правилу ПК соответствует условная тавтология. Итак, в общем, если в PC мы можем доказать ψ из φ, то материальное условное φ → ψ является тавтологией. Таким образом, правило введения для ∧ подразумевает, что следующее является тавтологией: φ → (ψ → (φ ∧ ψ)) и, следовательно, ◇p → (◇q → (◇p ∧ ◇q)).

  3. Теперь вы должны быть в состоянии показать, что ◇(p ∧ q) влечет каждое из ◇p и ◇q и, следовательно, по транзитивности влечет ◇p ∧ ◇q.