Does anyone know the Fitch program/ system used for logical proofs ?
I am stuck with using fitch to construct a proof of¬(¬A∨¬B) from the premises A and B ... This is how it looks like in fitch https://i.stack.imgur.com/6mn55.png and this is what I have done so far https://i.stack.imgur.com/hQlpN.png
When doing Fitch proofs, set-up is key!!
OK, so your goal is $\neg (\neg A \lor \neg B)$ ... which is a negation ... which suggests a proof by Contradiction, i.e $\neg$ Intro. Now, here is the all-important point: when setting up the proof by contradiction, make sure to enter the $\bot$ at the end of the subproofs, and to apply the $\neg$ Intro rule before doing anything else! That is, do:
Notice how you can already check out the $\neg$ Intro rule!
OK, so now you have $\neg A \lor \neg B$ to work with, which is a disjunction, so that suggests setting up a proof by cases, i.e. $\lor$ Elim:
Again, though, make sure that at the end of each subproof you put the statement that is going to be your goal before doing anything else. OK, but what is the goal? Well, since you're within the subproof of the proof by contradiction, that goal is $\bot$. So:
Again, notice how you can already check the correct application of the $\lor$ Elim rule.
OK, so this is what's called the proof skeleton (or proof plan, or proof strategy, or proof overview, or proof organization, or ... ). This gives you the basic organization of the proof. The rest is details ... and as you found out yourself, the rest is in fact completely trivial!
Good luck with future Fitch proofs!