# Formal proofs using subproofs

I have been trying to solve this question for couple hours and I still don't get it. The problem I'm trying to solve is 6.14 in the link below. This is what I attempted so far: I'm sure this is wrong, but I don't know the right answer.

6.14 is not valid.

The conclusion can be FALSE and the third premise can still be TRUE : it is enough that SameRow(d,f) is FALSE.

BUT if FrontOf(b,f) allows you to derive ¬SameRow(b,f), in this case the argument is valid.

With it and the second premise you are forced to have SameRow(d,f) true and thus, assuming Cube(f) you have the desired contradiction, concluding with ¬Cube(f).

• It's valid because you can't find a counterexample. So that's why the only way is to do subproofs but I'm not sure how to construct one with this. Do you know? – ashey Nov 8 '16 at 13:49
• @ashey - why "no counterexample" ? If Cube(f) is T, then the purported conclusion ¬Cube(f) is F. With SameRow(c,f) F, then ¬SameRow(c,f) is T. With SameRow(d,f) F and Cube(f) T we have that SameRow(d,f) ∧ Cube(f) is F and thus ¬(SameRow(d,f) ∧ Cube(f) is T. Finally, it is enough that SameRow(b,f) is T to satisfy the first premise. – Mauro ALLEGRANZA Nov 8 '16 at 13:54
• Maybe FrontOf(b,f) has some relationship with the other premises ? – Mauro ALLEGRANZA Nov 8 '16 at 13:55
• IF (big if) FrontOf(b,f) allows you to derive ¬SameRow(b,f), in this case it works : with the second premise, you are forced to have SameRow(d,f) true and assuming Cube(f) you arrive at the desired contradiction, concluding with ¬Cube(f). – Mauro ALLEGRANZA Nov 8 '16 at 15:48