늦어서 미안~
이런식으로 그림그려서 자연연역 표현하는 방법이 Gentzen Style 표기법인가봐.
나는 Ian Chiswell, Wilfrid Hodges의 Mathematical Logic이라는 책에서 배웠어~
저 그림을 설명하자면, 우선 산수에 비유할 수 있을 것 같아.
1. ----- 이렇게 그은 밑줄 오른쪽에 (->E), (->E), (vE) 이게 산수의 +, -, *, / 덧셈 뺄셈 기호에 해당하고,
2. ---- 그은 줄 위의 formula((A->C), (B->C) 등)들이 1 + 2에서 1과 2(피연산자)에 해당해.
3. 그리고 --- 아래의 formula(C)가 1 + 2 = 3의 3에 해당해(연산결과).
지나가던 사람인데 위에 보면 ∨E 규칙을 적용했는데, ∨E 규칙 자체가 A∨B, A→C, B→C // C 이거 아니야?
규칙 정의가 교과서마다 다르기도 한걸까? 내가 배운 text에선, 저렇게 discharged assumption을 언급하는 내용이 (vE) 규칙에 있었어. 그래서 엄밀히 말하면 내가 배운 내용이랑은 댓글달아준 내용은 다른 것 같아 - dc App
어느 쪽을 규칙으로 쓰는지는 책 마음입니다. 비슷하게 고전귀류법 ~A ㅏ ⊥ // ㅏ A이나 이중부정제거 ㅏ ~~A // ㅏ A도 상호환 가능하고요. 저건 특히나 호환되는게 너무 뻔해서 좋은 증명 문제는 아니네요...
제가 알기로 겐첸이 원래 제시한 ∨E는 1+1=2님이 말씀하신, 가정 해제가 딸린 규칙이었습니다. 좀더 현대에서는, Curry-Howard isomorphism느낌을 받아들여서 112.34님 표현의∨E를 쓰기도 하는 것 같아요. (저도 후자를 선호합니다.)
이거 그냥 규칙으로 쓴다는거 아니임? (-.-)a
ㅇㅅㅇa - dc App
->E 에 대해 설명좀 해주셈
앗.. 그.. 내가 사실은 아니지만 대충 비유로 느낌만 설명해 줄 수는 있어. 하지만 정확히 사실을 말하려면 몇가지 배경지식을 얘기해야하고. - dc App
그런데 대충 사실이 아닌 얘기를 하면 내가 거짓말을 한게 되서 안하느니만 못한 설명일까봐.. - dc App
zzz 설명안해도됌 고마움