MathJax와 자연 연역

Fitch style proof나 truth tree proof (tableaux method) 등을 통한 자연 연역 표기를 \(\LaTeX\)에서는 패키지 추가를 통해 할 수 있는데, 유감스럽게도 MathJax는 관련 익스텐션을 제공하지 않는다. 그래서 align을 통해 아래와 같은 Lemmon style proof를 시험 삼아 작성해 보았다.

$$
\begin{align}
&\{1\}&&1.&&\forall x(Fx\supset Fa)\tag{Ass.}\\
&\{2\}&&2.&&\neg Fa \tag{Ass.}\\
&\{1, 3\}&&3.&&Fu \supset Fa\tag{1 UI}\\
&\{1, 3\}&&4.&&\neg Fu\tag{2, 3 MT}\\
&\{1\}&&5.&&\neg Fa\supset\neg Fu\tag{2-4 Cond.}\\
&\{1\}&&6.&&\forall x(\neg Fa\supset\neg Fx)\tag{4 UG}\\
&&&7.&&\forall x(Fx\supset Fa)\supset\forall x(\neg Fa\supset\neg Fx)\tag{1-6 Cond.}
\end{align}
$$

이 증명식을 작성하기 위한 코드는 다음과 같다:

$$\begin{align}
&\{1\}&&1.&&\forall x(Fx\supset Fa)\tag{Ass.}\\
&\{2\}&&2.&&\neg Fa \tag{Ass.}\\
&\{1, 3\}&&3.&&Fu \supset Fa\tag{1 UI}\\
&\{1, 3\}&&4.&&\neg Fu\tag{2, 3 MT}\\
&\{1\}&&5.&&\neg Fa\supset\neg Fu\tag{2-4 Cond.}\\
&\{1\}&&6.&&\forall x(\neg Fa\supset\neg Fx)\tag{4 UG}\\
&&&7.&&\forall x(Fx\supset Fa)\supset\forall x(\neg Fa\supset\neg Fx)\tag{1-6 Cond.}
\end{align}$$

그런데 이렇게 쓰자니 탭(&)이 너무 많아서 표기가 번거롭다. 해서 탭을 몇 개 제거해 보았는데, 다음과 같이 나타난다:

$$
\begin{align}
&\{1\}&1.&\forall x(Fx\supset Fa)\tag{Ass.}\\
&\{2\}&2.&\neg Fa \tag{Ass.}\\
&\{1, 3\}&3.&Fu \supset Fa\tag{1 UI}\\
&\{1, 3\}&4.&\neg Fu\tag{2, 3 MT}\\
&\{1\}&5.&\neg Fa\supset\neg Fu\tag{2-4 Cond.}\\
&\{1\}&6.&\forall x(\neg Fa\supset\neg Fx)\tag{4 UG}\\
&&7.&\forall x(Fx\supset Fa)\supset\forall x(\neg Fa\supset\neg Fx)\tag{1-6 Cond.}
\end{align}
$$

이 증명식을 작성하기 위한 코드는 다음과 같다:

$$\begin{align}
&\{1\}&1.&\forall x(Fx\supset Fa)\tag{Ass.}\\
&\{2\}&2.&\neg Fa \tag{Ass.}\\
&\{1, 3\}&3.&Fu \supset Fa\tag{1 UI}\\
&\{1, 3\}&4.&\neg Fu\tag{2, 3 MT}\\
&\{1\}&5.&\neg Fa\supset\neg Fu\tag{2-4 Cond.}\\
&\{1\}&6.&\forall x(\neg Fa\supset\neg Fx)\tag{4 UG}\\
&&7.&\forall x(Fx\supset Fa)\supset\forall x(\neg Fa\supset\neg Fx)\tag{1-6 Cond.}
\end{align}$$

코드는 한 결 나아졌지만 증명식의 표기가 그다지 아름답지 못하다. 명제번호와 명제 사이의 거리가 너무 좁다. 원래 방식대로 쓰는 것이 낫다고 생각한다.

