예를 들어서,
ㅏ ((A->B)->C) <->(A->(B->C))
는 항진명제가 아니니까, 증명할 수도 없는데, 그것을 증명할 수 없다는 것을 증명하려면 어떻게 해야 하나요?
꼭 의미론적으로 항진명제가 아니라는 것과 명제논리의 완전성을 이용해야 하나요???
(완전성을 이용한다는게 너무 파리 잡는데 총을 쏘는 것 같은 느낌이 들어서요 ㅠ)
구문론적으로도 할 수 있을것 같은데, 일반적인 방법이 있나요? 아니면 케바케인가요???
어떤 논리식을 '증명할 수 없다'는 것을 증명하기
익명(119.203)
2019-07-31 21:58
추천 0
댓글 19
다른 게시글
-
기호논리학 질문 하나만 올립니다. [6]익명(220.118) | 19.07.27추천 0
-
이런 논리를 뭐라고 하나요? [1]익명(124.49) | 19.07.21추천 0
-
힐베르트 스타일과 자연 연역의 차이가 의미하는 바가 뭘까요? [2]익명(119.203) | 19.07.16추천 0
-
숙명여대 펜스룰 사건보면익명(14.43) | 19.07.15추천 0
-
양상논리와 술어논리의 주된 차이점? [5]익명(223.62) | 19.07.13추천 0
-
수리논리학입문 출판되었는데 깜빡했다. [3]톱니까막(nonli) | 19.07.10추천 0
-
자연스럽게 행동하라고 강요하는 사람들이익명(119.70) | 19.07.10추천 1
-
일본에서 논리학 공부하면서 인상깊었던 점 [9]PaulSohn(paulsohn) | 19.07.08추천 30
-
논리학은 현실적 문제의 완전한 해결책이 아님not Tarski(219.249) | 19.07.07추천 28
-
논리학 출판 툴 [3]톱니까막(nonli) | 19.07.06추천 2
증명가능성은 증명 하나를 제시하면 바로 보일 수 있지만, 증명불가능성은 무한한 수의 증명들이 가지는 일반적 성질을 보여야 하지요. 후자가 훨씬 강한 주장인 만큼 이를 증명하기 위해 더 복잡한 테크닉을 동원하는 것이 딱히 이상하거나 피해야 할 일은 아니라고 봅니다.
물론 저도 일반적으로는 의미론과 완전성 정리가 필요하다는데 동의합니다. 그렇지만 예를 들어 ㅏ a &~a 처럼 거짓임이 분명해보이는 단순한 경우에는 간단한 증명이 가능하지 않을까 해서요. 보기를 이걸로 들을걸 잘못했네요.
이 경우에도 구문론적으로는 추론규칙을 케이스별로 따져야 되는 건가요?그렇다면 매우 귀찮은 일이 될 것 같긴 하네요 ㅎ
말씀하신 명제논리와 같은 경우 sequent calculus의 invertibility를 사용하는 방법이 가장 간단한 일반적 방법 아닐까요? ⊢((A→B)→C)↔(A→(B→C)) ⟹ ⊢(A→(B→C))→((A→B)→C) ⟹ (A→(B→C))⊢((A→B)→C) ⟹ ... ⟹ B⊢A,C 이지만 B⊬A,C 이므로 ⊬((A→B)→C)↔(A→(B→C)).
계속 수정하는데 유니코드가 도저히 먹지를 않네요; 어쨌든 connective 마다 invertibility 를 따로 보여야 한다는 점은 맞습니다.
다만 sequent calculus 자체가 구문론의 탈을 쓴 countermodel construction이기 때문에 이 방법은 좀 반칙에 가깝긴 하지요.
⊢A&~A 는 cut-free sequent calculus에서 마지막에 사용 가능한 규칙이 &R 뿐이고, ⊢A 와 ⊢~A 어느 쪽도 증명불가능하므로 invertibility에 대한 보조정리 없이도 바로 보일 수 있습니다.
음, 좋은 답변 감사합니다. 헌데 제가 지식이 짧아서 잘 못 알아듣겠습니다..ㅠ 죄송하지만 connective의 invertibility가 무엇인지 조금 설명해 주실 수 있나요? 그리고 첫번째로 제시해주신 증명에서 ⟹ ... ⟹를 못 따라가겠는데 어떻게 앞에서 그걸 유도할 수 있나요??
또 sequent calculus 자체가 countermodel construction는 무슨 뜻인가요? 순수 구문론이 아니라는 뜻인가요? 혹시 관련 자료를 알려주실 수 있으신가요?? 흥미로운 이야기 같은데, 처음 듣는 말이라서요..
Invertibility의 개요는 joo.gl/dyZof 이 노트의 Proposition 3를 참조해 보시면 도움이 될 것 같습니다.
`A ⟹ B` 는 A로부터 한 번의 inversion으로 B를 얻을 수 있다는 뜻입니다 (표준적 기호는 아니고, 그냥 편의로 화살표를 사용했습니다).
따라서 `A ⟹ B ⟹ C ⟹ ... ⟹ Z` 는 [A 가 증명 가능하다면 B가 증명 가능하고, B가 증명 가능하다면 C가 증명 가능하고... Z가 증명 가능하다" 로 읽으시면 됩니다.
Sequent calculus는 여타 proof calculus에 비해 의미론과 더 밀접한 관계를 가집니다. 예를 들어 sequent calculus를 이용한 증명 탐색 도중 증명이 불가능한 subgoal sequent가 생성되면 이 sequent로부터 당초의 conclusion이 증명 불가능함을 보이는 countermodel을 곧바로 얻을 수 있습니다. 그래서 해당 방식의 증명 탐색을 countermodel 구성 알고리즘으로 보기도 합니다. 저도 어디선가 읽거나 들은 이야기인데, 정확한 출처는 기억이 안 나네요.
정말 고맙습니다. 링크해주신 문서 잘 읽겠습니다~ 또 sequent가 그런 의미를 갖는다는 것도 처음 들었습니다. 흥미로운 말씀 감사합니다.
보통 반례를 찾곤 하죠. 물론 반례의 해석(이 경우 T,F 진릿값)과 추론규칙이 sound하다는 건전성정리가 뒷받침되어야 하고요. 반례는 lp님 말씀대로 sequent calculus로 찾아낼 수도 있습니다. 다만 이건 명제논리나 순수 1차논리처럼 공리가 없을 때 얘기고, PA같이 공리가 끼어들었을 경우 공리계에서 모순이 증명된다면 임의의 문장이 (그 부정과 동시에) 증명가능하므로 '증명 불가능하다'는 보일 수 없게 됩니다. (이 경우 공리를 만족시키는 반례도 찾을 수 없죠)
답변 감사합니다. 아, 완전성이 아니라 건전성이 필요하군요. 완선성이 필요한 줄 알았는데 착각했습니다. 제 수준이 이렇습니다 ㅠㅠ 논리외적 공리가 있기만 하면 항상 '증명 불가능하다'는걸 보일 수 없다는 말씀이 아니라 공리가 consistent하지 않을 때 증명불가능한 명제가 없으니까 그렇다는 말씀이시죠? 그리고, 사실 sequent calculus로 반례를 찾아낸다는게 좀처럼 이해가 안 되는데 여기에 대해서 더 설명해주실 수 있으신가요??
네, 논리외 공리가 있어도 consistent하다면 상관없죠. 조금 에매하게 썼네요.
sequent inversion으로 B|- A,C라는, 1. 각 문장이 연결사 없이 원자명제이며 2. 어떤 문장도 양쪽에 동시에 나타나지 않는 시퀀스를 찾아냈다면, 그 다음은 간단합니다. 그냥 왼쪽(B)에 전부 T를, 오른쪽(A,C)에 전부 F를 할당하면 그게 반례가 되지요.
아하, 그렇군요. 좋은 답변 정말 고맙습니다~