논리 퀴즈: 좋아하는 책
퀴즈 1
불휘는 자신이 좋아하는 부류의 책만 좋아하는 사람에 관한 책만 좋아한다. 보람이 불휘에 관한 책을 쓴다면, 불휘는 그 책을 좋아할까?
퀴즈 2
보람은 자신이 좋아하는 부류의 책만 좋아하지 않는 사람에 관한 책만 좋아한다. 불휘가 보람에 관한 책을 쓴다면, 보람은 그 책을 좋아할까?
저는 논리적 역설을 잘 만들 줄 모르네요. 저녁 먹고 나서 정말 뜬금없이 생각한 문제예요.
불휘는 자신이 좋아하는 부류의 책만 좋아하는 사람에 관한 책만 좋아한다. 보람이 불휘에 관한 책을 쓴다면, 불휘는 그 책을 좋아할까?
보람은 자신이 좋아하는 부류의 책만 좋아하지 않는 사람에 관한 책만 좋아한다. 불휘가 보람에 관한 책을 쓴다면, 보람은 그 책을 좋아할까?
저는 논리적 역설을 잘 만들 줄 모르네요. 저녁 먹고 나서 정말 뜬금없이 생각한 문제예요.
퀴즈 1 : 네. 보람은 보람이 좋아하는 부류의 책만 좋아합니다.
퀴즈 2 : 보람이 그 책(A)을 좋아한다고 합시다. A는 보람에 관한 책이며, 보람이 좋아합니다. 따라서 보람은 보람이 좋아하는 부류의 책만 좋아하지 않는 사람입니다. A는 보람이 좋아하기 때문에 보람은 Q를 좋아하지 않습니다. 이는 모순입니다.
보람이 그 책(A)를 좋아하지 않는다고 합시다. 만약 A가 보람이 좋아하는 부류의 책만 좋아하지 않는 사람에 관한 책이라면, 보람은 A를 좋아해야 합니다. 이는 모순입니다. 따라서 A는 보람이 좋아하는 부류의 책만 좋아하지 않는 것이 아닌 사람에 대한 책입니다. 즉, 보람은 보람이 좋아하는 부류의 책만 좋아하지 않는 것이 아닙니다. 여기는 딱히 모순이 없습니다. 따라서 보람은 그 책을 좋아하지 않습니다.
'보람'을 '불휘'로 전부 바꾸시면 위의 말씀이 맞아요.
Q를 A로 바꾸시면 위의 말씀도 맞아요.
보람이 책 A를 좋아하지 않음을 @aaaa 님이 이미 가정하셨으니, A는 '보람이 좋아하는 부류의 책만 좋아하지 않는 사람에 관한 책'이 아니에요. 이 진술이 다음 진술과 논리적으로 동등한지는 저도 좀 더 생각해 볼게요.
따라서 A는 보람이 좋아하는 부류의 책만 좋아하지 않는 것이 아닌 사람에 대한 책입니다.
위의 진술이 참임을 방금 제가 확인했어요. 다만, "A는 보람이 좋아하는 부류의 책만 좋아하지 않는 사람에 관한 책이 아니다."라는 진술에서 "A는 보람이 좋아하는 부류의 책만 좋아하지 않는 것이 아닌 사람에 대한 책입니다."라는 진술이 어떻게 도출되는지를 더 자세히 설명하셨으면 좋을 듯해요.
퀴즈 1.
형식화: ∀x∀y∀z((Fax∧Axy)→(Fyz→Faz)) // ? ∀x((Wbx∧Axa)→Fax)
(F: …가 책 …을 좋아한다; A: …는 …에 관한 책이다; W: …가 …를 쓴다; a: 불휘; b: 보람)
반례:
F=∅
A=(c, b)
W=(a, c)
반례 검사:
위 모형에서 ∀x∀y∀z((Fax∧Axy)→(Fyz→Faz))는 참이다. 모든 x에 대해 ¬Fax이므로, 어떠한 할당에서도 Fax∧Axy가 거짓임에 따라 (Fax∧Axy)→(Fyz→Faz)가 참이 된다. 반면 ∀x((Wbx∧Axa)→Fax)는 거짓이다. x에 c가 할당될 경우 (Wbx∧Axa)→Fax의 전건은 참이지만, 후건은 거짓이다.
퀴즈 2.
형식화: ∀x∀y∀z((Fbx∧Axy)→(Fyz→¬Fbz)) // ? ∀x((Wax∧Axb)→Fbx)
반례:
F=∅
A=(c, a)
W=(b, c)
이유는 위와 같다.
아무래도 제가 아이패드 미니로 메모하는 걸 멈추고 내일 한번 제 퀴즈를 형식화해 봐야겠네요.
// ? 부분이 무슨 뜻인가요?
임의로 쓴 표현입니다. 저런 종류의 표현이 정식으로 있지는 않다고 압니다. 다만 알고리즘을 mock-code할 때의 관례처럼, 이하 절의 여부를 묻는 표현으로 사용했습니다.
A // ? B: A이다. 그렇다면 B인가?
음, 저런 식은 처음 보네요. 알겠습니다.
“X ?= Y“같은 전산식의 경우가 여기에 해당합니다.
그거도 처음 보네요....
일단 제가 풀이를 린 4로 적긴 했는데, 제 풀이와 여러분의 풀이가 꽤 다르니 나중에 좀 더 자세히 비교할까 해요.
-- this code is written in Lean 4.25.0
class FavoriteBooks (Human : Type u) (Book : Type v) where
Likes : Human → Book → Prop
IsAbout : Book → Human → Prop
isAbout_functional {b : Book} {x y : Human} (h₁ : IsAbout b x) (h₂ : IsAbout b y) : x = y
section
infix:55 " likes " => FavoriteBooks.Likes
infix:55 " is_about " => FavoriteBooks.IsAbout
variable {Human : Type u} {Book : Type u} [FavoriteBooks Human Book]
theorem quiz01
{bulhwi : Human}
(bulhwi_likes : ∀ {b : Book}, bulhwi likes b ↔
∃ (x : Human), b is_about x ∧ ∀ {c : Book}, x likes c ↔ bulhwi likes c)
{boram's_book : Book}
(book_isAbout : boram's_book is_about bulhwi) :
bulhwi likes boram's_book := by
rw [bulhwi_likes]
exists bulhwi
theorem quiz02
{boram : Human}
(boram_likes : ∀ {b : Book}, boram likes b ↔
∃ (x : Human), b is_about x ∧ ∀ {c : Book}, ¬x likes c ↔ boram likes c)
{bulhwi's_book : Book}
(book_isAbout : bulhwi's_book is_about boram) :
¬boram likes bulhwi's_book := by
intro h
rw [boram_likes] at h
let ⟨x, h₁, h₂⟩ := h
have heq : x = boram := FavoriteBooks.isAbout_functional h₁ book_isAbout
subst x
exact not_iff_self (@h₂ bulhwi's_book)
theorem aaaa {boram : Human} {bulhwi's_book : Book} (book_isAbout : bulhwi's_book is_about boram) :
∃ (x : Human), bulhwi's_book is_about x ∧ ¬∀ {c : Book}, ¬x likes c ↔ boram likes c := by
refine ⟨boram, book_isAbout, ?_⟩
intro h
exact not_iff_self (@h bulhwi's_book)
end
그리고 보조사 '만'의 의미도 명확지 않았어요. 앞선 두 퀴즈에서 제가 정확히 표현하지 않은 부분을 고친 결과는 다음과 같아요.
퀴즈에 나온 문장들을 제가 너무 많이 바꿨죠? 죄송합니다. 역시 형식화를 해야 실수가 보이네요.
위의 린 4 코드 중 정리 aaaa를 참고해 주세요.
퀴즈 1
따라서 보람이 오직 불휘만을 다루는 책을 쓴다면, 불휘는 그 책을 좋아한다.
퀴즈1 : 예
퀴즈 2
보람은 자신이 좋아하는 부류의 모든 책을 그리고 그런 책만 좋아하지 않을 수 없다. 만약 가능하다면, 보람이 좋아하는 책은 보람이 좋아하지 않아야 하기 때문이다. 거꾸로 보람이 좋아하지 않는 책은 보람이 좋아하는 책이다. 하나의 책에 모순된 두 성질이 부여되기 때문에 이는 불가능하다.
책의 존재를 가정한 논증이기 때문에, 세상에 책이 없으면 어떻게 되냐고 할 수 있으나, 이는 불휘가 책을 썼기 때문에 책의 존재는 보장된다.
따라서 보람이 좋아하는 책은, 오직 보람만을 다루는 책이 될 수 없다. 따라서 불휘가 쓴 오직 보람만을 다루는 책은 보람이 좋아하지 않는다.
퀴즈 2 : 아니오
제가 논리학은 양화논리를 대충 배워서, 이런 논증을 기호화해서 보이고 싶은데 어떻게 공부하면 좋을까요?
제가 바빠서 답장이 늦어지고 있네요. 내일 오전에 글을 쓸게요!
오늘 오후에야 제가 글을 쓰고 있네요. 린 코드는 이항관계 IsAbout의 이름을 IsOnlyAbout으로 바꾸기만 하면 되더군요. 그 밖에는 고칠 부분이 없었어요. 다음 링크를 참고해 주세요.
https://paste.sr.ht/~chabulhwi/dfcedb2df9e5fd8ea8eec349c96b40595c62c166
위의 풀이에 나온 두 진술은 각각 다음과 같이 형식화할 수 있어요.
1번 진술은 2번 진술을 이끌어 내는 데 필요하지 않아요. 2번 진술을 증명하는 데는 1번 진술 말고 다음 가정을 이용하셔야 해요. 이 가정은 제가 퀴즈에서 제시했어요.
∀b (bulhwi likes b ↔ ∃x [b is only about x ∧ ∀c (x likes c ↔ bulhwi likes c)])
린 증명 보조기로 형식화한 정리의 진술과 그 증명은 다음과 같아요.
theorem aaaa01 {bulhwi : Human} : ∀ {b : Book}, bulhwi likes b ↔ bulhwi likes b :=
Iff.rfl
theorem aaaa02
{bulhwi : Human}
(bulhwi_likes : ∀ {b : Book}, bulhwi likes b ↔
∃ (x : Human), b is_only_about x ∧ ∀ {c : Book}, x likes c ↔ bulhwi likes c) :
∀ {b : Book}, b is_only_about bulhwi → bulhwi likes b := by
intro b hb
rw [bulhwi_likes]
exists bulhwi
각 증명 단계의 순서만 고치시면 좋을 듯해요. 보람이 책 b를 좋아하고, 책 b가 오직 보람만을 다룬다고 가정하면 거기서 다음 진술을 이끌어 낼 수 있어요.
보람은 자신이 좋아하는 부류의 모든 책을 그리고 그런 책만 좋아하지 않는다.
이는 모순이므로 다음 결론이 나오죠.
보람이 좋아하는 모든 책은 오직 보람만을 다루는 책이 아니다.
명제 논리와 양화 논리를 주로 다루는 형식 논리학 교재를 정독하고 연습 문제를 푸시길 추천해요.