다만 이렇든 저렇든 모바일에서 보기 너무 힘들다는 것이 문제다. 모바일에서 오버플로우된 수식에 스크롤이 적용되게 하긴 했지만, 그래도 뭔가 아쉽다. 딱히 해결할 방법은 없는 것 같다.

그나저나 Lemmon style proof를 배운 적이 없어서, 쓰면서도 맞게 쓰는 것인지를 알 수가 없다. 벤슨 메이츠의 《기호 논리학》 정도가 Lemmon style을 사용하는 교재인데, 다행히 집에 책이 있어 틈틈이 참고를 하며 쓸 수 있을 것 같다. Fitch system이 너무 그립다…(눈물)

SEP는 자연 연역을 다음과 같은 코드로 표기하고 있다.:

$$
\begin{alignat*}{4}
\{1\}\hspace{.2cm} &1. \hspace{.2cm}((p\rightarrow q)\land(\neg r\rightarrow\neg q)) &&\text{Assume} \\
\{2\}\hspace{.2cm} &2. \hspace{.2cm}p   &&\text{Assume}\\
\{1\}\hspace{.2cm} &3. \hspace{.2cm}(p\rightarrow q)  &1,\ & {\land}\text{-Elim}\\
\{1,2\}\hspace{.2cm} &4. \hspace{.2cm}q  &2,3,\ & {\rightarrow}\text{-Elim}\\
\{1\}\hspace{.2cm} &5. \hspace{.2cm}(\neg r\rightarrow\neg q)  &1,\ & {\land}\text{-Elim}\\
\{6\}\hspace{.2cm} &6. \hspace{.2cm}\neg r  & &\text{Assume}\\
\{1,6\}\hspace{.2cm} &7. \hspace{.2cm}\neg q &5,6,\ & {\rightarrow}\text{-Elim} \\
\{1,2,6\}\hspace{.2cm} &8. \hspace{.2cm}(q\land\neg q)  &4,7,\ & {\land}\text{-Intro}\\
\{1,2\}\hspace{.2cm} &9. \hspace{.2cm}\neg\neg r  &\text{6–8},\ & {\neg}\text{-Intro} \\
\{1,2\}\hspace{.2cm} &10. \hspace{.2cm}r  &\text{6–8},\ & {\neg\neg}\text{-Elim} \\
\{1\}\hspace{.2cm} &11. \hspace{.2cm}(p\rightarrow r)  &\text{2–9},\ & {\rightarrow}\text{-Intro}\\
\emptyset\hspace{.2cm} &12. \hspace{.2cm}(((p\rightarrow q)\land(\neg r\rightarrow\neg q))\rightarrow (p\rightarrow r)) &\text{ 1–11},\ & {\rightarrow}\text{-Intro}
\end{alignat*}
$$

\begin{alignat*}{4}
\{1\}\hspace{.2cm} &1. \hspace{.2cm}((p\rightarrow q)\land(\neg r\rightarrow\neg q)) &&\text{Assume} \\
\{2\}\hspace{.2cm} &2. \hspace{.2cm}p   &&\text{Assume}\\
\{1\}\hspace{.2cm} &3. \hspace{.2cm}(p\rightarrow q)  &1,\ & {\land}\text{-Elim}\\
\{1,2\}\hspace{.2cm} &4. \hspace{.2cm}q  &2,3,\ & {\rightarrow}\text{-Elim}\\
\{1\}\hspace{.2cm} &5. \hspace{.2cm}(\neg r\rightarrow\neg q)  &1,\ & {\land}\text{-Elim}\\
\{6\}\hspace{.2cm} &6. \hspace{.2cm}\neg r  & &\text{Assume}\\
\{1,6\}\hspace{.2cm} &7. \hspace{.2cm}\neg q &5,6,\ & {\rightarrow}\text{-Elim} \\
\{1,2,6\}\hspace{.2cm} &8. \hspace{.2cm}(q\land\neg q)  &4,7,\ & {\land}\text{-Intro}\\
\{1,2\}\hspace{.2cm} &9. \hspace{.2cm}\neg\neg r  &\text{6–8},\ & {\neg}\text{-Intro} \\
\{1,2\}\hspace{.2cm} &10. \hspace{.2cm}r  &\text{6–8},\ & {\neg\neg}\text{-Elim} \\
\{1\}\hspace{.2cm} &11. \hspace{.2cm}(p\rightarrow r)  &\text{2–9},\ & {\rightarrow}\text{-Intro}\\
\emptyset\hspace{.2cm} &12. \hspace{.2cm}(((p\rightarrow q)\land(\neg r\rightarrow\neg q))\rightarrow (p\rightarrow r)) &\text{ 1–11},\ & {\rightarrow}\text{-Intro}
\end{alignat*}

