저도 Quiz...

상자 위의 말들과 실제 상황에 모순이 없어야 한다거나
둘다 참이어야 한다거나, 하나는 참이고 하나는 거짓이어야 한다는 등의 조건이 없으니까
명확히 답을 낼 수 없는 거 아닌가요?

은상자의 진술에 참/거짓을 진술할 수 없을 것 같은데요.

금상자에 초상화가 있으면 (은상자의 진술은 (은상자의 진술이 참)이어야 참)이 되는 무한 반복에 빠질 것 같고,
은상자에 초상화가 있으면 (은상자의 진술은 (은상자의 진술이 참)이면 거짓이 되고 (은상자의 진술이 거짓)이면 참)이 되는 자기 부정에 빠질 것 같군요.

그러므로 포샤의 시험은 무효가 되거나, 아니면 그냥 운에 맡겨야 할 것 같습니다.

논리학은 모르겠지만 그저 True or False 로 생각 해보자면...

if ( 은상자 위에 문구 = True )
     금상자 위에 문구 = False 가 되므로
     금상자에 초상화가 있다.
else
     은상자 위에 문구 = False 가 되므로
     if ( 금상자 위에 문구 = True )
          금상자에는 초상화가 없다.
     else
          금상자 위에 문구 = False 가 되므로
          금상자에 초상화가 있다.
end if

결론
두 상자 안에 어딘가에 초상화가 있다는 사실이 참이라면
금상자에 초상화가 있을 확률은 75%
은상자에 초상화가 있을 확률은 25%
ㅡ.ㅡ;; 쿨럭

문제는 장난기가 많다고 해서 반드시 거짓말을 하지는 않으리라는 점입니다. 논리로 결론이 날 수 없다는 쪽에 한표..

이 분 의견에 한표.

답이 나왔으면 이만 알려주시는게...
궁금합니다. +_+

^^ 예, 저 역시 논리적으로는 금상자라고 생각합니다.
위에 적은것은, 문제 내신분께서 말씀하신 "장난끼"에 편승해 적은 것 입니다.

논리적인 답은 금상자 라고 생각하고 있습니다.

포샤는 가장 똑똑한 남편을 얻기를 원합니다.
어려운 퀴즈를 맞추는 사람만이 남편감이 될 수 있습니다.
똑똑한 사람일 수록 어려운 퀴즈를 잘 풉니다.

그러므로 포샤는 가장 어려운 퀴즈를 낼 것입니다.

거짓말을 하면 퀴즈가 어려워집니다.
그러므로 거짓말도 할 것입니다.

여친이랑 놀러갔다 왔더니 이런 퀴즈가 생겼네요.. :P

금상자 위에 있는 진술을 A, 은상자 위의 진술을 B라 해 보겠습니다.

xor 을 둘중 하나만 참이다.. 라는 논리기호라 해보겠습니다.

그렇다면 진술 B는

B= A xor B = A xor (A xor B) = A xor (A xor (A xor B) ) = ...

순환논법입니다.

즉, 명제 B는 참 거짓의 진리값을 가질수 없는 명제입니다.

포샤의 장난기란 이것인가요?

nachnine님이 올려주신 문제를 보니,

예전에 보던 책이 생각나네요.

대충 '이책의 제목은 무엇인가'였던거 같습니다.

그러나 똑똑한 좋은 남편을 얻기를 바란다는 보장도 없습니다. ^^;

말씀대로 자기에게 장난을 치는지를 구분을 못한다면 아마 가장 똑똑한 남편이라고 할 수 없겠죠. 만약 똑똑한 남편을 바란다면 "문제에 오류가"를 지적하는 남편을 고를 것입니다. : )

과연 포샤는 어떤 남편을 바라는 걸까요..? ^^;;

금상자가 참이라면, 은상자가 거짓일 수도 참일 수도 있다.
여기서, 은상자가 참이 된다면, 모순
그러므로, 금상자가 참이라면, 은상자가 거짓. => 은상자에 초상화

장난기가 힌트라면,
결국 문제를 가지고는 초상화를 찾을 수 없다?
잘찍어라?

:roll:

답은 벌써 나왔지만, 넌센스라고 생각하면..

금상자에도 은상자에도 초상화는 없습니다.

문제에서 그 가운데 한 상자라고 했으니까..

금상자와 은상자 사이(가운데) 에 또다른 상자가.. :oops:

정답은 금상자도 맞고 은상자도 맞다.

그러므로 구리상자도 받을 수 있다,

그러나 포샤가 남자 이므로 정답을 맞쳐도 낭패다.

아 덥다.

이건 문제랑 상관없는데요,

문제를 풀때, 문제를 심히 비약적으로 바꿔서 자기만의 답을 내는 경우에는

그런 경우의 답도 있나요?

예를들어, 미로 찾기인데, 인쇄 실수로 벽면에 구멍 뚫린걸 보고,
길이라고 그거 찾아서 출구까지 줄그어 논 사람들이나...

좀 이상하게 보이던데..흐..

