저도 Quiz...

nachnine의 이미지

꽤 유명한 Quiz 입니다.

========== 문제 시작 ==========

장난기 가득한 포샤는 남편감을 고르기 위해 다음과 같은 특이한 시험을 합니다.

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

금상자

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

은상자

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

포샤와 결혼하기위해서는 어떤 상자를 골라야 할까요?

========== 문제 끝 ==========

이문제의 이미 풀어 답을 알고 있거나, 논리학에 대해 어느정도 소양이

있지 않은 사람이라면 풀수 없다는데 100원 겁니다

File attachments: 
첨부파일 크기
Image icon jjj55.jpg27.72 KB
kmhh0021의 이미지

금상자.
하나가 참이다라는게 맞다면.. 은 상자가 이미 참이니까.

금상자는 거짓 그래서..

금상자가 답...


-------------------------------------------
피바다=피받아
http://blood.egloos.com
[一笑一少 一怒一老]
[笑門萬福來]

nachnine의 이미지

논리학에 대해 어느정도 소양 이라는 말을

쉽게 보시면 안되요 ^^

sangwoo의 이미지

초상화를 고르면 결혼하게 되는 겁니까?

----
Let's shut up and code.

nachnine의 이미지

상자 열었을때 초상화가 있으면 결혼하는 겁니다.

어떤 걸 골라야 할까요?

결정적힌트 : 장난기

===

꽤 유명한 문제라서 , 이미보셨던 분들이 많을겁니다.

답을 알고 계신분은 리플을 자제해주세요 ^^;

gilsion의 이미지

답 : 은상자
금상자의 진술은 참이고, 은상자의 진술도 참이다. 그러므로 은상자의
진술자체가 거짓이므로 답은 은상자이다.

라고 생각했지만 말이 꼬이는군요.

nachnine의 이미지

처음 풀었을때

논리학적 소양이 있지 않은 사람이

"문제의 풀이 방법을 정확히 제시할" 확률은

감히 5% 이하라 생각합니다.

문제는 간단하지만 풀이가 결코 간단하지 않은 문제입니다.

Prentice의 이미지

그런데 상자에 써져 있는 내용이 모두 참이고, 모순이 없다는 말은 없었잖아요.

논리라는 것은 "가정이 모두 참일 때, 결론이 거짓일 수 없는" 결론도출과정을 의미합니다.

sangwoo의 이미지

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

----
Let's shut up and code.

icanfly의 이미지

아...이런 퀴즈 내지 맙시다.. :evil:

가벼운 기분으로 왔다가 우울하게 돌아갑니다.

오기도 싫어지고.. :cry:

Risty의 이미지

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

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

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

Fe.head의 이미지

금 상자 에 들어 있을 경우

 금상자 : 거짓말 (초상화가들어 있지 않다. )
 은상자 : 진실(둘 중 하나만이 진실)

은 상자에 있을 경우

 금상자 : 진실(초상화가들어 있지 않다. )
 은상자 : 거짓(둘중 하나만이 진실이다.) --> 둘다 거짓이거나 둘다 진실일 경우 임--> 금상자가 진실이므로 은상자도 진실이어야 함 --> 그러나 은상자에 쓰여진 "둘중 하나만이 진실" 말과 모순됨

그러므로 금상자에 들어 있음.

고작 블로킹 하나, 고작 25점 중에 1점, 고작 부활동
"만약 그 순간이 온다면 그때가 네가 배구에 빠지는 순간이야"

neobug의 이미지

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

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

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

futari의 이미지

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

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

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

무한 반복에 빠질 필요는 없을 것 같네요. 그냥 금상자 구라, 은상자 참. 하면 되는거 아닐까요? 둘다 구라.. 해도 금상자가 되지 싶고...

상자 위에 적힌 진술로는 금상자에 초상화가 들어 있다는 이야기인거 같은데,

포샤가 거짓말을 하는지 안하는지를 알수가 없으니 ...

무효 =_=!

뭐 장난기가 많으면 포샤가 거짓말을 했다 치고 은상자 -_-;;

-------------------------
The universe is run by the complex interweaving of three elements: matter, energy, and enlightened self-interest.
- G'kar, Babylon 5

Prentice의 이미지

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

최종호의 이미지

금상자 진술 은상자 진술

