I am trying to prove the sequent $$\lnot T \to \lnot F,\lnot A \to \lnot T, F \vdash A. $$ I thought I had come up with a solution entailing assuming not-A, then using arrow elimination and RAA to prove A. However, I cannot seem to prove the arguments validity using a logic Daemon. Where am I going wrong? I assume somewhere in (7) or (8).
The first column indicates the active assumptions or context under which the statement is derived, and this is typically numbered by the line on which an assumption was raised (by the rule of assumption: $\mathsf A$). Further, the first three assumptions are premises; the conclusion should have all three active, and no other.
The active assumptions for an inference the active assumptions are the union of the context for the lines from which it is derived, unless the rule discharges one of the assumptions. RAA is such a rule of discharge.
Reduction Ad Absurdum requires a contradiction to be derived so that one of that line's active assumptions may be discharged. Eg lines 3 and 6 contradict, enabling assumption 4 to be discharged.
$$\boxed{\begin{array}{crlr} 1 & (1) & \neg T\to\neg F & \mathsf A\\ 2 & (2) & \neg A\to\neg T & \mathsf A\\ 3 & (3) & F &\mathsf A\\ 4 & (4) & \neg A&\mathsf A\\ 2,4 & (5)& \neg T &2,4~{\to}\mathsf E\\ 1,2,4 & (6) & \neg F&1,5~{\to}\mathsf E\\ 1,2,3 & (7) & A & 3,6~\mathsf{RAA}~(4)\hspace{-4ex} \end{array}}$$