문제 보고 문제에서 답을 푸는것이..?

이런... -_-;;;

포샤는 이제 노처녀로 늙어버릴까요...?

아무튼... 진실된 사랑엔 문제도 없는 법...

오페라 '투란도트'의 내용처럼 천자의 딸이 아닌바에야...

//1 .은상자의 진술은 두진술중 딱하나만 참이다.
//2. 금상자의 진술은 "은상자에 있다."
//2. 은상자의 진술이 거짓이라면 '둘다 거짓이거나 둘다 참이다'.

결과부터 생각해서

const 금상자에 초상화가 있다면
금상자의 진술 = false;
은상자의 진술 = true; //은상자의 진술만이 참이다.

const 은상제 초상화가 있다면
금상자 진술 = true;
은상자의 진술은 모순이 된다.
( 은상자의 진술이 참이라면 은상자의 진술(둘중하나만 참)이 거짓(둘다참)이 되므로.
은상자의 진술이 거짓이라면 '둘다 거짓이거나 둘다 참이다' 그래서 은상자 진술이 참(이미 금상자가 참)이 되므로 모순.
)

답은 금상자.(문제에는 오류가 있지만 답은 있네요 :lol: )

저도 댓글을 달았는데

결과부터 생각해보세요

금상자에 있을경우와, 은상자에 있을경우.
금상자에 있을경우는 상자의 글이 논리적이구요

은상자에 있을 경우는 모순입니다.
==
장난기 가득한 포샤는 남편감을 고르기 위해 특이한 시험을 합니다.
특이한 시험은 남편감을 고르기 위한것입니다.

특이한 시험은 금상자,은상자중에 초상화를 넣어두고 상자의 뚜껑에 글을 써놓죠.

금상자 은상자의 글에 신경쓸 필요가 없다면

문제는 "금상자 은상자중에 초상화가 들어있는 상자는?" 과 똑같죠.

밑도 끝도 없이

'전지현 송혜교중 내가 누굴 좋아하게?" 라는 것과 일맥상통하겠네요. :)

말그대로 장난기 가득한 포샤죠.

이런 장난기 가득한 한 포샤의 행동이 quiz가 된다는것 부터 말이안된다고 생각합니다.

"내가 누굴 좋아하게?"
이런 말이 유명한 퀴즈가 된다는것이죠.

논리가 어떤것인지 한글 사전부터 찾아봐야 겠네요.. 제가 잘몰라서.. --;;

논리(論理)[놀―][명사]
1.의론이나 사고·추리 따위를 끌고 나가는 조리(條理).
¶논리를 무시한 글.
2.사물 속에 있는 도리. 또는, 사물끼리의 법칙적인 연관.
¶적자생존의 논리./역사 발전의 논리.
3.<논리학>의 준말.

장난기 가득한
거짓말을 한다는 보장이 없으므로 상자의 글을 보아야함(힌트기때문)
상자의 글을 보든 안보든 상관없지만 힌트가 없기 때문에 그거라도 보아야함.

포샤와 결혼 하기 위해 어느 상자를 골라야 할까요?
당연히 초상화가 들어있는 상자를 골라야 한다.

퀴즈(quiz)[명사]
1.어떤 질문에 대한 답을 알아맞히는 놀이, 또는 그 질문.
2.수수께끼.

어느[관형사]
분명하지 않은 사물이나 사람·때·곳 따위를 막연히 가리키는 말

아ː무
Ⅰ[대명사] 꼭 누구라고 가리키지 아니하고, 들떼놓고 가리킬 때 쓰이는 말. 하모(何某).

====
퀴즈의 답이 '아무상자' 이고 논리적으로 풀어야 한다면
당연히 따지겠죠. 논리라는것이 그런것이니까요.

-_-;; 또 쓰고나니 횡설 수설 이네..

포샤와 결혼 하기 위해 어느 상자를 골라야 할까요?
저 질문을 보고 (1.금상자 2.은상자 3.아무상자 4.아무상자도 아니다)
라는 답의 종류를 생각하는 사람이 몇이나 될까요?
논리적이라는 것은 '사물속이 있는 도리' 입니다.

저 4가지 답을 생각하지 못한다면 세상사람의 몇 %나 비논리적일까요?
제 생각에는 80% 이상일거라고 생각합니다.
그럼, 우리는 비논리적인 세상에 사는것이고 , 논리적이라는 것은 '사물속에 있는 도리' 이므로 비논리적인 세상의 도리이므로 비논리가 논리가 되겠죠.

-_-;;;;; 계속 횡설수설이네요..

무조건 금상자죠..ㅡ,.ㅡ;;

왜냐면.. 금상자위의 글이 참이라가정하면..은상자위의 글은 믿을것이 못됩니다.
그렇다면 상자위의 글은 금상자든 은상자든어쨋든 못믿을건 마찬가지고
금상자가 그짓이라면 은상자는 참이 될수도 거짓이 될수도 있습니다.
이런상황에서 먼저 문제에서 초상화를 고르면 결혼할수있다는보장도 없고
금상자를 믿어보려하면 어차피 논리에 어긋날뿐만아니라.
제일중요한건 일단 금더비싸니까요..ㅡ,.ㅡ;;

문제에 모순이 있다는 등 여러가지 의견들이 많군요. 많은 공부가 되었습니다.

먼저 비정형적인 방법으로 간단히 이야기해보겠습니다. 이 문제의 '답'을 쉽게 얻기 위해서는 금상자 위의 명제 G에 대해서가 아니라 은상자 위의 명제 S에 대해서 Excluded Middle rule(∀P(prop) · P ∨ ￢P : 이하 'EM')로 refine해야합니다. 즉, S가 참인 경우와 거짓인 경우로 나눠서 생각해보면 G는 양 쪽 경우 중 어느 쪽에서도 참이 될 수 없습니다. 즉, 자체 모순을 피하기 위해서는 어쩔 수 없이 G가 항상 거짓이어야만 한다는 뜻입니다.

정리 증명 과정이란, 비록 complete하지는 못하더라도 최소한 sound함을 기본으로 합니다. 주어진 가정들 사이에 "빼도박도 못하는 모순"이 있다면 그 가정들 자체만으로도 모순이고 그런 가정들로부터 어떤 것을 증명하려는 시도는 ⊥(absurd)-elimination rule에 의해서 무조건 성공합니다. 조금 자연어스럽게 말하자면 모순 → any라는 뜻이죠. (이는 아래에서 소개할 LEGO system에 정의된 실제 absurd_elim의 타입입니다: ⊥ → ∀P(Prop) · P) 반면에, 가정들 사이에 "모순을 피할 수 있는 상황"이 있다면 암묵적으로 그 상황임을 가정하는 것이 기본적인 추론 규칙인 것으로 알고 있습니다.

fibonacci님께서 말씀하신 exclusive-or 연산자가 일반적으로 흔히 하듯이 Prop → Prop → Prop 타입의 함수로 정의되어있다고 가정할 때, 이 함수의 성질(properties)을 살펴보시면 쉽게 알 수 있습니다:

• P ⊕ False ≡ P (항등원)
• P ⊕ P ≡ False (역원)
• P ⊕ True ≡ ￢P

따라서, 명제 G 속에 거꾸로 S가 bound되어있지 않다고 가정할 때 (지금 이 문제의 경우에는 S가 G 속에 등장하지 않으니 통과) S가 G를 이용해서 "G ⊕ S"라고 정의되어 있다면, 비록 S 그 자체는 fibonacci님 말씀대로 이 정의만 가지고 그 진리값을 판별할 수 없지만, 그럼에도 불구하고 이 정의가 의미를 갖기 위해서는 G는 반드시 배타적논리합의 항등원인 False여야만 한다는 뜻입니다.

지금 조금 생소할 수도 있는 ⊕연산이어서 얼핏 거부감부터 들 수도 있는데, 그러면 전혀 거부감이 없을만한 아주 평이한 예를 하나 들겠습니다: 정수의 덧셈 방정식에 관해 생각해봅시다. 만일 어떤 중학교 수학 시험에

물론 여기에는 두 가지 맹점이 있습니다. 첫째, "S와 G ⊕ S의 진리값이 같다, 즉 동치이다"라는 사실과 "S란 G ⊕ S라는 명제다"라는 정의(defiintion)와 "S를 G ⊕ S라고 하겠다"는 선언(declaration)은 모두 전혀 다른 차원의 이야기이며 함부로 서로간에 비약해서 옮겨다니면 안됩니다. 이 부분은 대단히 중요한 문제이지만 애석하게도 제가 타입 시스템의 cumulativity 등 관련 내용에 대한 공력이 부족하여 정확히 말할 수 없으므로 지금은 일단 생략하겠습니다.

또 한가지, S의 진리값이 참인 경우와 거짓인 경우 모두에 대해서 어떤 결론 C를 얻었다고 해서 "항상 C이다"라고 말할 수 있는 것은 어디까지나 classical logic system에서만 가능한 이야기입니다. (우리가 초중고등학교에서 배웠던 논리 체계는 모두 classical logic입니다.) Classical logic system에는 EM rule이 있기 때문에 P의 진리값을 몰라도 P ∨ ￢P가 참이라고 생각하지만, 그렇기 때문에 이 논리 체계에서는 P ∨ ￢P가 참이라는 정형적 증거(formal proof)를 만들어보일 수는 없습니다. 반면에, EM이 없는 constructive logic system (Calculus of Constructions: 이하 'CC')에서 P ∨ ￢P가 참이라고 말하고 싶으면 P가 참이어서 그런지 ￢P가 참이어서 그런지를 분명히 밝혀야만 합니다. 즉, CC로는 이 초상화 문제에서 S가 참인 경우와 거짓인 경우 모두 G가 거짓일 수 밖에 없더라도 'G는 항상 거짓이다'라고 말하지 못하는 것입니다. 즉, 초상화가 금상자에 들어있다는 것을 classical logic system으로 증명할 수는 있지만, 애석하게도 CC 특유의 '정형적 증거'는 만들어보일 수 없는 문제입니다.

