Natural Deduction proof: C Ʌ D, C ↔ E |- (C V F) Ʌ (D V F) Ʌ (E V F)

This is one of the tasks that I'm working on in Logic class of a CS degree program at University.

The teacher just said to me that my answer was wrong, but she never told me when I asked her where I made a mistake. All she says is "You are not using the logical rules correctly, review it and fix the mistakes"

1 C Ʌ D Premise

2 C ↔ E Premise

3 C 1 (VE)

4 D 1 (VE)

5 C -> E 2 (↔E)

6 (C V F) Ʌ (D V F) Ʌ (E V F) 3, 4, 5 (ɅI)

I realized that the part "1 (VE)" for 3 and 4 should have been "1 (ɅE)", but can't really tell what other mistakes are left.

** I attached a screenshot so it'll be easier to read.

screenshot

Revised version

• Perhaps she wants you to explicitly write down that you deduce $C \lor F$ from $C$ via disjunction elimination. Also in the textbook I used biconditional $A \leftrightarrow B$ elimination works not by producing $A \rightarrow B$, but by allowing you to assume $A$ and deduce $B$ in that subproof. But AFAIK these things differ in different textbooks. – CrabMan Apr 24 at 9:02
• Thanks for your comment. I know that I omitted some steps instead of writing down literally every single steps, but the problem was I didn't know exactly what steps I happened to omit. I edited the post and attached another screenshot, where I revised in green. Do you see anything I'm still not explicit enough or anything I did in a wrong way? – Shinichi Takagi Apr 24 at 9:30
• José Carlos Santos, thank you for the links! I didn't know how to make the formula in my question look nicer and ended up just writing all of them in plain text. I'll check the links you gave me and make the most of them from the next time I post a question! – Shinichi Takagi Apr 24 at 10:46

1. As you already figured out, steps 3 and 4 are applications of $$\land E$$, not $$\lor E$$.
2. In step 5 when you apply the $$\leftrightarrow E$$ rule, your conclusion is not the implication $$C \to E$$, but the proposition $$E$$. The point of $$\leftrightarrow E$$ (at least by all the formulations of the rule that I am aware of, but that depends on what particular rule set you are using) is that given $$A \leftrightarrow B$$ and $$A$$, you can conclude $$B$$ and vice versa, i.e. exchange one formula for the other. Alternatively, if $$\leftrightarrow E$$ indeed gives you only the implication for one direction ($$C \to E$$), you would in addition have to apply $$\to E$$ together with $$C$$ to obtain $$E$$, since $$E$$ is the formula you need to construct $$E \lor F$$.
3. You can't just mash together multiple rule applications in one line, as you did in line 6:
First derive each of the disjunctions $$C \lor F, D \lor F, E \lor F$$ individually by three applications of $$\lor I$$. Then introduce the conjunction in two $$\land I$$ steps: First $$(C \lor F) \land (D \lor F)$$, then $$((C \lor F) \land (D \lor F)) \land (E \lor F)$$.

With this, your proof should be as follows: (produced with the Natural deduction proof editor and checker)

• Thank you! Your explanation is really direct to the point and concise, and it's extra helpful that you even included a step by step concrete example! – Shinichi Takagi Apr 24 at 10:41

I think that this is an exhaustive list of your errors:

as you already realized 3 and 4 are really instances of conjunction elimination, and not disjunction elimination.

By the definition of the biconditional 5 can be thought of as another instance of conjunction elimination (I've never seen a rule like "biconditional elimination", not even in advanced textbooks on proof theory so I can't say whether you applied it correctly, I suspect it's like a modus ponens for the biconditional but there's no need for it)

You're missing an instance of modus ponens to go from $$C \rightarrow E$$ to $$E$$.

You skipped the 3 disjunction introduction to obtain formulae like $$\;C\vee F$$.

The revised version is better but you should introduce the disjunctions first on the three formulae, and then the final conjunction. (To be overly pedantic there should be two uses of conjunction introduction at the end).

• I wanted to say hello but it gets cancelled automatically in the answers, so hello. – Simone Apr 24 at 10:16
• Thanks for your comment. It seems there are fairly many steps that are omitted in my thinking process. The challenge is that how to explicitly extract them and write them down. It feels hard now but I'll try to get used to it! – Shinichi Takagi Apr 24 at 10:43