그런데 내 방식에서, 동일한 식은 다음의 코드로 표현된다:

\begin{align}
&\{1\}&&1.&&((p\rightarrow q)\land(\neg r\rightarrow\neg q))\tag{Ass.}\\
&\{2\}&&2.&&p\tag{Ass.}\\
&\{1\}&&3.&&(p\rightarrow q)\tag{1 $\land$E}\\
&\{1, 2\}&&4.&&q\tag{2, 3 $\rightarrow$E}\\
&\{1\}&&5.&&(\neg r\rightarrow \neg q)\tag{1 $\land$El}\\
&\{6\}&&6.&&\neg r\tag{Ass.}\\
&\{1, 6\}&&7.&&\neg q\tag{5, 6 $\rightarrow$E}\\
&\{1, 2, 6\}&&8.&&(q\land \neg q)\tag{4, 7 $\land$I}\\
&\{1, 2\}&&9.&&\neg\neg r\tag{6-8 $\neg$I}\\
&\{1, 2\}&&10.&&r\tag{6-8 $\neg$E}\\
&\{1\}&&11.&&(p\rightarrow r)\tag{2-9 $\rightarrow$I}\\
&\emptyset &&12.&&(((p\rightarrow q)\land(\neg r\rightarrow \neg q))\rightarrow (p\rightarrow r))\tag{1-11 $\rightarrow$I}
\end{align}

... 코드의 간명함에서는 아무래도 후자가 낫다.

하지만 이 코드는 아래와 같이 표현된다:

$$
\begin{align}
&\{1\}&&1.&&((p\rightarrow q)\land(\neg r\rightarrow\neg q))\tag{Ass.}\\
&\{2\}&&2.&&p\tag{Ass.}\\
&\{1\}&&3.&&(p\rightarrow q)\tag{1 $\land$E}\\
&\{1, 2\}&&4.&&q\tag{2, 3 $\rightarrow$E}\\
&\{1\}&&5.&&(\neg r\rightarrow \neg q)\tag{1 $\land$El}\\
&\{6\}&&6.&&\neg r\tag{Ass.}\\
&\{1, 6\}&&7.&&\neg q\tag{5, 6 $\rightarrow$E}\\
&\{1, 2, 6\}&&8.&&(q\land \neg q)\tag{4, 7 $\land$I}\\
&\{1, 2\}&&9.&&\neg\neg r\tag{6-8 $\neg$I}\\
&\{1, 2\}&&10.&&r\tag{6-8 $\neg$E}\\
&\{1\}&&11.&&(p\rightarrow r)\tag{2-9 $\rightarrow$I}\\
&\emptyset &&12.&&(((p\rightarrow q)\land(\neg r\rightarrow \neg q))\rightarrow (p\rightarrow r))\tag{1-11 $\rightarrow$I}
\end{align}
$$

장단이 나름 확실하다. 내 코드가 훨씬 간명하고 미려하지만, 가로폭을 너무 많이 잡아먹는다.