3

I am trying to prove the following:

⊢ (□p ∨ □q) → □(p ∨ q)

However, I think that I am lacking the knowledge of a tautology in classical logic that would help me prove this.

I tried something, but it seems too contrived to work and I'm thinking there's an easier solution.

1.    p → (p ∨ q)            tautology
2.    □(p → (p ∨ q))         necessity axiom
3.    □p → □(p ∨ q)          distribution axiom *
4.    q → (p ∨ q)            tautology
5.    □(q → (p ∨ q))         necessity axiom
6.    □q → □(p ∨ q)          distribution axiom **

Now, I wanted to use the following tautology from classical logic:

⊢ (A → C) → (B → C) → ((A ∨ B) → C)

Where I would substitute A=□p, B=□q, C=□(p ∨ q) which I think would get me the result I want. However, I am unable to get □p and □q alone.

Even more, if I'm to use this in my test, I'd need to prove the tautology via natural deduction first and then use it. Since this is the case, I thought that there had to be another, more easier way to do it.

Could someone help?

Improve this question
4
  • you don't need to get ☐p or ☐q alone. You already have the desired results from 3 and 5 of your answer so you may conclude directly
    – emesupap
    Jun 23 at 20:01
  • 1
    Your proof is very nearly complete. Many systems of natural deduction contain the disjunction elimination rule: A ∨ B; A ⊢ C; B ⊢ C; therefore C. You just need to convert your lines 3 and 6 from conditional sentences into proofs, i.e. with 3, go from □p → □(p ∨ q) to □p ⊢ □(p ∨ q) using modus ponens.
    – Bumble
    Jun 24 at 0:42
  • @Bumble but wouldn't I need to have (□p ∨ □q) as a premise for disjunction elmination to work?
    – john doe
    Jun 24 at 0:52
  • Yes. Just assume (□p ∨ □q) and then discharge your assumption at the end to introduce the conditional. Speaking quite generally, a good rule of thumb for proving conditional sentences is to assume the antecedent, derive the consequent and discharge the assumption using the rule of conditional proof.
    – Bumble
    Jun 24 at 0:59

1 Answer 1

Reset to default
1

We have the theorem p -> p or q. Use necessitation, then K to obtain

☐p -> ☐(p or q). Do similar for the q -> p or q. This is all as you have done so far. Now use disjunction elimimation on "☐p or ☐q" to obtain your desired result.

Improve this answer
7
  • 1
    in other words, your proposed solution is indeed the most direct proof
    – emesupap
    Jun 23 at 20:00
  • I'm sorry I didn't quite understand what my next step (7.) should be. I know I have □p → □(p ∨ q) and □q → □(p ∨ q) but I'm not sure how to get □p ∨ □q → □(p ∨ q) from this, other by the theorem I mentioned (which i would like to avoid since I'd need to prove it in classical logic)
    – john doe
    Jun 23 at 23:17
  • @johndoe the most natural way to proceed is via the theorem you have mentioned- this is the most direct proof. disjunction elimination is built right into the rules of natural deduction, so the proof is mostly trivial in ND. are you using a hilbert style system?
    – emesupap
    Jun 23 at 23:40
  • yes, we follow the rules P1 to P4 mentioned here: en.wikipedia.org/wiki/Hilbert_system. I'm trying to prove it but somehow i always end up stuck
    – john doe
    Jun 23 at 23:44
  • ahh, I see. Have you covered deduction theorem and/or derived rules? even in Hilbert, the way I have mentioned is still the most direct route, although ofc more troublesome
    – emesupap
    Jun 23 at 23:45

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .