Proof for sequent in pLJ I'm looking for a proof in the extended sequent calculus pLJ+ for the following sequent:
⊢ ¬¬A → A
pLJ+ is pLJ extended with the axiom ⊢ A v ¬A
Thanks for your help!!
 A: The intuitive argument goes like this:

Suppose $\neg\neg A$ for the sake of argument.
You have $A \lor \neg A$. So argue by cases (what else?!). The first disjunct gives you $A$ trivially. The second disjunct $\neg A$, together with your supposition,  gives you $\bot$ and hence $A$ (by ex contradictione quodlibet). So either way you have $A$.
Now discharge the initial temporary supposition to get $\neg\neg A \to A$.

Now, exercise: massage that intuitive proof idea into sequent calculus form!
A: I will draft two separate sub-derivations (A) and (B) :

$A \rightarrow A$ --- Axiom
$\lnot \lnot A, A \rightarrow A$ --- Weakening-left

$A \rightarrow \lnot \lnot A \supset A$ --- $\supset$-right --- (A)

$A \rightarrow A$ --- Axiom
$\lnot A, A \rightarrow$ --- $\lnot$-left
$\lnot A \rightarrow \lnot A$ --- $\lnot$-right
$\lnot \lnot A , \lnot A \rightarrow$ --- $\lnot$-left
$\lnot \lnot A , \lnot A \rightarrow A$ --- Weakening-right

$\lnot A \rightarrow \lnot \lnot A \supset A$ --- $\supset$-right --- (B)


Now we apply $\lor$-left to (A) and (B) to get :

$A \lor \lnot A \rightarrow \lnot \lnot A \supset A$

Finally, we apply Cut to the last formula with the axiom : $\rightarrow A \lor \lnot A$ (used as cut-formula) and we have :


$\rightarrow \lnot \lnot A \supset A$


