최원배 교수님 논리적사고의기초 에서 Lemmon스타일(Suppes-Lemmon)을 다루고 있는 부분이 있는데, 제가 추천하고 싶은 테이블 증명은 이쪽이에요. proof tree랑 호환되는거 보이는것도 쉽고, 말인즉슨 proof tree 그리는 거랑 난이도가 똑같다는 거고.


그에 비해 사실 Fitch스타일은 가정 순서도 편하게 못바꾸고 복잡한 증명에서 편한 기법은 아닙니다. (뭐 진짜 복잡한 증명은 다들 비형식적으로 해버리겠지만)
sequent형태로 바꿔보면 아시겠지만 substructural rule이 집합이 아니라 LIFO 스택 형태로 나옵니다. 즉 Fitch는 자연연역이 아니라 자연연역하고 동치인 subset을 쓰는 격이라, 좀 많이 돌아가야 하는 부분이 있어요.

물론 증명만 되면 장땡이다 라고 생각할 수도 있겠는데, 힐베르트연역이 심플한 것처럼 굴다가 그냥 쓰기엔 너무 토나온다고 메타정리로 연역정리(자연연역선 →I로 이미 있는거) 도입하고 추론규칙처럼 쓰는 삽질을 보고있자면 처음부터 쎈 거 쓰는 게 나은 거 같아요.