자연 연역의 소증명(subproof) 표기법에 관한 생각

논리학
1

방금의 글(조건문에 있어 도입 규칙이란 무엇인가?)에 이어서, 잠시 딴생각이 들어 공유해보는 아이디어입니다.

통상 자연 연역에서 가정의 도입으로 시작하고 해제로 종결되는 소증명(subproof)들은 세로선이나 테두리 박스를 통해 본체 증명과 구분되지요 (Fitch 스타일의 배리에이션들). 그런데 이런 증명 환경을 조판하기란 상당히 까다롭습니다.

이때문인지 《두보계》에서는 가정에 종속된 절들에 별표(*)를 다는 형식을 취합니다. 그런데 이 방법에는 치명적인 문제가 있습니다. 때로 우리는 소증명 내에 또다른 소증명을 취하곤 하는데, 그런 경우를 구현하기가 영 까다롭죠. 별을 두개 달면 된다고는 하지만 보기에 너무 헷갈리게 되고 맙니다.

그러다 문득 든 생각이, ‘어, 그냥 계층형 넘버 구조를 쓰면 되는 것 아닌가?’였습니다. 가령 n번째 라인에서 가정이 도입되고 소증명이 시작되면, n번 이하 라인을 n.1., …, n.m., 형식으로 쓰고, 가정을 해제하는 라인에 n+1번을 다는 것이죠.

예시로, 이 표기법을 사용하면 경우에 의한 논증(P ∨ Q, P → R, Q → R // R)의 타당성을 다음과 같이 증명하게 됩니다.

  1. P ∨ Q (전제)
  2. P → R (전제)
  3. Q → R (전제)
  4. ¬R (가정)
    4.1. ¬P (2, 4 MT)
    4.2. Q (1, 4.1 ∨E)
    4.3. R (4, 4.2. MP)
  5. ¬¬R (4 ¬I)
  6. R (5 ¬E) ∎

앞으로 교안 작성이나 논문 작성 시에 사용해 보아야겠습니다. 잡설 끝.

6개의 좋아요
2

다음 글에서는 제가 계층형 번호 구조로 증명을 작성하긴 했는데, 논리식을 안 썼네요.

2개의 좋아요
3

멋집니다. 이미 이 표기법을 사용한 교재가 없다면, 서강올빼미의 연구성과(ㅋㅋㅋㅋ)로 보고해도 되겠습니다^^;

3개의 좋아요
4

와 깔끔하고 좋네요. 보조선을 그리거나 붙여넣기 귀찮아서 레몬 스타일을 사용했는데 말이죠.

근데 레몬 스타일은 소증명들 간의 층위가 직관적으로 명확하게 보이지 않는 점이 아쉬웠는데, 이 표기법은 그 차이도 잘 보이네요!

3개의 좋아요
5

애용해 주시고… 언젠가 ‘그게 대체 뭔 못배워먹은 표기법이냐’ 하며 묻거든 저와 @chabulhwi 님께 크레딧을 돌려주시길...

4개의 좋아요
6

ㅋㅋㅋㅋㅋㅋ종종 애용하겠습니다

4개의 좋아요
7

이 방법을 LaTeX 용 스타일로 짜봤습니다. 제가 코딩한 건 아니고, 로직만 준 뒤 제미나이에게 만들게 했어요. (GPT는 코딩 바보라서 이런거 못하더라고요.)

제가 만든 스타일에서 다음과 같은 꼴의 코드를 넣으면,

증명 대상: $((P \land Q \land R \land S) \to T) \vdash P \to (Q \to (R \to (S \to T)))$

\begin{hnd}
\h. (P \land Q \land R \land S) \to T \note{전제}
\h.\h. P \note{$\to$I를 위한 가정}
\h.\h.\h. Q \note{$\to$I를 위한 가정}
\h.\h.\h.\h. R \note{$\to$I를 위한 가정}
\h.\h.\h.\h.\h. S \note{$\to$I를 위한 가정}
\h.\h.\h.\h.\h. P \land Q \note{2, ::1 $\land$I}
\h.\h.\h.\h.\h. (P \land Q) \land R \note{.2, :::1 $\land$I}
\h.\h.\h.\h.\h. ((P \land Q) \land R) \land S \note{.3, ::::1 $\land$I}
\h.\h.\h.\h.\h. T \note{1, ::::4 $\to$E}
\h.\h.\h.\h. S \to T \note{:::2 $\to$I}
\h.\h.\h. R \to (S \to T) \note{::2 $\to$I}
\h.\h. Q \to (R \to (S \to T)) \note{:2 $\to$I}
\h. P \to (Q \to (R \to (S \to T))) \note{2 $\to$I}
\end{hnd}

다음 사진과 같은 형태로 파싱됩니다. 여기에서 :은 같은 논증 블록의 단계수를 표시합니다. 가령, 2.2.2.2.n줄에서 :::1을 쓰는 것은 2.2.2.1을 언급하는 것인 식입니다.

image
image636×866 26.2 KB

문장 번호가 길어지는 게 생각보다 치명적인 약점입니다. 우단 note의 길이가 지나치게 길어져서요. : 노테이션을 약정해서 이 문제를 극복하고 있습니다. 표준적인 표기가 되기 어려운 결정적 문제이지만, 어쩌면 꽤나 편할지도 모릅니다.

6개의 좋아요
8

함유된[nested] 부분 증명이 너무 많은 게 보기는 안 좋네요. 한 부분 증명이 둘 이상의 가정을 가질 수 있는 증명 체계가 이 문제점을 해결할 수 있을까요?

9

그건 사실상 Lemmon식 증명인데, 개인적으로는 별로 안 좋아합니다. 어느 명제가 어느 명제의 지배 아래 있는지가 한눈에 안 보여서…. 위에 제시된 전개 방식은 Fitch식 증명에서 소증명을 격자 대신 숫자로 쓴 형태인 것인데, 저는 이쪽이 증명 구조를 보기 더 좋다고 생각해요.

덧) 저는 위 시스템을 위한 레이텍 스타일시트인 hndproof.sty에 5단계 depth까지만을 정의했습니다. Fitch식의 특성상 너무 많은 depth가 적용되면 조판에 애로가 생긴다는 고려 때문에요. 아주 많은 가정이 요구되는 증명은 확실히 Lemmon식이 낫습니다. 다만, 이 경우에도 가정의 수가 너무 많아지면 조판이 좀 못생겨져요. 가정이 많아지면 조판이 못생겨지는 건 모든 자연연역의 특성 같기도 합니다.

2개의 좋아요
10

복잡한 증명은 이용자와 상호 작용을 할 수 있는 파일 형식으로 내보내야 할지도 모르겠네요. 제가 만들려는 게임의 중요한 부분이 그런 기능을 갖춰야 돼요. 상호 작용이 불가능한 문서는 복잡한 증명을 이용자에게 보기 좋게 제시하는 데 한계가 있다고 저는 오래전부터 느꼈어요.

11

그런 점에서는 LaTeX은 증명 공부에는 별로 안 좋습니다. 아무래도 라이브 뷰어 환경이 제공되는 몇몇 환경(가령, Texifier)을 제외하곤 실시간 상호작용은 안 되니까요. 하지만 LaTeX은 조판 시간을 단축시킨다는 강점이 있죠. LaTeX과 유사하면서도 작성자와의 상호작용이 되는 인터페이스가 있다면 좋겠지만, 그 형태는 분명하지 않네요.

2개의 좋아요