Is there a good resource for how to understand the rules of a Fitch proof system, or an alternative? I'm currently trying to get a sense or how things are proved in natural deduction, which differs in that context changes are allowed / assumptions can be introduced and discharged, and so on.
Can you still make a proof using the line-by-line approach like you could in a Hilbert system? I don't really understand the usefulness of the Fitch system when it's hard to type and present outside of a handwritten diagram. Is there an "equivalent" way we can represent what's going on, perhaps, so that the Fitch system is easier to understand?
I get that an indentation level is a "new context" or an "introduced assumption" but I don't know what we're allowed to write on which lines in general, when we're allowed to discharge an assumption, when we know when we've proven something, when we are finished, etc.
A reference that might rapidly get you past concerns with using Fitch-style natural deduction is the forallx Calgary Remix: An Introduction to Formal Logic text and the corresponding general-use, Fitch-style proof checker. See links below.
For example, consider a proof of disjunctive syllogism: $¬A, A ∨ B ∴ B$.
Here is how the proof checker might allow you to prove this:
There are two options: TFL (Truth Functional Logic) and FOL (First Order Logic). They work for general purpose questions and not only the problems in the text. The software resolves formatting issues with the indented subordinate proofs and provides an ability to check along the way to make sure mistakes have not been made.
The text provides a slightly different proof in section 19.2 as well as providing an introduction to the other rules available in natural deduction along with an introduction to formal logic.
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, Winter 2018. http://forallx.openlogicproject.org/