$P \to \lnot P: \lnot P$ in 11 lines The tools that can be used are DNE, DNI, augmentation, MT, MP, &I, &E, and CP - nothing else. According to the Tomassi Logic Textbook, this should take 11 lines. I get the following 10 line solution.
{1}    1. $P \to \lnot P$                 [P]
{2}    2. $P$                              [A for CP]
{3}    3. $P \to \lnot P$                 [A for CP]
{2,3} 4. $\lnot P$                         [MP 2,3]
{2}   5. ($P \to \lnot P) \to \lnot P$   [CP 3,4, discharge 3]
{2}   6. $\lnot \lnot P$                      [DNI 2]
{2}   7. $\lnot (P \to \lnot P$)             [MT 5,6]
{ }    8. $P \to \lnot (P \to \lnot P$)     [CP 2,7 discharge 2]
{1}   9. $\lnot \lnot (P \to \lnot P$)           [DNI 1]
{1}   10. $\lnot P$                         [MT 8,9]
I'm probably being really dumb here, but I'm not seeing how to do this in 11 lines. What am I missing?
 A: $$\begin{array}{l}\{1\}&1.&P \to \lnot P&[\mathsf P]
\\
\{2\}    &2. &P&[\textsf{A for CP}]
\\
\{3\}    &3. &P \to \lnot P&                 [\textsf{A for CP}]
\\
\{2,3\} &4. &\lnot P&                         [\textsf{MP 2,3}]
\\
\{2\}   &5. &(P \to \lnot P) \to \lnot P&   [\textsf{CP 3,4, discharge 3}]
\\
\{2\}   &6. &\lnot \lnot P&                      [\textsf{DNI 2}]
\\
\{2\}   &7. &\lnot (P \to \lnot P)&             [\textsf{MT 5,6}]
\\
\{ \}    &8. &P \to \lnot (P \to \lnot P)&     [\textsf{CP 2,7 discharge 2}]
\\
\{1\}   &9. &\lnot \lnot (P \to \lnot P)&           [\textsf{DNI 1}]
\\
\{1\}   &10. &\lnot P&                         [\textsf{MT 8,9}]
\end{array}$$
In a Fitch format that would be:
$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{~~1.~P\to\lnot P}{\fitch{~~2.~P}{\fitch{~~3.~P\to\lnot P}{~~4.~\lnot P}\\~~5.~(P\to\lnot P)\to\lnot P\\~~6.~\lnot\lnot P\\~~7.~\lnot(P\to\lnot P)}\\~~8.~P\to\lnot(P\to\lnot P)\\~~9.~\lnot\lnot(P\to\lnot P)\\10.~\lnot P}$$
So, yes, those ten lines are valid, and you have used only the allowed rules — in fact only CP, MP, MT, and DNI.
