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

[chabulhwi]

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

음주자 역설

수리 논리학자 레이먼드 스멀리언(Raymond_Smullyan)이 사람들에게 알린 음주자 역설[drinker paradox]은 고전 술어 논리의 정리이고, 그 진술은 다음과 같습니다. 사람이 적어도 한 명 있는 모든 선술집에 대해, 다음 요건을 갖추는 사람 x가 그 선술집에 존재한다. x가 술을 마시고 있으면, 그 선술집에 있는 모든 사람이 술을 마시고 있다. 린 정리 증명기로 이 정리의 증명을 작성했는데, 그 증명은 잠시 후에 공유하겠습니다. 위의 요건을 충족하는 사람의 보기를 들 때, 그 사람이 술을 마시고 있지 않아도 된다는 점이 실마리입니다. 한국어 증명은 다음과 같습니다. 그 선술집에 있는 모든 사람이 술을 마시고 있거나, 그 선술집에 있으면서 술을 마시고 있지 않은 사람이 존재합니다. (배중률, 보편 명제의 부정) 선언 (1)을 이루는 첫째 명제가 참이라고 가정하겠습니다. (가정) 2.1. 그 선술집에는 사람이 적어도 한 명 있으므로, 그런 어느 한 …