임의 명제문자 A에 대해서, ⊢A가 증명 불가능하다는 것을 증명하려면

[익명(119.203)]

어떻게 해야 될까요?

저 아래 글의 lp님 덧글에서, ⊢A가 증명 불가능하다는 것을 이용하셨는데,

처음 읽을 때는 너무도 당연해 보여서 당연하지 하고 넘어갔는데, 문득 궁금증이 들었습니다.

이것을 엄밀하게 증명하려고 한다면 어떻게 해야 될까요?

B⊢A

는 어떨까요? 이것도 마찬가지의 이유에서 궁금합니다^^

[lp(50.243)]

⊢A 또는 B ⊢A 를 결론으로 하는 증명에서 마지막으로 사용된 추론법칙이 무엇인지 case analysis 해 보면 됩니다. 결론에 접속사가 없으니 \/R이나 /\L 같은 L/R 법칙일 수는 없고, 남는 것은 axiom 뿐이지만 좌변에 A가 없으니 이도 불가능하죠.

[lp(50.243)]

sequent calculus 가 cut-free 여야 한다는 조건이 붙는 이유는, cut 이 허용될 경우 (임의의 논리식 F 에 대해) ⊢ F 와 F ⊢ A 를 전제로 cut 을 사용해서 ⊢ A 를 얻은 것이 마지막 추론일 수 있기 때문에 위의 case analysis 가 성립하지 않기 때문이지요.

[익명(119.203)]

음.. 만일 A&B 에서 &소거로 얻었을 수도 있지 않나요? 이런 경우는 어떻게 배제할 수 있나요? 귀납법을 쓰는 것 같은데, 쉽진 않네요ㅠ

[lp(24.131)]

소거와 도입 규칙을 쓰는 것은 sequent calculus 가 아니라 자연연역입니다. Cut-free sequent calculus 는 역방향 연역에서 어떤 추론법칙을 쓰더라도 논리식이 더 단순해집니다. 이는 구문론과 증명 자동화에서 sequent calculus 가 선호되는 이유 중 하나이기도 하지요.

[익명(119.203)]

아하 그렇군요. 감사합니다~!

[익명(119.203)]

그러면 자연연역에서는 이를 간단히 보일 수는 없는 것일까요?

[익명(119.203)]

아마도 자연연역에서는 경우가 상당히 많아지는 것 같습니다. 체계에 따라 다르겠지만 ㄱㄱA에서 A를 얻는다던지 하는 것도 기본 규칙으로 해놓은것도 있고 해서요...

[lp(24.131)]

자연연역이 sequent calculus 보다 구문론적으로 다루기 까다로운 근본적인 이유는 전자가 후자보다 더 자유도가 높기 때문입니다. 반대로 말하자면 sequent calculus 는 추론법칙의 적용 순서를 엄격하게 제한한 자연연역이라 볼 수 있습니다.

[lp(24.131)]

[sequent calculus 증명에서 최상단의 initial sequent 로부터 밑으로 내려가면서 sequent 가 변화하는 과정] = [자연연역 proof tree 가 순차적으로 구성되면서 변화하는 과정] 이라고 생각하면 이를 시각적으로 쉽게 이해할 수 있습니다.

[lp(24.131)]

따라서 자연연역이 sequent calculus 만큼 편리한 구문론적 성질을 가지려면 후자에 준하는 추론 순서의 제한을 걸어야 합니다. 어렴풋한 기억으로는 polarity switching 같은 테크닉으로 이런 효과를 구현할 수 있었던 것 같은데... 정확한 레퍼런스가 좀 긴가민가 하네요. 솔직한 감상으로는 이런 품을 들이느니 그냥 sequent calculus 를 쓰는 게 더 편하기도 하구요.

[익명(119.203)]

그렇군요. 아직 초보라서, 말씀하신 내용을 전부 이해하지는 못하지만 깊은 함의가 있는 말씀이신 것 같습니다. 더 공부하면서 생각해 보겠습니다. 그리고.. 나중에라도 레퍼런스가 기억나시면 부탁드립니다^^

[익명(119.203)]

혹시 normalization 이라는 기법으로 constant를 쉽게 증명할 수 있는 것 같은데, 그것에 의하면 ㅏA도 ㅏㄱA도 증명 불가능하다는걸 알 수 있지 않나요? normalization 이 뭔지 몰라서 자신이 없습니다... 혹시 명제논리에 한해서라도 normalization을 공부할 만한 자료도 있나요?

[lp(96.66)]

그러고 보니 기본인 normalization 을 잊고 있었네요. Normalize 된 자연연역 증명은 subformula property 를 가지는데, 이는 Γ ⊢ φ 의 증명에 사용되는 모든 논리식이 Γ ∪ {φ} 의 원소이거나 원소의 subformula 임을 뜻합니다. 따라서 ⊢A 의 normalize 된 자연연역 증명에는 (A의 subformula 가 아닌) A /\ A 가 등장할 수 없으므로 마지막 추론 법칙이 /\E 가 아님을 알 수 있죠.

[lp(96.66)]

명제논리 normalization 의 기본은
http://www.math.helsinki.fi/logic/sellc-2010/course/restall.pdf
이 텍스트에 잘 소개되어 있습니다.

[익명(119.203)]

아하 그렇군요. 그걸 이용하면 쉽게 증명할 수 있겠군요. 정말 감사합니다. 링크해주신 자료도 잘 읽겠습니다. 감사합니다~!