비슷한 차원에서, G("이 금상자에는 초상화가 안 들어있지롱"이라는 명제)가 거짓임을 증명하는 문제와 not G가 참임을 증명하는 문제 또한 CC에서는 전혀 다른 이야기입니다. CC에는 EM rule이 없기 때문에 당연히 Reductio Ad Absurdum (reduction to an absurdity, ∀P · (￢￢P) → P : 이하 RAA)도 증명할 수 없습니다. 물론 ∀P · P → ￢￢P 는 쉽게 증명할 수 있습니다. 따라서, CC로는 금상자 위의 명제가 항상 거짓임을 증명한다고 해서 초상화가 금상자에 들어있다고 말하지 못한다는 뜻입니다.

그럼 이제 조금 정형적인 이야기를 해 보겠습니다. 초상화가 금상자에 들어있음을 보이고 싶습니다. 바로 조금 전 단락에서 말한 문제의 복잡성을 피하기 위해, classical logic이라고 가정하고 (EM rule을 강제로 만들어주고) 그냥 "금상자 위의 명제가 거짓임"을 증명하는 것으로 끝내겠습니다. 즉, 지금부터 증명하려는 논리식은 (∀P · P ∨ ￢P) → (∀G∀S · (S ≡ G ⊕ S) → ￢G)입니다.

종이에 natural deduction을 전개할 수도 있지만 실수할 여지도 있거니와 이 게시판에 옮겨쓰기가 고약해서 LEGO라는 증명 보조 도구를 하나 쓰도록 하겠습니다. 지금부터 인용하는 코드는 LEGO 증명 스크립트 파일이 아니라 대화식 증명 환경의 동작을 그대로 옮겨온 것입니다:

먼저 LEGO를 기동합니다:

reeseo@kircheis Lego $ lego
LEGOPATH=.:/usr/lib/lego/lib_Type:/usr/lib/lego

Standard ML with LEGO
Generated  using Standard ML of New Jersey, Version 0.93, February 15, 1993
LEGO 1.3.1
use command 'Help' for info on new commands.
'Qrepl' configured
Extended CC: Initial State!
strong predicative Sigma-types
Lego>

and, or 등의 함수와 이들 중 일부에 대응하는 ∧, ∨ 등의 중위연산자들을 쓰기 위해서 lib_logic 모듈을 불러옵니다:

Lego> Module quiz Import lib_logic;
Including module quiz
(* opening file /usr/lib/lego/lib_Type/lib_logic.o *)
Including module lib_logic
(* opening file /usr/lib/lego/lib_Type/parameters.o *)
Including module parameters
Creating mark "parameters" [/usr/lib/lego/lib_Type/parameters.o]
defn  SET = ... : Type
  (* time= 0.0  gc= 0.0  sys= 0.0 *)
defn  TYPE = ... : Type
  (* time= 0.0  gc= 0.0  sys= 0.0 *)
defn  TYPE_minus1 = ... : TYPE
  (* time= 0.0  gc= 0.0  sys= 0.0 *)

...

defn  Equivalence = ... : {T|SET}(T->T->Prop)->Prop
  (* time= 0.010000  gc= 0.0  sys= 0.0 *)
defn  respect = ... : {T,S|SET}(T->S)->({X|SET}X->X->Prop)->Prop
  (* time= 0.010000  gc= 0.0  sys= 0.0 *)
defn  respect2 = ... : {T,S,U|SET}(T->U->S)->({X|SET}X->X->Prop)->Prop
  (* time= 0.020000  gc= 0.0  sys= 0.0 *)
(* closing file /usr/lib/lego/lib_Type/lib_logic.o; time= 0.530000  gc= 0.010000  sys= 0.020000 *)
(** time since mark "lib_logic": time= 0.530000  gc= 0.010000  sys= 0.020000 **)
Creating mark "quiz" []
Lego>

LEGO는 Extended CC를 위한 goal-driven refinement proof system입니다. 아까 이야기했듯이 CC에는 EM rule이 없으므로, classical logic system의 특성을 얻기 위해서 EM rule을 강제로 선언(declare)해주겠습니다:

Lego> [EM : {P:Prop} P \/ not P];
decl  EM : {P:Prop}(P \/ not P)
  (* time= 0.0  gc= 0.0  sys= 0.0 *)
Lego>

애석하게도 LEGO의 lib_logic에는 xor 연산자가 없(거나 제가 찾지 못했)습니다. 직접 정의(define)해서 쓰겠습니다. (함께 정의하는 xor_elim은 이름 그대로 xor-elimination rule을 만들어두는 것입니다. 증명 과정에서 필요해집니다):

Lego> [xor = [A,B:Prop]{C|Prop}(A->(not B)->C)->((not A)->B->C)->C];
defn  xor = [A,B:Prop]{C|Prop}(A->(not B)->C)->((not A)->B->C)->C
      xor : Prop->Prop->Prop
  (* time= 0.0  gc= 0.0  sys= 0.0 *)
