1

S1: $A \leftrightarrow(B\vee E)$

S2: $E \rightarrow D$

S3: $C \wedge F \rightarrow \neg B$

S4: $E \rightarrow B$

S5: $B \rightarrow F$

S6: $B \rightarrow C$

I'm not quite sure how logical proofs like this work. If we have $\neg A \wedge \neg B$, do we have to prove both sides of the conjunction? If so, what rule allows us to bring them together?

Jenn Parker
  • 149

4 Answers4

3

Consider a proof by contradiction. Suppose instead that $\neg(\neg A \land \neg B)$ is true so that by DeMorgan's Law, we have that $A \lor B$ is true. Then we claim that $B$ is true. To see this, there are $2$ cases to consider:

  • Case 1: Suppose that $A$ is true. Then by S1 we know that $B \lor E$ is true. Now there are $2$ cases to consider:

    • Case 1.1: Suppose that $B$ is true. Then we're immediately done.
    • Case 1.2: Suppose that $E$ is true. Then by S4 and Modus Ponens, we know that $B$ is true, so we're done.

  • Case 2: Suppose that $B$ is true. Then we're immediately done.

Having established that $B$ is true, notice that by S6 and S5 and Modus Ponens, we know that both $C$ and $F$ is true so that $C \land F$ is true. But then by S3 and Modus Ponens, we know that $\neg B$ is true. But this contradicts the fact that $B$ is true. So we conclude that $\neg A \land \neg B$, as desired.

Adriano
  • 41,576
  • That sounds like a very clever arrangement. Can you perhaps proceed without deriving a contradiction? Is this how proofs of this type are typically conducted? – Jenn Parker Oct 20 '14 at 07:12
  • @JennParker The argument you've provided us with could get proven in an axiomatic system where the only rules of inference are uniform substitution and detachment. So, yes, no contradiction actually has to get derived in the proof. – Doug Spoonwood Oct 22 '14 at 05:03
2

First, by looking at the given propositions S1-S6 we see that they do not immediately show us how to derive $\neg A \wedge \neg B$ by the so-called conjunction introduction inference rule. However, if we observe that

$\neg A \wedge \neg B \equiv \neg (A \vee B)$

we can prove the equivalent negated statement instead.

Since it has the form of a negation, in order to prove it, we assume it as given and then derive a contradiction. With this we are able to conclude that the negation holds. This inference rule is known as negation introduction.

Now, suppose $A \vee B$. How do you derive a contradiction?

We observe that $B$ implies $\neg B$ (see S3,S5,S6), and that $A$ implies $B$ (that implies $\neg B$). Can you continue from here?

Bruno Bentzen
  • 3,362
1

Here's a Prover9 proof [1]. The lower case letters "x, y, z, u, w, v, v5, ... ,vn" in Prover9 are variables. All other lower case letters are nullary functions or equivalently constants. The "|" symbol means logical disjunction or "or". The "-" means logical negation, or "not". You can read "P" as meaning "provable" or "$\vdash$". Assumption 2 "-P(x -> y) | -P(x) | P(y)." via the rule of hyperresolution enables Prover9 to produce results just like condensed detachment does.

% -------- Comments from original proof --------

% Proof 1 at 0.03 (+ 0.01) seconds.

% Length of proof is 76.

% Level of proof is 19.

% Maximum clause weight is 20.

% Given clauses 82.

1 P(-a & -b) # label(non_clause) # label(goal). [goal].

2 -P(x -> y) | -P(x) | P(y). [assumption].

3 P(x -> (y -> x)). [assumption].

4 P((x -> (y -> z)) -> ((x -> y) -> (x -> z))). [assumption].

5 P(x & y -> x). [assumption].

6 P(x & y -> y). [assumption].

7 P(x -> (y -> x & y)). [assumption].

10 P(x | y -> ((x -> z) -> ((y -> z) -> z))). [assumption].

11 P((x <-> y) -> (x -> y)). [assumption].

14 P((-x -> y & -y) -> x). [assumption].

15 P(a <-> b | e). [assumption].

17 P(c & f -> -b). [assumption].

18 P(e -> b). [assumption].

19 P(b -> f). [assumption].

20 P(b -> c). [assumption].

21 -P(-a & -b). [deny(1)].

22 P(x -> (y -> (z -> y))). [hyper(2,a,3,a,b,3,a)].

23 P(((x -> (y -> z)) -> (x -> y)) -> ((x -> (y -> z)) -> (x -> z))).
[hyper(2,a,4,a,b,4,a)].

25 P((x -> y) -> (x -> x)). [hyper(2,a,4,a,b,3,a)].

27 P(x -> (y & z -> y)). [hyper(2,a,3,a,b,5,a)].

29 P(x -> (y & z -> z)). [hyper(2,a,3,a,b,6,a)].

31 P((x -> y) -> (x -> x & y)). [hyper(2,a,4,a,b,7,a)].

32 P(x -> (y -> (z -> y & z))). [hyper(2,a,3,a,b,7,a)].

58 P((x | y -> (x -> z)) -> (x | y -> ((y -> z) -> z))). [hyper(2,a,4,a,b,10,a)].

91 P(x -> ((-y -> z & -z) -> y)). [hyper(2,a,3,a,b,14,a)].

93 P(a -> b | e). [hyper(2,a,11,a,b,15,a)].

107 P(x -> (c & f -> -b)). [hyper(2,a,3,a,b,17,a)].

