With a premise that $p \implies q$ how does this Fitch system proof "prove" that $\neg q \implies \neg p$?

Question

I am having trouble getting a "feel" for Fitch system proofs. I was surprised at the resolution of this problem in the Stanford Logic class using their Fitch system engine.

It seems trivially obvious that $(\phi \implies \psi) \models (\neg \psi \implies \neg \phi)$ in the sense that given the premise that "if $\phi$, then $\psi$", then, if it is the case that there is $\neg \psi$, then this implies there must be $\neg \phi$. The truth tables bear this out such that $(\phi \implies \psi) \equiv (\neg \psi \implies \neg \phi)$:

| $p$ | $q$ | $\neg q$ | $\neg p$ | $p \implies q$ | $\neg q \implies \neg p$ |

T | T| F | F |    T    |     T     |  
T | F| T | F |    F    |     F     |  
F | T| F | T |    T    |     T     |  
F | F| T | T |    T    |     T     |  

I am not quite grokking how this Fitch system proof "proves" it tho:

1) $p \implies q$ --------Premise
2) | $\neg q$ --------------Assumption
3) | | $p$ --------------Assumption
4) | | $\neg q$ ------------Reiteration, 2
5) | $p => \neg q$ -------Implication Introduction: 3, 4
6) | $\neg p$ --------------Negation Introduction: 1, 5
7) $\neg q \implies \neg p$ ----Implication Introduction: 2, 6

I understand that I am negating a contradiction to derive $\neg p$, but I am not quite understanding how the Fitch system is demonstrating this as a conclusive proof (say as compared to evaluating the truth table).

I am confused at a couple points.

1. Am I using $\models$ and $\equiv$ correctly?
2. Why does the second assumption increase the "level" of sub-proof?
3. Is reiteration merely a staging maneuver, i.e. is the implication introduction always such that the Fitch proof translates "top to bottom" into an implications "left to right"?
4. why is it necessary to reiterate 2?
   i.e. why does this:
   1) p => q ------Premise
   2) | ~q --------Assumption
   3) | | p --------Assumption
   ...result in this:
   4) | p => p ----Implication Introduction: 3, 3
   ...when I select 2 & 3 for implication introduction?
5. I like doing long division, but Fitch feels like a rococo long division. Where truth tables might quickly become akin to doing long division with Roman numerals, is the elegance of Fitch just not as apparent when working with $2^2$ truth values?

Answer 1

Comments

1) Yes: we may say that truth-table "proves" $\vDash$ why the "calculus" (like Natural Deduction, the proof system implemented in Fitch) "proves" $\vdash$.

2) The "indenting" of sub-proofs is a way to keep track of assumptions and the way what depends on what. Thus the inner sub-proof depends both on assumption 3) and on assumption 2).

3) Yes; reiteration is not "formally" necessary. If we "run" the derivation by hand using paper and pencil, we can check visually that after step 3) the assumption 2) is "still there" and we are not forced to re-write it.

4) The re-iteration of $\lnot q$ under assumption $p$, in order to use $\to$-intro to derive $p \to \lnot q$, is not strictly necessary.

In Natural Deduction, a correct use of $→$-intro is: from $q$, derive $p → q$, for $p$ whatever.

The inference is valid because, assuming $q$ (i.e. that $q$ is true), we have that, by the truth-table for the conditional, $p→q$ must be true.

I suppose that this "move" is not implemented in Fitch, and thus the system needs the re-iteration.