Logic Question in a fitch style system - disjunction elimination

I am having difficulty in formally proving two arguments.

Firstly, given the premises

• A ∨ (B∧C)
• ¬B∨¬C∨ D

derive A v D.

I can see why it has to be either A or D, because if it's B and C, then it cannot be ¬B or ¬C so it must be D. And if it's not B and C, then it has to be A. But I can't work out how to show that using disjunction elimination formal proofs (Fitch).

Secondly, I have these premises

• ¬(¬Cube(a)∧Cube(b))
• ¬(¬Cube(b)∨Cube(c))

and I have to derive Cube(a).

I don't really know where to start. Whilst I understand the basic concepts, I'm a complete beginner at applying them formally and I'm struggling to manipulate the formulas in a way that works.

Any help would be greatly appreciated, I've been trying for hours

The key to solving this kind of deduction is how to perform the disjunctive syllogism, i..e how get from A v B and ¬A to B, using disjunction elimination.
The idea is the following: There two cases to consider -- either A or B. Assume A. This leads to a contradiction with the second assumption ¬A, so we get ⊥. From a contradiction we may assume anything, so conveniently we can choose B. And the second case, B, is easy -- we already have our desired conclusion right there, we can just reiterate the assumption. Since from both cases we obtained B, and we know that at least one of the cases is true, we may conclude B for sure. This is disjunction elimination.

Formally, this looks as follows: Now we just need to apply this technique to the disjunctions in your problem.

I can see why it has to be either A or D, because if it's B and C, then it cannot be ¬B or ¬C so it must be D.

First, let's figure out how to conclude from B and C that it cannot be ¬B or ¬C. So we need a subproof with premise B ^ C that has ¬(¬B ∨ ¬C) as its conclusion. We do not apply the disjuntive syllogism technique yet, ths is for later; instead, the idea is a proof by contradiction:
Assume that (¬B ∨ ¬C) does hold, and furthermore add B ^ C to the premise. There are two subproofs: 1. Assume ¬B. Form B ^ C we know B, which is a contradiction to ¬B, hence ⊥. 2. Analogous for ¬C. So from both disjuncts we get ⊥, and by disjunction elimination we are allowed to conclude ⊥. Since the assumption (¬B ∨ ¬C) led to a contradiction, we can apply negation introduction and get ¬(¬B ∨ ¬C), which we wanted because we can plug this in in the other proof. Now we're in the state that we have ¬(¬B ∨ ¬C), and want to conclude D. This is where the disjunctive syllogism enters. ¬(¬B ∨ ¬C) is our ¬A from above, and ((¬B ∨ ¬C) v D) is A v B. So just insert these formulas into the schema from above, and we get Plugging these two pieces together (the second proof is just a continuation of the first proof, which ended with ¬(¬B ∨ ¬C)), we got from B ^ C to D: We successfully proved

if it's B and C, then it cannot be ¬B or ¬C so it must be D.

| B ^ C
| ...
| ¬(¬B ∨ ¬C)
| ...
| D

Now we just need to justify the assumption B ^ C somehow, and get from D to A v D.
The above all happend under the assumption B ^ C. Now B ^ C is just one of the disjuncts in the premise A v (B ^ C). So to complete the proof, we make a second subproof which starts with A, and if we manage to conclude A v D from both cases, then we are allowed to apply a final disjunction elimination and proved A v B from the disjunction A v (B ^ C):

| A v (B ^ C)
| -------------
| | A
| | -----------
| | ...
| | A v D
|
| | B ^ C
| | -----------
| | ...
| | A v D
| A v D            (vE)

So how to fill in the ...s?
In the subproof starting with assumption B ^ C, we already got D, so we can weaken this to A v D by a simple disjunction introduction.
And likewise, in the subproof starting with A, we already got A, so we can weaken this with a disjunction introduction on the other side to A v D.

And no we're done -- this is what the final proof looks like: Using the schema shown above, maybe you can figure out the proof for the cube problem yourself?

This is not likely using the proof checker that you are using, but it may provide a hint on how to proceed. It is however a Fitch-style proof checker.

For the first one consider the following proof using disjunction elimination: I consider both cases of the disjunction in line 1 by starting two subproofs, the first on lines 3-4 and the second on lines 5-16. In both subproofs I was able to derive the goal A v D. That allowed me to use disjunction elimination on line 17, referencing the disjunction on line 1 and the two subproofs.

Here is the second one. Since there were no variables, I simplified the problem by writing Cube(a) as A, Cube(b) as B and Cube(c) as C: I used DeMorgan's law (DeM), conjunction elimination (∧E), disjunctive syllogism (DS) and double negation elimination (DNE). These are available as inference rules in the proof checker I am using. Something similar is likely available in what you are using.

Links to the proof checker and the online introductory logic textbook are below.

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

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf