> How do you find out if it is valid or not?
Well, try to think about whether it would be possible for the premises to be true and the conclusion false. If this is possible, it's not valid; if it's not possible, the argument is valid. (If necessary you could construct a truth table to determine whether the argument is valid, or you could even plug the premises into Fitch, set the goal to be the conclusion, and use the Taut Con rule to determine whether the conclusion is a tautological consequence of the premises. But in most cases just thinking the argument through should give you a pretty good idea whether it's valid or not.)
Also, if course, if you can construct a proof, that shows that the argument is valid, and if you can construct a counterexample, that shows that it's not valid. But you should try to get an initial sense of whether it's valid or not so you'll know whether to work on a proof or a counterexample.
By the way, read the directions carefully. A counterexample will need to use the predicates available in Tarski's world, not A, B, C, etc. So if you construct a counterexample, you need to construct sentences that use the Tarski's World predicates, but have the same form as the premises and conclusion in the problem. Write the sentences in a .sen file with premises first and conclusion last, and then construct a .wld file in which the premises are true and the conclusion false.
Took me six steps (counting the empty first line as a step, since that's the way Fitch numbers them).
Took me seven steps, including the premise.
Took me 22 steps.
> What is a good way to shorten 30?
This one took me 21 steps. Two of those are because I use ~Intro to prove a negation and then use ~Elim to get what I want -- Fitch would allow doing this in one step, which would make the total 19. If anyone finds a shorter way, please let me know!
The hard part is the subproof from ~(P->Q) to P & ~Q. I did two negation intro subproofs, one to get P and one to get ~Q. First one: assume ~P. Now we need to get a contradiction. Well, we have ~(P->Q) and ~P, so if we could get either P or P->Q we'd be home free. But P is what we're trying to use the subproof to reach, so maybe we'd better try for P->Q instead.
A similar subproof, assuming Q and deriving a contradiction, will get us ~Q. Then &Intro gets us P & ~Q.