What are the syntactic restrictions on proof by contradiction? I am reading Natural Logic by Neil Tennant and I am met with this example of proof by contradiction.


It bothers me that the premise ~Ga was introduced seemingly arbitrarily.
What is to stop me from proving that 10 is prime with

---
Composite(10)
    
    ---
    ~Composite(10)
-------
   #
-------
~Composite(10)  (negating our original premise because we reached a contraditiction)

There must be some syntactic rule that justifies introducing ~Ga but prohibits introducing ~Composite(10), but I am not sure what it would be.
Edit: I think I have a better understanding now after creating some extra examples that are closer to Tennant's example, but where an extra assumption Ha is introduced. In each of them except the last one, the conclusion seems ok to me. But I think there's still something I'm missing because of the fourth example.
        \forall x Fx => Gx
--  --  ------------------
Fa  Ha    Fa => Ga
------------------          ---
       Ga                   ~Ga
       ------------------------
                #
               ---
               ~Ha          (discharge Ha instead of Fa)
          ---------------
             ~Ga => ~Ha
          ---------------
     \forall x ~Gx => ~Ha       (invalid because Fa never gets discharged)

        \forall x Fx => Gx
--  --  ------------------
Fa  Ha    Fa => Ga
------------------          ---
       Ga                   ~Ga
       ------------------------
                #
               ---
               ~Ha          (discharge Ha instead of Fa)
          ---------------
          Fa AND ~Ga => ~Ha
          ---------------
     \forall x Fx AND ~Gx => ~Ha        (vacuously true because the hypothesis will always be false, so no problem here)

        \forall x Fx => Gx
--  --  ------------------
Fa  Ha    Fa => Ga
------------------          ---
       Ga                   ~Ga
       ------------------------
                #
               ---
            ~Ha OR ~Fa      (discharge both Fa and Ha)
          ---------------
          ~Ga => ~Ha OR ~Fa
          ---------------
     \forall x ~Gx => ~Hx OR ~Fx    (still a valid conclusion because the ~Fx part will be true, so we don't have to worry about ~Hx)

        \forall x Fx => Gx
--  --  ------------------
Fa  Ha    Fa => Ga
------------------          ---
       Ga                   ~Ga
       ------------------------
                #
               ---
               ~Ha
          ---------------
            ~Ga => ~Ha
          ---------------
        \forall x ~Gx => ~Ha
      -------------------------
     Fa => (\forall x ~Gx => ~Ha)     (this can't be right, but I'm not sure what's wrong about this discharging of Fa)

 A: There is no restriction in assuming $\lnot G(a)$ or $\lnot \text{Composite}(10)$. You can add whatever further assumption you want. The point is that, later in your derivation, you should have a way to discharge that further assumption. It is really important that at every stage of your derivation is clear which assumptions are still "alive" and which ones have been discharged (that is, they are not hypotheses anymore).
The derivation from Tennant's textbook, assumes $\lnot G(a)$, from it and from the hypothesis $\forall x (F(x) \to G(x))$ it derives $\lnot F(a)$, and then it applies the rule $\to_\text{intro}$ that discharges the assumption $\lnot G(a)$ and gives a derivation of $\lnot G(a) \to \lnot F(a)$ from the only hypothesis $\forall x (F(x)\to G(x))$.
In your attempted derivation about $\lnot \text{Composite(10)}$, read top-down, you start with two assumptions, $\text{Composite}(10)$ and $\lnot \text{Composite}(10)$, you derive a contradiction and then, thanks to the rule $\lnot_\text{intro}$ that discharges the assumption $\text{Composite}(10)$, you have a derivation of $\lnot \text{Composite}(10)$ from the hypothesis $\lnot \text{Composite}(10)$, because your assumption $\lnot \text{Composite}(10)$ has never been discharged and is still "alive".
Clearly, saying that $\lnot \text{Composition}(10)$ under the hypothesis that $\lnot \text{Composition}(10)$, is completely different from saying that $\lnot \text{Composition}(10)$ (without any hypothesis)! The first claim is true and actually you provided a formal derivation of it. The second claim is false and it can never be proved (if your formal system is coherent).