1. T T => 오류
2. T F => 오류
3. F T => 오류없음
4. F F => 오류없음

금상자 진술을 A라 하고, 은상자 진술을 B라 하면,

1번 경우는 A가 T가 되고, B도 T라면 결과적으로 (A와 B중 하나만 T라는) B가 F가 되므로 모순,
2번 경우에는 A가 T이고, B가 F라면 결과적으로 B가 T가 되므로 모순,
3번의 경우는, A가 F이고 B가 T 라면 결과적으로 B가 T인 상황이므로 모순없음
4번의 경우는 A가 F이고 B가 F 라면 결과적으로 B가 F이므로 모순 없음.

어떤 경우든지 금상자 진술이 F 인 경우에 오류가 없으므로
금상자를 선택해야 하지 않을까요?

'장난기' 가 힌트라는 것이 이 문제를 푸는데 논리적으로 추가적인 정보를 제공하나요?
있는데 없다고 써 놓은 것이 '장난기'랑 관련이 있긴 하지만,
문제를 푸는데 추가적인 정보를 제공하지는 않는 것 같은데 말이예요.. :cry:

앙마의 이미지

fehead wrote:
금 상자 에 들어 있을 경우
 금상자 : 거짓말 (초상화가들어 있지 않다. )
 은상자 : 진실(둘 중 하나만이 진실)

은 상자에 있을 경우

 금상자 : 진실(초상화가들어 있지 않다. )
 은상자 : 거짓(둘중 하나만이 진실이다.) --> 둘다 거짓이거나 둘다 진실일 경우 임--> 금상자가 진실이므로 은상자도 진실이어야 함 --> 그러나 은상자에 쓰여진 "둘중 하나만이 진실" 말과 모순됨

그러므로 금상자에 들어 있음.

이 분 의견에 한표.

autography

인간에게는 자신의 운명을 거부할 권리가 있다.

neobug의 이미지

### 발전형 ###

if [ $은상자 = True ]
then

	echo "금상자에 초상화가 있다."

elif [ $은상자 = False ]
then

	if [ $금상자 = True -a $은상자 = True ]
	then

		echo "출력될리가 없지...은상자는 False 니까."

	elif [ $금상자 = True -a $은상자 = False ]
	then

		echo "둘 중에 하나는 True 라는 은상자의 진술이 참이 되니까 은상자가 False인 IF 문에서는 무효!"

	elif [ $금상자 = False -a $은상자 = True ]
	then

		echo "아 출려 될리가 없다니까...은상자는 False 니까."

	elif [ $금상자 = False -a $은상자 = False ]
	then

		echo "금상자에 초상화가 있다"

	fi

fi

정 답 : 금상자
근데 포샤 이뻐요?

nachnine의 이미지

지금까지 나온의견

1. 문제가 성립할수 없다. ( 논리로 답이 나오지 않는다 )

2. 금상자다

3. 금상자같은데 장난기가 많다고 했으므로 은상자를 하는게 맞다.

4. 금상자일 확률이 더 높다.

답이 벌써 나왔네요.

nanosec의 이미지

흠.. 제 생각에는 모순 투성이 퀴즈이므로

1. 마음에 드는 남자라면 : 양쪽에 다 넣고, 무조건 찾아내게해 하고, 그쪽 논리로 몰고나가 결혼한다.

2. 마음에 들지않는 남자라면 : 양쪽에 다 넣지않고, 무조건 틀린쪽으로 몰고나가 보내버린다.. 에... ^^;

0x2B | ~0x2B
- Hamlet

앙마의 이미지

nachnine wrote:
지금까지 나온의견

1. 문제가 성립할수 없다. ( 논리로 답이 나오지 않는다 )

2. 금상자다

3. 금상자같은데 장난기가 많다고 했으므로 은상자를 하는게 맞다.

4. 금상자일 확률이 더 높다.

답이 벌써 나왔네요.

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

autography

인간에게는 자신의 운명을 거부할 권리가 있다.

Fe.head의 이미지

nanosec wrote:
흠.. 제 생각에는 모순 투성이 퀴즈이므로

1. 마음에 드는 남자라면 : 양쪽에 다 넣고, 무조건 찾아내게해 하고, 그쪽 논리로 몰고나가 결혼한다.