Lego> [xor_elim = [A,B,C|Prop][M: xor A B][N1:A->(not B)->C][N2:(not A)->B->C]M N1 N2];
defn  xor_elim =
  [A,B,C|Prop][M:xor A B][N1:A->(not B)->C][N2:(not A)->B->C]M N1 N2
      xor_elim : {A,B,C|Prop}(xor A B)->(A->(not B)->C)->((not A)->B->C)->C
  (* time= 0.0  gc= 0.0  sys= 0.0 *)
Lego>

자, 이제 LEGO에게 우리의 문제 상황을 이야기해주겠습니다. 먼저 금상자와 은상자 위에 쓰여있는 두 명제 G, S를 각각 선언하겠습니다:

Lego> [G, S: Prop];
decl  G S : Prop
  (* time= 0.0  gc= 0.0  sys= 0.0 *)
Lego>

이제 LEGO에게 알려줄 상황 정보 중 가장 중요한 요소로서, S라는 명제의 내용이 G ⊕ S임을 말해줄 차례입니다. 이 사실을 어떻게 표현할 것인가가 매우 중요한데, 저는 "S와 G ⊕ S가 동치다"라고 말해주는 방식을 택했습니다. 동치성도 복잡한 부분이고 여러가지 동치 개념이 있겠지만, 여기서는 단순히 명제의 진리값 동치를 뜻하므로 "A ≡ B" 를 "(A → B) ∧ (B → A)"라고 풀어서 말했습니다:

Lego> [rule = (S -> xor G S) /\ ((xor G S) -> S)];
defn  rule = S->xor G S /\ (xor G S)->S
      rule : Prop
  (* time= 0.0  gc= 0.0  sys= 0.0 *)
Lego>

이제 사전 준비는 끝났습니다. 증명해야할 목표(goal)를 설정하고 실제로 증명하는 일만 남았습니다. 그럼 무엇을 증명해야 할까요? 지금 제가 증명하고 싶은 것은 "위와 같은 rule 하에서 G는 항상 거짓이다"입니다만, 기왕에 classical logic을 가정했고 문제를 괜히 복잡하게 만들 필요는 없으니 그냥 "위와 같은 rule 하에서 not G가 항상 증명된다"라고 바꾸겠습니다. 만일 이를 증명할 수 있다면 그 proof term(증거)의 이름을 'answer'라고 하겠습니다:

Lego> Goal answer: rule -> not G;
Goal answer
   ?0 : rule->not G
Lego>

이제 LEGO의 proof state로 진입했습니다. 지금 현재 증명해야할 목표는 한 가지이고 그 번호는 0번이며 증명을 위해서 쓸 수 있는 hypothesis는 없습니다. (global assumption인 EM은 곧 쓰게됩니다.) 하지만 일단, "rule"이라고 불리는 놈의 실체를 보면서 증명하는 것이 쉽겠습니다:

Lego> Expand rule;
Expand rule relative to the path []
   ?0 : (S->xor G S /\ (xor G S)->S)->not G
Lego>

goal이 바뀐것은 아니고, 단지 rule이라는 이름을 그 내용으로 환원시킨 것 뿐입니다. 여전히 goal의 main connective는 implication operator고, 역으로 implication-introduction rule을 역행하여 새로운 subgoal과 hyorthesis 하나를 얻겠습니다. (새로 얻게되는 hypothesis의 이름은 '우리의 규칙'이라는 뜻으로 'R'이라고 하겠습니다):

Lego> intros R;
intros (1) R
  R : S->xor G S /\ (xor G S)->S
   ?1 : not G
Lego>

아까 전에 아무런 가정 없이 길다란 0번 goal을 증명해야했던 문제가, 이제 R이라는 이름의 가정 하에 새로운 1번 subgoal인 not G를 증명하는 문제로 바뀌었습니다. 자, 이제 여기서 "S가 참이든 거짓이든 상관 없이 (심지어 알 수 없더라도)"라는 의미를 추가하는 작업을 해봅시다. 이를 위해서는 EM으로 Refine해야합니다:

Lego> Refine EM;
Refine by  EM
   ?2 : Prop
   ?4 : ?2->not G
   ?5 : (not ?2)->not G
Lego> Prf;
  R : S->xor G S /\ (xor G S)->S
   ?2 : Prop
   ?4 : ?2->not G
   ?5 : (not ?2)->not G
Lego>

이제 문제는 3개의 subgoal들을 증명하는 문제로 바뀐 것입니다. 물론 우리의 가정 R도 아직 사라지지 않았습니다. Prf 명령을 통해 현재 가정들과 서브골들을 확인할 수 있습니다. 위에서 2번 서브골은 EM 룰 중 ∀P라는 universal quantification 때문에 나타난 Π-term으로서 어떤 명제 하나를 증거로서 제시하라는 뜻입니다. 지금 우리는 S가 참이든 거짓이든 상관 없는 상황을 만들려는 것이고 그 S라는 명제의 '존재'를 알고 있으므로 2번 서브골은 간단히 증명됩니다:

Lego> Refine S;
Refine by  S
   ?4 : S->not G
   ?5 : (not S)->not G
Lego> Prf;
  R : S->xor G S /\ (xor G S)->S
   ?4 : S->not G
   ?5 : (not S)->not G
Lego>

이제 4번 서브골과 5번 서브골을 모두 증명하면 애초의 규칙 rule 만으로도 S에 관계 없이 항상 not G임을 증명하는 셈입니다. 먼저 4번 서브골에 implication introduction rule을 적용합니다:

Lego> intros Ps;
intros (1) Ps
  Ps : S
   ?6 : not G
Lego>

자, 여기서 한 가지 트릭인데, 사실 not G라는 타입은 함수 타입입니다. (즉, 이 속에 implication이 숨어있습니다) not G라는 것은 실제로는 G → absurd라는 함수 타입의 HNF 형태이고, 이를 다시 갈라치기 위해서 Intros 전략을 씁니다:

Lego> Intros Pg;
Intros (1) Pg
  Pg : G
   ?7 : absurd
Lego> Prf;
  R : S->xor G S /\ (xor G S)->S
  Ps : S
  Pg : G
   ?7 : absurd
Lego>

이제 우리의 문제는 R, Ps, Pg라는 가정 하에 7번 서브골을 증명하고, (현재 스코프는 아니지만 아까 잠시 보았던 대로) R이라는 가정 하에 5번 서브골을 증명하는 문제로 바뀌었습니다. 여기서, 가정 R을 좀 더 효율적으로 사용하기 위해서 fst 함수와 snd 함수를 사용하겠습니다. 각각의 타입과 함수 정의는 다음과 같습니다:

Lego> fst; snd;
value of fst = [A,B|Prop][h:A /\ B]h ([g:A][_:B]g)
type  of fst = {A,B|Prop}(A /\ B)->A
value of snd = [A,B|Prop][h:A /\ B]h ([_:A][g:B]g)
type  of snd = {A,B|Prop}(A /\ B)->B
Lego>

즉, 예를 들어 fst 함수를 가정 R에 적용하면 다음과 같습니다:

Lego> fst R;
value = fst R
type  = S->xor G S
Lego>

fst R의 타입이 S -> xor G S라는 함수 타입이므로, 이 함수를 S 타입의 증거에 적용하면 xor G S가 나올겁니다. 우리는 S 타입의 증거를 local hypothesis로서 가지고 있습니다:

Lego> Prf;
  R : S->xor G S /\ (xor G S)->S
  Ps : S
  Pg : G
   ?7 : absurd
Lego>

따라서 fst R Ps의 타입은 xor G S입니다:

Lego> fst R Ps;
value = fst R Ps
type  = xor G S
Lego>

이제 대망의 xor_elim의 차례가 되었습니다. Natural deduction 상 xor-elimination rule에 해당하며, 함수 정의와 타입은 다음과 같았음을 기억하실겁니다:

Lego> xor_elim;
value of xor_elim =
  [A,B,C|Prop][M:xor A B][N1:A->(not B)->C][N2:(not A)->B->C]M N1 N2
type  of xor_elim = {A,B,C|Prop}(xor A B)->(A->(not B)->C)->((not A)->B->C)->C
Lego>

xor_elim의 첫번째 인수의 타입은 xor P Q입니다. 따라서 이 시점에서 문제를 xor_elim (fst R Ps)로 refine해보면:

Lego> Refine xor_elim (fst R Ps);
Refine by  xor_elim (fst R Ps)
   ?13 : G->(not S)->absurd
   ?14 : (not G)->S->absurd
Lego>

13번 서브골에는 →-introduction을 두 번 적용할 수 있습니다. 각각에 의해 발생해는 두 개의 지역 가정들의 이름은 LEGO가 자동적으로 지정해주는 대로 받아먹도록 하겠습니다:

Lego> intros;
intros (2)
  H : G
  H1 : not S
   ?15 : absurd
Lego> Prf;
  R : S->xor G S /\ (xor G S)->S
  Ps : S
  Pg : G
  H : G
  H1 : not S
   ?15 : absurd
Lego>

새로운 가정 H1의 타입인 not S는 실제로는 S → absurd였음을 상기하시기 바랍니다. 따라서, H1이라는 함수를 S 타입의 증거에 적용하면 absurd 타입에 대한 증거가 됩니다. 즉, 15번 서브골이 증명됩니다!

Lego> Refine H1 Ps;
Refine by  H1 Ps
Discharge..  H1 H
  R : S->xor G S /\ (xor G S)->S
  Ps : S
  Pg : G
   ?14 : (not G)->S->absurd
Lego>