112 P(x -> (e -> b)). [hyper(2,a,3,a,b,18,a)].

117 P(x -> (b -> f)). [hyper(2,a,3,a,b,19,a)].

122 P(x -> (b -> c)). [hyper(2,a,3,a,b,20,a)].

126 P(x -> (a -> b | e)). [hyper(2,a,3,a,b,93,a)].

132 P(x -> (y -> (e -> b))). [hyper(2,a,3,a,b,112,a)].

149 P((x -> y) -> (x -> (z -> y))). [hyper(2,a,4,a,b,22,a)].

157 P(x -> x). [hyper(2,a,25,a,b,122,a)].

163 P(x -> (y -> y)). [hyper(2,a,3,a,b,157,a)].

196 P((x -> c & f) -> (x -> -b)). [hyper(2,a,4,a,b,107,a)].

204 P(x -> ((y -> z) -> (y -> y & z))). [hyper(2,a,3,a,b,31,a)].

285 P((x -> (-y -> z & -z)) -> (x -> y)). [hyper(2,a,4,a,b,91,a)].

339 P(x | y -> ((y -> x) -> x)). [hyper(2,a,58,a,b,163,a)].

369 P((x -> ((e -> b) -> y)) -> (x -> y)). [hyper(2,a,23,a,b,132,a)].

370 P((a -> (b | e -> x)) -> (a -> x)). [hyper(2,a,23,a,b,126,a)].

371 P((b -> (c -> x)) -> (b -> x)). [hyper(2,a,23,a,b,122,a)].

372 P((b -> (f -> x)) -> (b -> x)). [hyper(2,a,23,a,b,117,a)].

378 P((x & y -> (y -> z)) -> (x & y -> z)). [hyper(2,a,23,a,b,29,a)].

379 P((x & y -> (x -> z)) -> (x & y -> z)). [hyper(2,a,23,a,b,27,a)].

380 P((x -> ((y -> x) -> z)) -> (x -> z)). [hyper(2,a,23,a,b,22,a)].

389 P(b -> (x -> c & x)). [hyper(2,a,371,a,b,32,a)].

407 P(b -> c & f). [hyper(2,a,372,a,b,389,a)].

409 P(b -> -b). [hyper(2,a,196,a,b,407,a)].

418 P(b -> b & -b). [hyper(2,a,31,a,b,409,a)].

424 P(b -> (x -> b & -b)). [hyper(2,a,149,a,b,418,a)].

441 P(b -> x). [hyper(2,a,285,a,b,424,a)].

452 P(x -> (b -> y)). [hyper(2,a,3,a,b,441,a)].

461 P((x -> b) -> (x -> y)). [hyper(2,a,4,a,b,452,a)].

471 P(e -> x). [hyper(2,a,461,a,b,18,a)].

480 P(x -> (e -> y)). [hyper(2,a,3,a,b,471,a)].

494 P((x -> e) -> (x -> y)). [hyper(2,a,4,a,b,480,a)].

506 P((-x -> e) -> x). [hyper(2,a,285,a,b,494,a)].

543 P(b | e -> b). [hyper(2,a,369,a,b,339,a)].

557 P(x -> (b | e -> b)). [hyper(2,a,3,a,b,543,a)].

576 P(a -> b). [hyper(2,a,370,a,b,557,a)].

583 P(x -> (a -> b)). [hyper(2,a,3,a,b,576,a)].

593 P((x -> a) -> (x -> b)). [hyper(2,a,4,a,b,583,a)].

618 P(x -> (y -> y & x)). [hyper(2,a,380,a,b,204,a)].

622 P(--x -> x). [hyper(2,a,285,a,b,618,a)].

670 P(--a -> b). [hyper(2,a,593,a,b,622,a)].

673 P(--b -> x). [hyper(2,a,461,a,b,622,a)].

687 P(--a -> x). [hyper(2,a,461,a,b,670,a)].

694 P(-b). [hyper(2,a,506,a,b,673,a)].

707 P(-a). [hyper(2,a,506,a,b,687,a)].

714 P(x -> x & -a). [hyper(2,a,618,a,b,707,a)].

730 P(-b & -a). [hyper(2,a,714,a,b,694,a)].

800 P(x & y -> (z -> y & z)). [hyper(2,a,378,a,b,32,a)].

827 P(x & y -> y & x). [hyper(2,a,379,a,b,800,a)].

845 P(-a & -b) # label(non_clause) # label(goal). [hyper(2,a,827,a,b,730,a)].

846 $F. [resolve(845,a,21,a)].

1 W. McCune, "Prover9 and Mace4", http://www.cs.unm.edu/~mccune/Prover9, 2005-2010.

Doug Spoonwood
  • 11,211
0

Here is a proof using a Fitch-style proof checker:

enter image description here

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

Frank Hubeny
  • 1,527
  • 2
    You could probably shorten this a bit by putting the proof of $\lnot B$ first; then, assuming $A$, you conclude $B \vee E$, and then use $\vee$-elim along with $E \rightarrow B$ to conclude $B$, then apply $\lnot$ elim with the previous proof of $\lnot B$. – Daniel Schepler Aug 26 '19 at 21:21
  • @DanielSchepler I imagine this could be shortened since a pattern is repeated three times. I wanted to show deriving both conjuncts separately since the OP suggested do we have to prove both sides of the conjunction? – Frank Hubeny Aug 26 '19 at 21:45