Question

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: ~(A & B)~~A v ~A~~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]: ~A > (~A v ~B) by the axiom that A > (A v B)~~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. 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: ¬A & ¬B¬A & ¬¬B¬¬A & ¬B¬¬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. A. From ¬(A & B), assume ¬A. B. Then, ¬A ∨ ¬B follows by disjunction introduction. B. Assume ¬B. D. ¬A ∨ ¬B follows again by disjunction introduction. E. Combine both cases (¬A ∨ ¬B) by disjunction elimination.

Answer 1

To show that ~(A & B) > (~A v ~B) in intuitionistic logic, we can use a proof by cases. We assume the negation of each statement individually and show that ~A v ~B follows in each case. By combining all cases, we conclude that ~(A & B) > (~A v ~B) using weak excluded middle.

Step-by-step explanation:

The law of the excluded middle is a logical law that states that for any statement, either that statement or its negation is true. In intuitionistic logic, this law is not provable, so we need to use weak excluded middle as an additional assumption. To show that ~(A & B) > (~A v ~B), we can use a proof by cases. Assume ~(A & B) and show that ~A v ~B follows in all possible cases:

1. Assume ~A. In this case, we have ~A v ~B by disjunction introduction.
2. Assume ~B. Similarly, we have ~A v ~B by disjunction introduction.
3. Assume ~~A. From ~~A, we can derive A using double negation elimination. Since ~(A & B) > (A > ~B), by modus ponens, we have A > ~B. And from A, we can derive ~B using modus ponens again. Therefore, ~A v ~B follows.
4. Assume ~~B. Similarly, we can derive ~A v ~B using the same reasoning as in case 3.

By combining all four cases, we conclude that ~(A & B) > (~A v ~B) using the deduction theorem and weak excluded middle.