2. 마음에 들지않는 남자라면 : 양쪽에 다 넣지않고, 무조건 틀린쪽으로 몰고나가 보내버린다.. 에... ^^;

모순은 아닙니다.

분명 문제에

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

이런 문구가 있으므로.. 둘중 하나에는 반드시 초상화가 있어야 맞죠..

고작 블로킹 하나, 고작 25점 중에 1점, 고작 부활동
"만약 그 순간이 온다면 그때가 네가 배구에 빠지는 순간이야"

nanosec의 이미지

fehead wrote:

모순은 아닙니다.

분명 문제에

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

이런 문구가 있으므로.. 둘중 하나에는 반드시 초상화가 있어야 맞죠..

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

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

0x2B | ~0x2B
- Hamlet

atie의 이미지

결혼할 사람의 말을 믿어야죠. 금상자에 없다고 했고 한 곳에 넣었다고 했으니까 저같으면 은상자를 고르겠습니다. 그럼 금상자에 없다고 한말이 맞으니 은상자 위의 말이 맞는거죠. 초상화를 찾았는데 더 논리를 증명할 필요가 있나요?

----
I paint objects as I think them, not as I see them.
atie's minipage

Prentice의 이미지

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

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

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

kjw2048의 이미지

"결혼을 하지 못한다"

상자놀이는 그냥 장난.... -_-; (장난끼 가득하다잖아요;;)

(-_-)/

fibonacci의 이미지

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

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

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

그렇다면 진술 B는

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

순환논법입니다.

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

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

No Pain, No Gain.

앙마의 이미지

