Given two axioms from mereology below, I wish to prove that assuming part is a transitive relation then proper part is also transitive. See (Strict) Proper Parthood.
The following is a description of the proof below in more detail.
I assume the antecedent $(ProperPart(a,b) \land ProperPart(b,c))$ and then try to prove the consequent $ ProperPart(a,c)$.
The proof unfolds the definition of $ProperPart$ in $(ProperPart(a,b) \land ProperPart(b,c))$ and then attempts to prove the unfolded $ProperPart(a,c)$, which is $Part(a,c) \land \neg Part(c,a)$.
This proof task requires the proof $Part(a,c)$ and $\neg Part(c,a)$. On line 13 I used $\implies$-Elem to prove $Part(a,c)$. On line 19 I used $\neg$Intro to prove $\neg Part(c,a)$.
I used the Fitch software to validate the proof.
Questions: Is $\neg$Intro necessary to prove this theorem? Is there any general advice on when $\neg$Intro is necessary?
Note the commentary delivered by your formal proof system at line (19): it calls the rule you are applying "$\neg$ Intro".
And yes, the rule you are applying -- what you are, I think, calling Proof by Contradiction, what is often called Reductio ad Absurdum -- is the canonical way to prove a negated wff in your standard sort of natural deduction system, it is the standard introduction rule.
So it's not as if $\neg$ Intro/RAA is (in general) a short cut or avoidable detour; it's not an added derived rule (like e.g. Disjunctive Syllogism is in some systems). It is baked into the system, and your only option when you want to introduce a negation sign.
Contrast "$\neg$ Intro" with the double negation rule, or equivalently the rule that says "given a proof from $\neg\alpha$ to $\bot$, infer $\alpha$. This rule is not constructively valid; so as Mees de Vries implies, you do have a reason to avoid unnecessary applications of this rule if you want to keep your proof constructive. But $\neg$ Intro/RAA is constructively in good order -- so use it freely!