안녕하세요 걍 논리학이랑 무관한 대학생이고
이산수학 배우면서 코딩하는데 교재에서 수리논리학적 배경들을 얼렁뚱땅 넘어가는게 좀 개운하지가 않아서 파고들어가다보니
어쩌다 이쪽까지 와버렸네요
근데 자연 연역에서 종류가 보통 fitch 스타일, lemmon 스타일, 겐첸 스타일, prawitz 스타일
등등 종류가 뭔 시발 존나게 많드라구여;;
거기에 자연 연역 외의 증명 체계까지 포함하면 힐베르트체계, 시퀀트계산 등등
하여튼 자연 연역에서 행 단위로 구성되는 표 형태(테이블) 방식의 증명 연산이 있고
그리고 첨부한 짤처럼 바 오른쪽에 연산자 붙이는 방식의 증명 연산도 있고
트리로 되어있는 증명 연산도 있더군요
대체 자연 연역의 스타일은 몇가지가 있고 스타일마다 형태(트리, 테이블, 짤같은 방식)는 몇가지가 되고 그것들은 뭐라 정의하고 명명하는지
알려주세요
오른쪽에 뭐 써 둔 건 그냥 위를 전제로 할 때 아래를 도출하는 규칙을 우측의 표기와 같이 약호한다는 뜻입니다. 자연연역은 잘 알고 있으신 것처럼 겐첸, 피치, 레먼 스타일 등이 있고, 시퀀트 연산은 별다른 체계가 아니라 그냥 표기법입니다. '트리로 되어있는 증명'은 아마 tableau method를 뜻하는 것 같은데, 겐첸 시스템에서의 자연연역을 표현하는 방식 중 하나가 '증명 나무 방식'(이와 대조되는 게 시퀀트 방식)이라서 tree라고 부를 경우 혼동의 여지가 있습니다. (tableau를 tree라고 부르기는 부르는 것 같아요.) 잘 알고 있으신 것 같은데...