정답이랍니다.(http://puzzle.jmath.net/puzzles)

상자에 적혀 있는 문장이 참인지 거짓인지 알 수 없습니다.(피보나치 님 말씀처럼)

따라서 답은, "아무 상자나 고른다"입니다.

autography

인간에게는 자신의 운명을 거부할 권리가 있다.

atie의 이미지

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

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

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


좋은 남편은 머리 굴리지 않고 자기 말을 잘 믿는 사람이라고 포샤는 생각할텐데요. 상대방이 내 말을 믿게 하려면 거짓말 하지 말아야죠.

----
I paint objects as I think them, not as I see them.
atie's minipage

Prentice의 이미지

포샤는 좋은 남편을 얻기를 원합니다.
좋은 남편은 포샤의 말을 잘 믿어주는 사람입니다.
포샤를 잘 믿기 위해서는 포샤가 진실된 태도를 보여야만 합니다.
그러므로 포샤는 진실된 태도를 보입니다.

그러나 포샤가 좋은 남편을 얻기를 원한다는 가정이 참이리라는 보장은 없습니다.

또, 포샤가 퀴즈에서 장난을 친다고 해서 포샤가 불신을 받으리라는 보장도 없습니다.

쿠크다스의 이미지

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

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

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

과자가 아닙니다.
cuckoo dozen, 즉.12마리의 뻐꾸기란 뜻입니다.

atie의 이미지

검은해 wrote:
포샤는 좋은 남편을 얻기를 원합니다.
좋은 남편은 포샤의 말을 잘 믿어주는 사람입니다.
포샤를 잘 믿기 위해서는 포샤가 진실된 태도를 보여야만 합니다.
그러므로 포샤는 진실된 태도를 보입니다.

그러나 포샤가 좋은 남편을 얻기를 원한다는 가정이 참이리라는 보장은 없습니다.

또, 포샤가 퀴즈에서 장난을 친다고 해서 포샤가 불신을 받으리라는 보장도 없습니다.


좋은 남편을 얻기를 원하지 않는 여자와 결혼하는 남자가 가장 똑똑한 남편이라고 할 수는 없죠.
또, 자기에게 장난을 치는지도 구분을 못한다면 역시 가장 똑똑한 남편이라고 할 수 없고요.

----
I paint objects as I think them, not as I see them.
atie's minipage

Prentice의 이미지

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

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

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

Prentice의 이미지

Quote:
상자 열었을때 초상화가 있으면 결혼하는 겁니다.

고른 상자를 연다라든가 상자를 하나만 열수 있다는 얘기도 없으므로 양손으로 하나씩 동시에 열어도 되는 문제 아닐까요..?

그쪽이 장난끼가 있다면 이쪽에서 장난을 걸어보는 것도.. ^^;; (그랬다가 미움받으면 낭패 OTZ)

sjpark의 이미지

Quote:

금상자

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

은상자

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


은상자가 참이라면, 금상자가 거짓이 된다. => 금상자에 초상화

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

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

:roll:

파도의 이미지

포샤가 예쁜가요?

--------Signature--------
시스니쳐 생각 중..

yakkle의 이미지

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

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

nachnine wrote:
포샤는 금상자와 은상자를 만들게 하고, 그 가운데 한 상자에 자기 초상화를 넣어 두었으며,

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

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

===================
slow and steady

Prentice의 이미지

베니스의 상인 원작에 나오는 납상자요? ^^;

bloodntear의 이미지

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

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

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

아 덥다.

비명은 지르지마라 , 달콤한 고통을 음미 못할수 있으니 ... 흐흐흐

kirrie의 이미지

파도 wrote:
포샤가 예쁜가요?

왠지 이게 생각나는 것은;;;

참고로 이건 좀 쉬운 논리 문제입니다. 꼭 논리학 모르시는 분도 차근차근
생각해 보시면 풀 수 있는 문제에요.

이집트에 사는 어느 모자(母子)가 있었습니다. 나일강에는 악어들이 많이 살고
있었는데, 어느 날 아들이 강가에서 놀다가 악어에게 그만 잡히고 말았습니다.
어머니는 발을 동동 구르며 악어에게 사정을 하죠.
"제발 제 아들을 살려주세요.."
악어는 그런 어머니를 보며 장난기가 발동해 다음과 같은 문제를 내면서
만약 이 문제를 맞추면 아들을 살려주겠다고 합니다.
문제는 다음과 같습니다.
"만약 내가 네 아들을 잡아 먹을 건지 잡아 먹지 않을건지 맞춰 보아라."
지혜로운 어머니는 문제를 맞추어 아들을 살려냅니다.
과연 어떻게 답했을까요?

* 악어가 어떻게 말을 하냐.. 란 반론은 미리부터 반사합니다. :twisted:
* 설사 어머니가 문제를 맞췄더라도 악어가 약속을 어기고 아들을 잡아 먹을 수도 있다.. 라는 의견도 미리부터 반사! :twisted: :twisted:

댓글 첨부 파일: 
첨부파일 크기
Image icon 0바이트

--->
데비안 & 우분투로 대동단결!

sjpark의 이미지

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

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

그런 경우의 답도 있나요?

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

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

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

angpoo의 이미지

문제에 문제가 있을때는 문제점을 지적하는게 정답이죠

jachin의 이미지

이런... -_-;;;

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

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

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

angpoo의 이미지

kirrie wrote:
이집트에 사는 어느 모자(母子)가 있었습니다. 나일강에는 악어들이 많이 살고
있었는데, 어느 날 아들이 강가에서 놀다가 악어에게 그만 잡히고 말았습니다.
어머니는 발을 동동 구르며 악어에게 사정을 하죠.
"제발 제 아들을 살려주세요.."
악어는 그런 어머니를 보며 장난기가 발동해 다음과 같은 문제를 내면서
만약 이 문제를 맞추면 아들을 살려주겠다고 합니다.
문제는 다음과 같습니다.
"만약 내가 네 아들을 잡아 먹을 건지 잡아 먹지 않을건지 맞춰 보아라."
지혜로운 어머니는 문제를 맞추어 아들을 살려냅니다.
과연 어떻게 답했을까요?

엄마: 너는 내 아들을 잡아먹을것이다.
악어: 틀렸어! (일단 먹어. 배고프니까)
엄마: 내말이 맞았잖아
악어: 어, 그러네... 미리 말을하지.

alwaysN00b의 이미지

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

결과부터 생각해서

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

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

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

언제나 시작

행복한고니의 이미지

kirrie wrote:
이집트에 사는 어느 모자(母子)가 있었습니다. 나일강에는 악어들이 많이 살고
있었는데, 어느 날 아들이 강가에서 놀다가 악어에게 그만 잡히고 말았습니다.
어머니는 발을 동동 구르며 악어에게 사정을 하죠.
"제발 제 아들을 살려주세요.."
악어는 그런 어머니를 보며 장난기가 발동해 다음과 같은 문제를 내면서
만약 이 문제를 맞추면 아들을 살려주겠다고 합니다.
문제는 다음과 같습니다.
"만약 내가 네 아들을 잡아 먹을 건지 잡아 먹지 않을건지 맞춰 보아라."
지혜로운 어머니는 문제를 맞추어 아들을 살려냅니다.
과연 어떻게 답했을까요?

이건 어디선가 봤던건데... 정답은 "잡아 먹는다".

잡아 먹는다고 했는데, 만약 악어가 아들을 먹으려고 하면 어머니의 말이 맞은 것이므로 먹지 않아야 하는 상황에 빠지게 되죠. 그렇다고 놔주자니 어머니의 말이 틀려서 먹어야 되는데 그럼 앞의 경우에 걸려서 계속 순환하게 되는거죠. 이러지도 저러지도 못하는 상황이...

아... 그리고...
"남자 여자의 차이점" 퍼갑니다.

__________________________________
나는 세상에서 가장 중요한 사람이다.

nachnine의 이미지

논리적으로 해도

금상자가 답이 아닙니다;

아래 리플중에 math/puzzle 링크로 가시면 가장 정확한 설명이 있습니다.

간단하게 설명 드리자면

금상자에 써놓은 말은 " 그냥 포샤가 한 행동에 의한 결과 물 " 일 뿐이지

문제의 내용은 아닙니다.

그 말을 볼 필요가 없다는 말이죠.

( 서술이 모순이라는 것을 고려하지 않으면 필연적으로 금상자라는 답이 나와서 대부분의 사람이 " 답 : 금상자 " 라고 하죠 )

포샤가 초상화를 은상자에 넣고, 그 말을 써 붙일수도 있는것이죠.

( 신기하죠?... )

따라서 답은 랜덤입니다. - 즉 아무상자나 고른다- 가 답입니다.

이 문장은 거짓이다 - 에서 볼수 있듯이

서술이 참도 아니고 거짓도 아닌 "모순" 이라는게 존재하는데,

이걸 꼬아놓아 사람들을 헷갈리게 하는 절묘한 문제입니다.

방준영의 이미지

절묘한 문제가 아니라 엉터리 문제같은데요. :wink: 문제 자체가 모순인데 정답이 있을리가 없죠...

nachnine의 이미지

문제가 모순이 아닙니다.

문제에 등장하는 인물이 써놓은 말이 모순이죠.

" 등장인물이 상자위에 말을 썼다" 는 내용이 나오는건

문제 푸는 사람을

헷갈리게 할려고 한겁니다.

문제의 풀이와는 전혀 상관없는 서술이죠.


제 설명이 부족한거 같은데 , 시간나면 한번 full version 풀이를

보시기 바랍니다.

흠.. 문제 자체가 모순이라고 여기신다면 어차피 안 보시겠군요;

방준영의 이미지

말씀하신 대로 상자 위에 써있는 글귀는 정답과 상관이 없습니다.

실제로 눈을 감은 상태에서 아무 상자나 열었다고 합시다. 그럼 초상화가 나올 확률은 50%에 불과한데, 정답이 "아무 상자나 연다"라니 앞뒤가 안맞잖아요. 따라서 문제 자체가 모순입니다.

결론적으로 "아무 상자나 연다"는 "두 상자 모두 연다"를 한바퀴 꼬아서 표현한 것에 지나지 않습니다. 물론 두 상자 다 열면 반칙이구요.

alwaysN00b의 이미지

저도 댓글을 달았는데

결과부터 생각해보세요

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

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

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

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

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

밑도 끝도 없이

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

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

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

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

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

언제나 시작

alwaysN00b의 이미지

nachnine wrote:
논리적으로 해도

금상자가 답이 아닙니다;

아래 리플중에 math/puzzle 링크로 가시면 가장 정확한 설명이 있습니다.

간단하게 설명 드리자면

금상자에 써놓은 말은 " 그냥 포샤가 한 행동에 의한 결과 물 " 일 뿐이지

문제의 내용은 아닙니다.

그 말을 볼 필요가 없다는 말이죠.

( 서술이 모순이라는 것을 고려하지 않으면 필연적으로 금상자라는 답이 나와서 대부분의 사람이 " 답 : 금상자 " 라고 하죠 )

포샤가 초상화를 은상자에 넣고, 그 말을 써 붙일수도 있는것이죠.

( 신기하죠?... )

따라서 답은 랜덤입니다. - 즉 아무상자나 고른다- 가 답입니다.

이 문장은 거짓이다 - 에서 볼수 있듯이

서술이 참도 아니고 거짓도 아닌 "모순" 이라는게 존재하는데,

이걸 꼬아놓아 사람들을 헷갈리게 하는 절묘한 문제입니다.

full version 풀이를 아직 안봤는데, 글귀 전까지는 모순이 없습니다.
그러므로, 힌트인 글귀를 봐야겠죠.
-_-;;

그건 그렇고... full version 링크가 어딨어요? 못찾겠네.. -_-;; 낭패..

언제나 시작

alwaysN00b의 이미지

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

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

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

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

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

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

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

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

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

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

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

언제나 시작

angpoo의 이미지

단지 이문제만 접한다면 넌센스 이거나 의미 없는 문제 처럼 보일 수 있습니다.

이책의 제목은 무엇인가라는 책을 십년전에 읽었는데 그중에서도 기억에 남는문제 입니다.
책의 중반 이후에 나왔던것으로 기억을 하는데 이문제를 풀때쯤이면 이미 훨씬더 어려운 문제도 많이 풀어본 상태이기 때문에 아주쉽게 답을 내버리는데
그런데 의외의 정답을 보고 한방 먹게 되죠.

꼭 저책을 읽지 않아도 사람에게는 고정관념이라는게 있습니다.
전제 조건이 충분하지 않은데도 나름데로 해석해서 답을 내버리게되는거죠.

참이나 거짓으로 규정을 짓기위한 전제조건이 빠져있으면 참 거짓이라는게 의미가 없다것을 다시한번 생각해보게 하는 문제죠.

- nachnine님이 쓰신 문제를 다시 읽어 보니
상자를 열어보지 말고 고르라는 말이 없으니 둘다 열어보고 골라도 되겠네요.
그런데 초상화가 있는 상자를 고른다고 결혼해준다는 말도 없으니 결혼을 할 수 있을지는 장담할 수가 없군요.

ㅡ,.ㅡ;;의 이미지

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

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


----------------------------------------------------------------------------

alwaysN00b의 이미지

angpoo wrote:

- nachnine님이 쓰신 문제를 다시 읽어 보니
상자를 열어보지 말고 고르라는 말이 없으니 둘다 열어보고 골라도 되겠네요.
그런데 초상화가 있는 상자를 고른다고 결혼해준다는 말도 없으니 결혼을 할 수 있을지는 장담할 수가 없군요.

한표.

언제나 시작

차리서의 이미지

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

먼저 비정형적인 방법으로 간단히 이야기해보겠습니다. 이 문제의 '답'을 쉽게 얻기 위해서는 금상자 위의 명제 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
(단, True와 False는 Boolean 타입이 아닌 Propposition이고 ≡ 는 두 명제의 진리값이 같음을 의미)

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

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

어떤 수학 시험 wrote:
어떤 정수 x와 y에 대해서 y = x + y라고 한다. 그러면 x는?

라는 문제가 나왔다면 (중학교 수학이니까 cardinal number에 대해서는 생각하지 말기로 하고) 별다른 거부감 없이 정수 집합에서의 덧셈에 대한 항등원인 "0"이라고 대답할 것입니다. 물론 위 문제의 식으로부터는 죽었다 깨어나도 y의 값을 알 방법이 없지만, 그렇다고 해서 x가 0이라는 사실을 거부할 사람도, 문제 자체에 모순이 있다고 말할 사람도 거의 없으리라 믿습니다. (생각해보니 x가 0임을 거부할 수 있을만한 구멍들이 한 두 가지 떠오르는데, 나중에 기회가 되면 이런 이야기를 더 해보는 것도 재미있겠습니다.) 아무튼, 상기 덧셈의 예에서와 같은 맥락으로, S ≡ G ⊕ S로부터 G가 명제 집합에서의 xor에 대한 항등원인 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>

(위에서 [ID|Type]은 암묵적 전제, [ID:Type]Term은 λ-abstraction입니다.)

즉, 예를 들어 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

아무래도 명제(proposition)와 bool 타입은 다른 이야기라서 새로 Prop 타입을 정의했고, 보시다시피 g라는 명제를 거짓으로 정의해두었습니다. 이 때 hugs의 반응은 쉽게 예상할 수 있다시피 s의 값을 평가하기위해 무한 재귀에 빠집니다. (스택이 넘칠 때까지 기다려보지는 않고 Ctrl-C로 강제로 멈췄습니다.):
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>

그런데 Quiz.hs에서 g의 정의를 참으로 바꾸고나니:
...
g :: Prop
g = PropTrue
...

s를 평가하라는 명령에 hugs가 사망하셨습니다: :?
Quiz> s
Segmentation fault
reeseo@kircheis Haskell $
[/]

--
자본주의, 자유민주주의 사회에서는 결국 자유마저 돈으로 사야하나보다.
사줄테니 제발 팔기나 해다오. 아직 내가 "사겠다"고 말하는 동안에 말이다!

Prentice의 이미지

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

제가 이런 말을 해도 되는 분위기인지 아닌지 조금 겁이 나지만, 저는 논리는 "가정이 모두 참일 때 결론이 거짓일 수 없는" 결론 도출 과정이라고 배웠습니다.
barbarianmonk의 이미지

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

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

금상자 

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


은상자 

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

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

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

morethan의 이미지

그런데 문제가 뭘까요? :-)

