I am trying to prove A ^ B from the premises shown in the screenshot. As you can see in the screenshot I am struggling with the second sub-sub proof. Do you have recommendations for how to continue/finish the proof?

Thank you. enter image description here

Edit You can only use conjunctive, disjunctive, and negation intro/elim and only uses TautCon for DeMorgans.

I updated the picture of the problem. I am only struggling to cite the lines (I think).

  • Are you allowed to use double negation (~~P therefore P) or V-elim (P v Q, ~P, therefore Q) rules? These rules might be called different names depending on your book. Commented Mar 27, 2019 at 18:23
  • After step 5 use or-elim. Two cases a) ~~A i.e. A and with premise 1 it's ok. case b) ~B anf thus a contradiction with premise 1 from which A and again it's done. Commented Mar 27, 2019 at 19:48

2 Answers 2


Edit You can only use conjunctive, disjunctive, and negation intro/elim and only uses TautCon for DeMorgans.

You also seem to be using rules called "contradiction introduction", and "contradiction elimination". So I suspect what you call "negation elimination" is what is more usually called "double negation elimination".

Anyway, you have the first five lines okay.

 1|  B                 Promise
 2|_ ~((~A & B) v C)   Promise
 3|  ~(~A & B) & ~C    2, Taut Con (DEM)
 4|  ~(~A & B)         3, Conjunctive Elimination
 5|  ~~A v ~B          4, Taut Con (DEM)

Then you should have just used Disjunction Elimination.

 6| |_ ~~A            Assumption
 7| |  A              6, Double Negation Elimination
 8| |  A & B          7, Conjunction Introduction
  | + 
 9| |_ ~B             Assumption
10| |  #              1,9, Contradiction Introduction
11| |  A & B          10, Contradiction Explosion
12| A & B             5,6-8,9-11, Disjunctive Elimination

You can also prove this without invoking de Morgan's Law

You have B as a promise, so you just need to derive A. You may do that by reduction to absurdity.

 1|  B                 Promise
 2|_ ~((~A & B) v C)   Promise
 3|  |_ ~A             Assumption
 4|  |  ...            ...
 5|  |  ...            ...
 6|  |  #              Contradiction Introduction  5
 7|  ~~A               Negation Introduction       3-6
 8|  A                 Double Negation Elimination 7
 9|  A & B
  • Thank you! I now understand the concept! Commented Mar 28, 2019 at 1:38

Proof created with proofs.openlogicproject.org:

enter image description here

The proof assumes that you can use the double-negation rule and the disjuction-elimination rule. (When asking for help with logic problems, it's a good idea to say which rules you're allowed to use since different texts/programs allow different rules that others may not.) Also, lines 6-8 can be simplified by inferring ~~B from B (line 1) if your rules allow it. As far as I could tell, the proof tool I used does not so I had to go about it in a roundabout way.

  • Thank you, I updated the question to show my progress and the rules I can use. I cannot understand your citations (I am very new at this) but use I can use double negation and disjunctive elimination. Commented Mar 28, 2019 at 0:21

You must log in to answer this question.

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