Я был бы очень признателен за краткое изложение доказательства одной из формул или обеих:
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) , но у меня проблемы с этими двумя формулами.
РЕДАКТИРОВАТЬ: Что я придумал до сих пор (в середине еще не хватает нескольких шагов):
(¬p ∧ ¬q) → ¬p (тавтология ПК)
(¬p ∧ ¬q) → ¬q (тавтология PC)
◻(¬p ∧ ¬q) → ◻¬p (если φ → ψ, то ◻φ → ◻ψ)
◻(¬p ∧ ¬q) → ◻¬q (если φ → ψ, то ◻φ → ◻ψ)
(◻(¬p ∧ ¬q) → ◻¬p) → [(◻(¬p ∧ ¬q) → ◻¬q) → (◻(¬p ∧ ¬q) → (◻¬p ∧ ◻¬q) )] (тавтология ПК)
(◻(¬p ∧ ¬q) → ◻¬q) → (◻(¬p ∧ ¬q) → (◻¬p ∧ ◻¬q)) (modus ponens (3, 5))
◻(¬p ∧ ¬q) → (◻¬p ∧ ◻¬q) (modus ponens (4, 6))
пропущенные шаги
(◻¬p ∧ ◻¬q) → ◻¬(p ∧ q) (ВОТ ЧТО Я ХОЧУ)
[(◻¬p ∧ ◻¬q) → ◻¬(p ∧ q)] → [¬◻¬(p ∧ q) → ¬(◻¬p ∧ ◻¬q)] (тавтология ПК: (p → q ) → (¬q → ¬p))
¬◻¬(p ∧ q) → ¬(◻¬p ∧ ◻¬q) (modus ponens (9, 10))
◇(p ∧ q) → (◇p ∧ ◇q)
Посмотрим, смогу ли я дать вам подсказку для стратегии, а не полное доказательство. Возьмем ваше второе предложение в качестве кандидата на доказательство:
◇(p ∧ q) → (◇p ∧ ◇q)
Начните с доказательства ◇(p ∧ q) → ◇p, а также ◇(p ∧ q) → ◇q. Легко доказать их ◻ аналоги: (p ∧ q) → p является тавтологией PC, поэтому вы можете вывести ◻((p ∧ q) → p) и, следовательно, по K-аксиоме ◻(p ∧ q ) → ◻стр. Доказательство ◇ аналогов требует дополнительных шагов, потому что вам нужно использовать эквивалентность ◇φ и ¬◻¬φ и доказать противоположное. В общем, всегда так, что если φ → ψ, то ◇φ → ◇ψ, хотя это не нужно как отдельная аксиома внутри K, потому что ее можно вывести из других.
Теперь, когда у нас есть ◇p и ◇q, нам нужно добраться до ◇p ∧ ◇q. Если бы нам позволили разобраться в правилах PC, это было бы легко, потому что это просто вводное правило для ∧. Но ваша проблема указывает на то, что мы можем использовать только тавтологии ПК, а не его правила. Полезный совет состоит в том, что правилу ПК соответствует условная тавтология. Итак, в общем, если в PC мы можем доказать ψ из φ, то материальное условное φ → ψ является тавтологией. Таким образом, правило введения для ∧ подразумевает, что следующее является тавтологией: φ → (ψ → (φ ∧ ψ)) и, следовательно, ◇p → (◇q → (◇p ∧ ◇q)).
Теперь вы должны быть в состоянии показать, что ◇(p ∧ q) влечет каждое из ◇p и ◇q и, следовательно, по транзитивности влечет ◇p ∧ ◇q.
Пвниеп Ниепинеп
Элиран
Пвниеп Ниепинеп
Пвниеп Ниепинеп