# Formal proof errors

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.

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. 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. Mar 27, 2019 at 19:48

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! Mar 28, 2019 at 1:38

Proof created with proofs.openlogicproject.org:

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. Mar 28, 2019 at 0:21