초상화 들어 있는 쪽이면 결혼한다는 겁니까?

nachnine의 이미지

논리적으로도 답은 금상자가 절대로 아닙니다

상자위의 서술은 모순이며, 따라서 아무런 정보도 얻을수 없습니다.

ydongyol의 이미지

답인가요?
그러면 금상자에는 안들어 있고 (and)
은상자에는 들어잇을수도 있고 없을수도 있다(or)??
--
Linux강국 KOREA
http://ydongyol.tistory.com/

--
Linux강국 KOREA
http://ydongyol.tistory.com/

익명사용자의 이미지

아니옵니다 초상화가 들어있는 상자는 그냥 보통 나무 상자이옵니다

착하구나 금상자 은상자 모두 주마

- 포샤와 산신령

ㅡ,.ㅡ;;의 이미지

글쓴지 오래된 문제네요...

아마도 답을 금상자라고 낸거 같은데...

머 이유는 다른분들도 아시는거 같고..

논리적으로 따져보자면 참참 이라가정하면 논리에 어긋나고 참거짓도 어긋나고 거짓참이나 거짓거짓만이 될수 있다는결론이기때문에.

글래서 어찌됐건 금상자진술이 거짓이다..머이런...

그러나..여기엔 함정이 있군요..

은상자에 초상화가 있으면 금상자는참이고 은상자는 참거짓을 따질수 없게되는군요..

