코어논리학 술어논리 자연연역 파트 질문입니다

[익명(58.234)]

반대 방향의 추론은 부당하다는 것을 반례모델 찾는 방식이 아니라 자연연역 방식으로 증명할 수는 없을까요??

[익명(180.83)]

없습니다. 태블로를 사용하세요.

[익명(180.83)]

자연 연역 트리 시스템은 증명이 존재하는지 알려주는 시스템입니다. 타당하지 않은 이론에 증명 관점에서 신호를 주는 방법이 없어요. 그래서 이 경우 태블로를 사용하는 것이 옳습니다.

[익명(58.234)]

아하 감사합니다. 저 근데 태블로가 뭐에요?

[익명(180.83)]

semantic tableaux라는 증명 시스템이 있는데, 이 방법은 느려도 결정론적이고 정확한 반례를 줍니다. 국내에는 진리나무라는 방법으로 더 많이 알려져 있는데 애초에 모든 증명이 트리라서 이 이름은 조금 부적합한 듯 해요

[익명(58.234)]

아하 감사합니다!!

[Nb(118.32)]

“자연연역”을 코어논리학에서 사용하는 Fitch 방식으로 보지 않으면 다른 시스템에서 도출가능성 여부도 판단 가능합니다. Decidability 테스트도 연구되고요. Fitch 방식은 증명론에서 주된 시스템으로 사용하지는 않는 편이라서요. Semantic tableux는 국내에 진리나무로 알려진 게 아니라 truth tree라고 전통적으로 씁니다.

[익명(58.234)]

아 코어논리학에서 가르쳐주는 자연연역법이 주류가 아닌가 보군요 - dc App

[Nb(118.32)]

“애초에 모든 증명이 트리라서 이름이 부적합하다.”는 말은 무슨 말인지 모르겠어요. “Semantic tableux”는 이름만 보자면 truth table에 가까운데 이게 더 맞다고 볼 수 있을까요? 문장의 진리값을 분해하는 방식이 나무처럼 진행되니 truth tree도 적절해 보이네요.

[익명(58.234)]

진리테이블 방식은 익숙하긴 한데 뉴비라 semantic tableux란건 처음 듣네요 - dc App

[aa(118.32)]

Structural Proof Theory라는 책을 보시면 자연연역과 정식열 연산에서 decidability를 증명하는 작업을 소개합니다. 물론 고전논리 체계에서는 한계가 있지만요. 그리고 semantic tree method와 관련해서는 역사적으로 볼 때, 오히려 현대로 올 수록 'truth tree'라는 표현을 더 사용하는 것으로 보입니다. 20세기 중반에 유행한 R. Jeffrey의 Formal Logic 뿐만아니라 최근에 꽤나 읽히는 The Logic Book의 경우도 'truth tree'라는 개념을 사용하고 있죠. 윗분의 말씀은 조금 이해하기가 어렵네요.

[익명(58.234)]

아하 감사합니다. 코어논리학 다 보고 다른 증명법 소개하는 책들도 봐야겠군요 - dc App