이로서 15번 서브골 트리는 풀렸고, 15번 서브골 가지만의 local-scope hypothesis였던 H와 H1은 discharge되었습니다. 이제 방금 지나쳤던 14번 서브골 차례입니다. 방금 전과 똑같은 과정을 거치면 되지만, 좀 더 간단히 한 방의 refinement로 해결됩니다:

Lego> Refine [x:not G][y:S] x Pg;
Refine by  [x:not G][_:S]x Pg
Discharge..  Pg
Discharge..  Ps
  R : S->xor G S /\ (xor G S)->S
   ?5 : (not S)->not G
Lego>

아예 λx.λy.(x Pg)라는 함수를 만들어서 이것으로 refine해버린 것입니다. 이로서 15번 가지도 풀렸고, 오랜 시간 함께했던 지역가정 Pg와 Ps의 스코프에서 벗어나게되므로 이들도 discharge됩니다. 이제 남은 문제는 5번 서브골을 증명하는 것입니다. 이하로는 자세히 설명하지 않고 곧바로 한꺼번에 증명하겠습니다:

Lego> Intros Ns Pg;
Intros (2) Ns Pg
  Ns : not S
  Pg : G
   ?16 : absurd
Lego> Refine Ns;
Refine by  Ns
   ?17 : S
Lego> Refine snd R;
Refine by  snd R
   ?20 : xor G S
Lego> Prf;
  R : S->xor G S /\ (xor G S)->S
  Ns : not S
  Pg : G
   ?20 : xor G S
Lego> Expand xor;
Expand xor relative to the path []
  R : S->xor G S /\ (xor G S)->S
  Ns : not S
  Pg : G
   ?20 : {C|Prop}(G->(not S)->C)->((not G)->S->C)->C
Lego> intros;
intros (3)
  C | Prop
  H : G->(not S)->C
  H1 : (not G)->S->C
   ?21 : C
Lego> Prf;
  R : S->xor G S /\ (xor G S)->S
  Ns : not S
  Pg : G
  C | Prop
  H : G->(not S)->C
  H1 : (not G)->S->C
   ?21 : C
Lego> Refine H Pg Ns;
Refine by  H Pg Ns
Discharge..  H1 H C
Discharge..  Pg Ns
Discharge..  R
*** QED ***   (* time= 0.070989  gc= 0.001000  sys= 0.010999 *)
Lego>

증명이 끝났습니다. 이제 proof term을 저장하고 그 값을 보겠습니다:

Lego> Save;
"answer"  saved as global, unfrozen
Lego> answer;
value of answer =
  [R:S->xor G S /\ (xor G S)->S]
  EM S
   ([Ps:S][Pg:G]
    xor_elim (fst R Ps) ([_:G][H1:not S]H1 Ps) ([x:not G][_:S]x Pg))
   ([Ns:not S][Pg:G]
    Ns (snd R ([C|Prop][H:G->(not S)->C][_:(not G)->S->C]H Pg Ns)))
type  of answer = rule->not G
Lego>

이 "answer"는 rule → ￢G의 정형적 증거입니다. 비록 classical logic의 힘을 차용하기 위해서 EM rule을 선언하긴 했지만 (위에서 answer 값을 잘 보시면 EM이 들어있습니다), 어쨌든 CC 기반의 증명 시스템으로 이런 증거를 찾았다는 것은 rule → ￢G가 명백히 증명된다는 뜻입니다.

여기서 제 남은 의문은 이런 점입니다: 위 증명 과정에서 사용한 LEGO는 어디까지나 proof assistant일 뿐 자동 증명기가 아닙니다. 그렇다면, G의 정의 속에 S가 등장하지 않는다는 사실과 S가 G ⊕ S로 정의된다는 두 가지 사실로부터 '항상 ￢G'임을 기계적/자동적으로 추론하는 것은 어떻게 하면 가능할까요? 언뜻 생각하기에는 prolog의 backtrack을 사용하면 될 것 같기는 한데, 문제는 prolog가 과연 propositional symbol의 bound 관계와 재귀적 정의를 수용할 수 있을지 의문입니다. 애석하게도 제가 prolog에 대한 공력이 아직 미천하여 이 부분은 당분간 그저 궁금해할 수밖에 없군요. 누군가 prolog나 λ-prolog에 대해서 잘 아시는 분의 고견을 기다립니다.

아울러 이와 관련하여 또 한 가지 마음에 걸리는 점은, 지금 우리가 증명한 논리식 EM → ∀G∀S · (S ≡ G ⊕ S) → ￢G가 과연 주어진 문제의 상황을 제대로 반영하고 있는가 하는 점입니다. 엄밀히 말해서 S는 단지 G ⊕ S로 정의되어있을 뿐이고, 이것을 'S와 G ⊕ S가 동치라면'이라고 말하는 것은 분명히 상당한 비약입니다. 단지 저는 이 비약이 (일종의 weakening으로 보이므로) 충분히 안전하다고 믿고 있는 것 뿐인데, 제 믿음이 잘못되었을 가능성은 충분히 있습니다. 여러분은 이 문제에 대해 어떻게 생각하시는지요?