즉 은상자는 재귀적으로 자신의말을 재평가해야되는군요..즉결론이 안나죠..ㅎㅎ

이런거나 비슷하죠.. "나는 거짓말(지금이말)을 하고 있다" <= 이말은 참인가 거짓인가..?

어쨋거나.. 말이그렇다는거고..

현실적으론 어디에 들었는지 알수없음..


----------------------------------------------------------------------------

jerry.so의 이미지

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

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

___
Knowing Me, Knowing You...

esrevinu의 이미지

댓글 중에 답이 있을 것 같아서 일단 제가 생각하는 답을 적어보면
금상자입니다.

금상자에 초상화가 있으면 금상자 뚜껑의 진술은 거짓이 되고 은상자 두껑의 진술은 참이면 여전히 참이고, 거짓이면 여전히 거짓이 됩니다. 따라서 모순이 없는 거죠.
은상자에 초상화가 있으면 금상자 뚜껑의 진술은 참이 되고 은상자의 뚜껑의 진술은 참이면 거짓이고, 거짓이면 참이 되어 모순이 발생합니다.

그래서 금상자.

--
foldl (flip (:)) [] "universe"

Vadis의 이미지

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

장난기 금상자 은상자

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)

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

좋은 날 즐거운 날....

leonid의 이미지

상자 위에 써있는 말들이 모순되는지의 여부가

초상화의 위치와 아무런 관련이 없기 때문에

(다시말해.. "상자 위의 글들에 모순이 발생하면 안된다"라는 말이 없으므로)

상자 위의 글들은 초상화를 찾는데 전혀 도움이 되지 않을것 같습니다..