2

I am trying to show in intuitionistic logic that ~(A & B) > (~A v ~B) using the deduction theorem and weak excluded middle (~A v ~~A). I already proved (~~A & ~~B) > ~~(A&B) and ~(A & B) > (A > ~B)

My assumptions are:

  1. ~(A & B)
  2. ~~A v ~A
  3. ~~B v ~B

First I want to show that (~A v ~~A) > (~A v ~B) so I want to show that ~A > (~A v ~B) and ~~A > (~A v ~B) so I can use the axiom that [(A > C) & (B > C)] > [(A V B) > C]:

  1. ~A > (~A v ~B) by the axiom that A > (A v B)
  2. ~~A (assumption)

From here I want to get ~A v ~B and use the deduction theorem to get ~~A > (~A v ~B) but I don't know how to show ~A v ~B.

I get a similar issue when I try to show (~B v ~~B) > (~A v ~B): I can get ~B > (~A v ~B), but I don't know how to get ~~B > (~A v ~B)

I am really stuck; please help.

Improve this question
3
  • 4. is fine with Disjunction Introduction. Thus you are in 5. with assumption ~~A and you use weak LEM again: ~~B v ~B. From assumption 6. ~B you have (~A v ~B) again by Disjunction Intro. The last step is to use 7. ~~B to derive ¬A ∨ ¬B. How to do it? by three contradictions...
    – Mauro ALLEGRANZA
    Commented Dec 14, 2022 at 11:02
  • You have to assumptions: ~~A and ~~B. Start a sub-proof assuming ~(A & B) with also A and B; with then you get (A & B) and thus a contradiction, from which ~A: contradiction again (with ~~A) thus you derive ~B and we have a contradiction again (with ~~B) from which we conclude with the negation of the last temporary assumption to get: ~~(A & B). Now we have a contradiction with the original premise and we conclude (as per answer below) with (~A v ~B) by Explosion.
    – Mauro ALLEGRANZA
    Commented Dec 14, 2022 at 11:07
  • Having derived (~A v ~B) in all branches of the two weak LEMs, we can conclude with (~A v ~B) by Disjunction Elimination twice.
    – Mauro ALLEGRANZA
    Commented Dec 14, 2022 at 11:08

1 Answer 1

Reset to default
1

As I expect you know, this version of the de Morgan law: ¬(A & B) → (¬A ∨ ¬B) is not provable in intuitionistic logic, which is why you have to use weak excluded middle as an additional assumption.

A rough sketch of a proof is as follows. From ¬A ∨ ¬¬A together with ¬B ∨ ¬¬B we have four cases:

  1. ¬A & ¬B
  2. ¬A & ¬¬B
  3. ¬¬A & ¬B
  4. ¬¬A & ¬¬B

In cases 1 and 2, we can get ¬A and hence ¬A ∨ ¬B. In case 3, we can get ¬B and hence ¬A ∨ ¬B. In case 4, we can prove ¬¬(A & B) but this contradicts the given antecedent ¬(A & B), so it proves ⊥ and hence by explosion ¬A ∨ ¬B.

So, we have ¬A ∨ ¬B in all four cases and we just need to assemble the cases by iterative use of the OR-3 axiom.

Improve this answer
2
  • Thanks for your response. The informal reasoning makes complete sense to me, my difficulty is formalizing it. I don't get how we can just assume whatever we want. I was told to assume ~~A and from that get ~~A -> (~A v ~B) using the deduction theorem. I do not see how to formalize this particular step.
    – Clio
    Commented Dec 13, 2022 at 23:26
  • By the deduction theorem, from Γ ∪ {α} ⊢ β it follows: Γ ⊢ α → β. In effect it allows you to introduce any assumption α you like, derive β, and thus get to α → β.
    – Bumble
    Commented Dec 14, 2022 at 13:10

You must log in to answer this question.

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