게다가, ∀G∀S · (S ≡ G ⊕ S) → ￢G이 EM rule 없이는 (즉, 순수한 CC로는) 증명될 수 없다고 신나게 떠들긴 했는데, 어쩌면 단지 제 능력이 부족했을 뿐이고 실제로는 CC로도 증명되는 문제인지도 모릅니다. 제가 정의한 xor 하에서는 아직 EM 없이 증명하는 방법을 찾지 못했는데, 혹시 xor 자체에 EM이나 RAA 등을 추가하지 않고도 위 식을 EM 없이 증명하신 분은 꼭 알려주시기 바랍니다. (물론 제 xor 정의 자체가 틀렸을 가능성은 없어보입니다. 이미 위와 같이 정의된 xor를 가지고 ∀P∀Q · P ⊕ Q ≡ (P ∧ ￢Q) ∨ (￢P ∧ Q)임을 증명했기 때문입니다.)

그 외에도 위 내용을 자세히 읽으시다보면 여기저기에 태클을 걸만한 곳이 적지않게 있으리라 생각합니다. (아직 제 공력이 부족하기 때문입니다. 공부해야할게 산더미입니다. :cry: ) 이런 태클은 제게 피가되고 살이되니 부디 다양하고 적극적인 태클을 부탁드립니다. 그럼 전 이만 야심만만보러~~.

PS: 여담입니다만, 새벽에 재미있는 현상을 하나 발견했습니다. S의 definition 대신 property를 말해줬던 것이 아무래도 마음에 걸려서 Haskell로 S를 '정의'해보았습니다. Hugs의 반응이 재미있군요. 일단 아래 코드는 Quiz.hs라는 간단한 Haskell 코드입니다:

module Quiz (
        Prop (PropTrue, PropFalse),
        propNOT, propOR, propAND, propEquiv, propXOR,
        g, s
) where

data Prop = PropTrue | PropFalse

instance Show Prop where
        show PropTrue   = "T"
        show PropFalse  = "F"

propNOT :: Prop -> Prop
propNOT PropTrue        = PropFalse
propNOT _               = PropTrue

propOR :: Prop -> Prop -> Prop
propOR PropTrue _       = PropTrue
propOR _ y              = y

propAND :: Prop -> Prop -> Prop
propAND PropTrue y      = y
propAND _ _             = PropFalse

propEquiv :: Prop -> Prop -> Prop
propEquiv PropTrue y    = y
propEquiv _ y           = propNOT y

propXOR :: Prop -> Prop -> Prop
propXOR PropTrue y      = propNOT y
propXOR _ y             = y

g :: Prop
g = PropFalse

s :: Prop
s = propXOR g s

Prelude> :l Quiz
Reading file "Quiz.hs":

Hugs session for:
/usr/lib/hugs/lib/Prelude.hs
Quiz.hs
Quiz> :b
s :: Prop
g :: Prop
propXOR :: Prop -> Prop -> Prop
propEquiv :: Prop -> Prop -> Prop
propAND :: Prop -> Prop -> Prop
propOR :: Prop -> Prop -> Prop
propNOT :: Prop -> Prop
PropFalse :: Prop  -- data constructor
PropTrue :: Prop  -- data constructor
Quiz> s
{Interrupted!}

Quiz>

...
g :: Prop
g = PropTrue
...

Quiz> s
Segmentation fault
reeseo@kircheis Haskell $

포샤는 금상자와 은상자를 만들게 하고, 그 가운데 한 상자에 자기 초상화를 넣어 두었으며, 또한 상자의 뚜껑에는 다음과 같은 글을 써 두었습니다

전 말장난을 좋아하는데요... 위 글에서 한 상자에 자기 초상화를 넣고..
다른 상자에는 글을 적었다는것 입니다.
그러므로 상자위에 글을 적지않은 상자에 초상화가 있게 되죠.

금상자 

이 상자 안에는 
초상화가 
들어 있지 않다. 


은상자 

이 두 진술 ( 상자위의 진술) 가운데 
딱 하나만이 
참이다. 

윗글로 유추해 볼때 은상자 위에 글이 적혀 있을것으로 추정되므로
답은 금상자가 될수 있겠네요...

결국 포사의 장난이니깐. 결혼하는건 힘들겠군요. 아마도 맘에 들어야 하지 않을까요.. 컥..

결혼이 쉽지 않군요.
여자친구가 저런 문제 내면 난감하겠습니다.

맞추면 결혼, 아니면 끝...ㅡㅡ
___
Knowing me, knowing you...

'답은 간단히 말해서 두 상자 모두 초상화가 없다'입니다. 두둥

장난기 금상자 은상자

F(초상화) T
T T T(초상화)
T(NULL) F(NULL)

T F(초상화)
F F(NULL) F(NULL)
F(초상화) T

T(NULL) F(NULL)
NULL F(NULL) F(NULL)
F(NULL) T(NULL)

* 결론적으로 저 여자에게 놀아난 가능성이 가장 높다입니다...이만..ㅎㅎㅎ