I have built a proof for the folowing statement. However I am not sure if it is correct... Could you please help me assert if it is correct?
Edit
I have made my proof based on the exercise 14 of the book Applied Logic for Computer Scientists: Computational Deduction and Formal Proofs
Question
A predicate logic formula $\phi$ belongs to the negative fragment if $\phi$ can be constructed from the following grammar, where $t_1, t_2,..., t_n (n>0)$ are terms:
$\phi::= \hspace{2 mm}\neg p(t_1, t_2,..., t_n)\hspace{2 mm} ||\hspace{2 mm}\bot\hspace{2 mm}||\hspace{2 mm}(\neg\phi) \hspace{2 mm} ||\hspace{2 mm}(\phi\land\phi)\hspace{2 mm}||\hspace{2 mm}(\phi\rightarrow\phi)\hspace{2 mm}||\hspace{2 mm}(\forall_x \phi)$
Prove in minimal logic that $\neg\neg\theta \vdash_m \theta$ for any formula $\theta$ belonging to the negative fragment. Use induction on the structure of $\theta$.
PROOF
(IB) - induction basis
Case $(¬p(t_1,t_2,...,t_n ))$. $¬¬¬p(t_1,t_2,...,t_n ) ⊢_m ¬p(t_1,t_2,...,t_n )$
$\cfrac {\cfrac{\cfrac{}{¬¬¬p(t_1,t_2,…,t_n )} (Ax) \cfrac{[p(t_1,t_2,…,t_n )]^u}{¬¬p(t_1,t_2,…,t_n )}(¬¬_i)}{⊥} (¬_e )}{¬p(t_1,t_2,...,t_n ) } (¬_i )u $
Case $(⊥)$. $¬¬(⊥) ⊢_m ⊥$
$\cfrac{\cfrac{}{¬¬⊥} (Ax) \cfrac{[⊥]^u}{¬⊥} (¬_i) u}{⊥}(¬_e)$
(IS) - inductive step
Case $(¬ϕ)$. $¬¬¬ϕ⊢_m¬ϕ$
$ \cfrac{\cfrac{\cfrac{}{¬¬¬ϕ} (Ax) \cfrac{[ϕ]^u}{¬¬ϕ} (¬¬_i)}{⊥} (¬_e)}{¬ϕ} (¬_i) u $
Case $(ψ∧φ)$. $\neg\neg(\psi \land \varphi) \vdash_m (\psi \land \varphi)$
First, let us denote by $\nabla_0$ the following derivation for $\neg\neg(\psi∧\varphi)\vdash_m \neg\neg\psi\land\neg\neg\varphi$
$\cfrac{\cfrac{\cfrac{\cfrac{}{\neg\neg(\psi\land\varphi)}(Ax) \cfrac{\cfrac{[\neg\psi]^u \cfrac{[\psi\land\varphi]^v}{\psi}(\land_e)}{\bot}(\neg_e )}{\neg(\psi\land\varphi)}(\neg_i )v}{\bot}(\neg_e )}{\neg\neg\psi}(\neg_i)u \cfrac{\cfrac{\cfrac{}{\neg\neg(\psi\land\varphi)}(Ax) \cfrac{\cfrac{[\neg\varphi]^w \cfrac{[\psi\land\varphi]^y}{\varphi}(\land_e)}{\bot}(\neg_e )}{\neg(\psi\land\varphi)} (\neg_i )y}{\bot}(\neg_e )}{\neg\neg\varphi}(\neg_i)w }{\neg\neg\psi\land\neg\neg\varphi}(\land_i )$
By the IH, there are derivations $\nabla_1$ for $\neg\neg\psi\vdash_m \psi$ and $\nabla_2$ for $\neg\neg\varphi\vdash_m \varphi$. The proof is obtained as follows:
$\cfrac{\begin{array}{c}\cfrac{}{¬¬(ψ∧φ)}(Ax)\\ ∇_0 \\ \cfrac{¬¬ψ∧¬¬φ}{\begin{array}{c} ¬¬ψ\\∇_1 (i.h) \\\psi \end{array}} ( ∧_e) \end{array} \begin{array}{c}\cfrac{}{¬¬(ψ∧φ)}(Ax)\\ ∇_0 \\ \cfrac{¬¬ψ∧¬¬φ}{\begin{array}{c} \neg\neg\varphi\\ \nabla_2 (i.h) \\ \varphi \end{array}} ( ∧_e) \end{array}}{ψ∧ϕ}(∧_i )$
Case $(\psi\rightarrow\varphi)$. $\neg\neg(\psi\rightarrow\varphi) \vdash_m (\psi\rightarrow\varphi)$
First, let us denote by $∇_0$ the following derivation for $\neg\neg(\psi\rightarrow\varphi)\vdash_m(\neg\neg\psi\rightarrow\neg\neg\varphi)$.
$\cfrac{\cfrac{\cfrac{\cfrac{}{¬¬(ψ→φ)}(Ax)\cfrac{\cfrac{\begin{array}{c}{}\\{}[¬¬ψ]^u\end{array}\cfrac{\cfrac{\begin{array}{c}{}\\{}[¬φ]^v\end{array} \cfrac{[ψ→φ]^x [ψ]^y}{φ} (→_e )}{⊥} (¬_e )}{¬ψ}(¬_i )y}{⊥}(¬_e)}{¬(ψ→φ)}(¬_i)x}{⊥}(¬_e)}{¬¬φ} (¬_i ) v}{¬¬ψ→¬¬φ} (→_i )u $
By IH, there is a derivation $\nabla_1$ for $\neg\negφ⊢_m φ$. The proof is obtained as follows:
$\cfrac{\cfrac{\begin{array}{c}\cfrac{}{¬¬(ψ→φ)}(Ax\\∇_0\\¬¬ψ→¬¬φ\end{array}\cfrac{[ψ]^w}{¬¬ψ}(¬¬_i) }{\begin{array}{c}¬¬φ\\∇_1(h.i.)\\ φ\end{array}}(→_e)}{ψ→φ}(→_i) w$
Case $(∀_x φ)$. $¬¬∀_x φ \vdash_m ∀_x φ$
First, let us denote by $∇_0$ the following derivation for $¬¬∀_x φ \vdash_m ∀_x \neg\negφ$.
$\cfrac{\cfrac{\cfrac{\cfrac{}{¬¬∀_x φ} (Ax)\cfrac{\cfrac{[¬φ]^u\cfrac{[∀_x φ]^x}{φ} (∀_e )}{⊥} (¬_e )}{¬∀_x φ}(¬_i)x}{⊥} (¬_e )}{¬¬ φ}(¬_i)u}{∀_x¬¬ φ}(∀_i)$
By IH, there is a derivation $\nabla_1$ for $\neg\neg φ \vdash_m φ$. The proof is obtained as follows:
$\cfrac{\cfrac{\begin{array}{c}\cfrac{}{¬¬∀_x\varphi}(Ax)\\\nabla_0\\∀_x¬¬\varphi\end{array}}{\begin{array}{c}¬¬ϕ\\\nabla_1(h.i.)\\\varphi\end{array}}(∀_e) }{∀_x\varphi}(∀_i)$