양상논리 soundness 증명하는 책 같은 거 있음?

[익명(210.94)]

양상논리 S5체계 soundness 증명하는 것 좀 보고 싶은데 혹시 책이나 논문 알고 있으신 분 있나요

[익명(180.83)]

양은석선생의 논리와 구조에서 다룸.

[익명(180.83)]

영문으로는 Blackburn이나 더 옛날 책이면 Hughes-Cresswell이나 Chellas가 있음.

[1234(223.38)]

그럼 양상논리 구조에서 2계논리 완전성과 건전성까지 다룬 논문이나 책도 있나요

[두꺼비등핥개(wishes3594)]

그게 없으면 안 되겠죠...?

[1234(211.234)]

completeness의 경우 1계술어는 안되는걸로 증명 됐는데 2계는 뭐 다른가요??

[익명(180.83)]

1차술어논리 완전성은 증명됐습니다. 결정불가능할 뿐입니다.

[1234(121.160)]

결정불가능성과 완전성이 양립이 가능하던가요? 증명을 못하는 명제가 반드시 존재하게 되는데 어떻게 완전하죠?

[익명(180.83)]

완전성과 Undecidability는 아예 별개의 개념입니다.

[1234(121.160)]

괴델의 불완전성 정리가 결정불가능한 명제가 있다는거 아니에요?

[익명(180.83)]

이 부분에 대해 다시 조사해보시는 것이 좋을 듯 합니다. "일차술어논리"는 완전합니다. 그것도 괴델이 증명했고요. 불완전성정리보다 이 정리가 더 중요해요. 반면에 일차술어논리는 결정불가능합니다. 참이거나 거짓으로 결정할 수 있어야 하는데, 문장이 거짓이면서 특수한 경우에는 프로시저가 영원히 끝나지 않을 수 있습니다. 또한 자기 자신을 네스팅할 수 있는 언어(=이차 이상의 술어논리)에는 의미상 참인데도 증명해낼 수 없는 문장이 존재합니다. 이것도 결정불가능성이랑은 또 별개예요.

[1234(121.160)]

감사합니다. 맨 마지막에 말씀하신 2차 술어에서 참이지만 증명 못하는 문장의 존재를 다루는 문제는 키워드를 뭐로 잡고 봐야 할까요? 윗댓글에서 언급해주신 저자의 책에서 증명들을 다루나요?

[익명(180.83)]

바로 그 키워드가 바로 "괴델의 불완전성 정리"입니다. 이 정리는 기본적으로 수학을 완전히 술어논리 체계 상에 일관적이고 궁극적인 방식으로 정립하려는 시도, 예컨대 러셀-화이트헤드의 <수학원리>의 체계가 일관적이라면 참거짓 자체가 결정이 안 되는 문장이 존재한다는 것을 증명하는 것에서부터 시작됩니다. 연관된 문헌은 "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme(On Formally Undecidable Propositions of Principia Mathematica and Related Systems, 수학원리와 관련된 체계들에서 형식적으로 결정불가능한 명제들에 관하여)"에서 다루어지는데요.

[익명(180.83)]

이 논문은 영어번역본의 경우 밴하이어노트(J. van Heijenoort)의 유명한 책에 실려 있고요. 국역본은 아직 없는 걸로 알고있는데, 네이글-뉴먼의 <괴델의 증명>이 번역되어 있고, 이 책에서 자세히 입문할 수 있습니다.

[익명(180.83)]

영역본의 경우 밴하이어노트 말고도 마틴 데이비스 교수 편집의 The Undecidable이라는 논문집에도 실려있다고 기억합니다.