Box some equations inside align

Question

I'm trying to make something like this:

But I have just can't figure out how. I have tried with empheq and tikz, but I can't get it to work with only some boxes inside align. I have also tried with \boxed and \Aboxed, no success either.

I have a few example of what I have tried:

\documentclass[12pt]{article}
\usepackage[danish]{babel}
\usepackage [utf8]{inputenc}
\usepackage{moreverb}
\usepackage{listings}
\usepackage{graphicx}
\usepackage{verbatim}
\usepackage{amsmath}
\usepackage{empheq}

\begin{document}
\begin{align*}
& 1 &(p \wedge q) \wedge r && \text{premise} \\
& 2 & p \wedge q && \wedge_e_1 1 \\
& 3 & r && \wedge_e_2 1 \\
& 4 & p && \wedge_e_1 2 \\
& 5 & q && \wedge_e_2 2 \\
& 6 & q \wedge r && \wedge_i 5,3 \\
& 7 & p \wedge (q \wedge r) && \wedge_1 4,6
\end{align*}
\end{document}

This gives me something like the format but no boxes. Then I thought I could ditch the first column by just numerate the equations on the left with: \documentclass[12pt, leqno]{article}, but I have no idea on have I'm going to box some of the lines.

So I hope one of you experts can help me make something like this in Latex.

EDIT: I'm getting a bit closer my goal, I have now succesfully mad one box:

$$
\begin{tabular}{ccl}
1 & \neg p \rightarrow p & \text{premise} \\
\cline{2-3}
2 & \multicolumn{1}{|c}{\neg p} & \multicolumn{1}{l|}{\text{assumption}} \\
3 & \multicolumn{1}{|c}{p} & \multicolumn{1}{l|}{\rightarrow_e 2,1} \\
4 & \multicolumn{1}{|c}{\bot} & \multicolumn{1}{l|}{\neg_e 3,2} \\
\cline{2-3}
5 & \neg \neg p & \neg_i 2-4 \\
6 & p & \neg \neg_e 5 
\end{tabular}
$$

So the question is now. How do I make a Box inside the Box?

Answer 1

Here is a MWE using the tikzmark library.

\documentclass[letterpaper]{article}
\usepackage{amsmath}
\usepackage{array}
\usepackage{tikz}
    \usetikzlibrary{tikzmark}   

\begin{document}
\renewcommand{\arraystretch}{1.2}
    \begin{tabular}{l@{\hspace{2em}}ll}
        1 & $p\wedge q\rightarrow r$ & premise\\
        2 & \pgfmark{a}$p$ & assumption\\
        3 & \pgfmark{c}$q$ & assumption\\
        4 & $p\wedge q$ & $\wedge i\ 2,3$\pgfmark{d}\\
        5 & $q\rightarrow r$ & $\rightarrow i\ 3-5$\pgfmark{b}\\
        6 & $p\rightarrow (q\rightarrow r)$ & $\rightarrow i\ 2-6$
    \end{tabular}
    \tikz [remember picture]{ 
    \draw [overlay,->] ([shift={(-1em,2ex)}]pic cs:a) rectangle ([shift={(1.5em,-1.25ex)}]pic cs:b);
    \draw [overlay,->] ([shift={(-0.75em,2ex)}]pic cs:c) rectangle ([shift={(2.5em,-1.25ex)}]pic cs:d);}
\end{document}

On a quick note, since most of your content is to be in mathmode, you can use an array instead of a tabular. I have edited your example below:

{\renewcommand{\arraystretch}{1.2}
$\begin{array}{ccl}
1 & \neg p \rightarrow p & \text{premise} \\
\cline{2-3}
2 & \multicolumn{1}{|c}{\neg p} & \multicolumn{1}{l|}{\text{assumption}} \\
3 & \multicolumn{1}{|c}{\pgfmark{e}p} & \multicolumn{1}{l|}{\rightarrow_e 2,1\pgfmark{f}} \\
4 & \multicolumn{1}{|c}{\bot} & \multicolumn{1}{l|}{\neg_e 3,2} \\
\cline{2-3}
5 & \neg \neg p & \neg_i 2-4 \\
6 & p & \neg \neg_e 5 
\end{array}$}
\tikz [remember picture]{% 
    \draw [overlay,->] ([shift={(-1.5em,2ex)}]pic cs:e) rectangle ([shift={(2em,-1.25ex)}]pic cs:f);}