doc: add Korean translation of chapter 2 quiz

docs/glossary/glossary.txt

@@ -0,0 +1,101 @@
+# Glossary in tab-separated format -*- coding: utf-8 -*-
+St. Anselm	안셀무스
+ontological	존재론적
+argument	논증
+argument	인수
+Lean	린
+Lean community	린 커뮤니티
+God	신
+Alvin Plantinga	앨빈 플랜팅아
+exist	존재하다
+existence	존재
+the understanding	지성
+reality	현실
+assumption	가정
+reductio	귀류법
+great	큰
+premise	전제
+being	존재자
+conceive	생각하다
+definition	정의
+true	참
+true	참인
+false	거짓
+false	거짓인
+formulate	정식화하다
+formulation	정식화
+formalize	형식화하다
+formalization	형식화
+property	속성
+redundant	불필요한
+sentence	문장
+state	진술하다
+statement	진술
+proposition	명제
+negation	부정
+axiom	공리
+theorem	정리
+theory	이론
+conclude	결론하다
+prove	증명하다
+SEP	스탠퍼드 철학 백과사전
+Eric Wieser	에릭 비저
+Alistair Tucker	앨리스터 터커
+philosophy	철학
+Owl of Sogang	서강올빼미
+type theory	유형론
+universe level	유형 세계 변수
+type	유형
+type	입력하다
+type check	유형을 확인하다
+type check	유형이 확인되다
+type check	유형 확인이 잘되다
+type class	유형 클래스
+instance	사례
+category mistake	범주 실수
+class	클래스
+example	보기
+example	예
+inductive type	귀납형
+define	정의하다
+constructor	구성자
+Apache License, Version 2.0	아파치 라이선스, 버전 2.0
+under the terms of	의 조건에 따라
+OmegaT	오메가T
+symbolic link	심벌릭 링크
+directory	디렉터리
+root directory	최상위 디렉터리
+documentation	문서
+English	영어
+Korean	한국어
+chapter	장
+quiz	퀴즈
+question	문제
+command	명령어
+error	오류
+code	코드
+evaluate	계산하다
+keyword	핵심어
+declare	선언하다
+constant	상수
+reference	참고 문헌
+universe-polymorphic	세계 다형적
+parametrically polymorphic	매개 변수 다형적
+function	함수
+identifier	식별자
+definitionally equal	정의상 같은
+natural number	자연수
+input	입력값
+return	반환하다
+non-zero	영이 아닌
+zero	영
+alpha-equivalent	알파 동등한
+less-than-or-equal-to sign	작거나 같음 부호
+dependent function	의존 함수
+dependent function type	의존 함수형
+dependent product	의존곱
+dependent product type	의존곱형
+underscore	밑줄
+implicit	암시적
+explicit	명시적
+sigma type	시그마

docs/ko/notes/chapter03/propositions.md

@@ -0,0 +1,74 @@
+# Propositional Logic
+
+## Propositions
+
+### The Usages of the Term 'Proposition'
+
+> The term ‘proposition’ has a broad use in contemporary philosophy. It is used
+> to refer to some or all of the following: the primary bearers of truth-value,
+> the objects of belief and other “propositional attitudes” (i.e., what is
+> believed, doubted, etc.), the referents of that-clauses, and the meanings of
+> sentences. (McGrath and Frank 2024)
+
+### Propositions in School Mathematics in South Korea
+
+> 문장 ‘2는 소수이다.’는 참이고, 식 ‘`√2 + √3 = √5`’는 거짓이다. 이와 같이 참,
+> 거짓을 명확하게 판별할 수 있는 문장이나 식을 **명제**라고 한다. (전인태 n.d.,
+> 83)
+>
+> The sentence ‘2 is prime’ is true and the expression ‘`√2 + √3 = √5`’ is
+> false. We refer to a sentence or expression whose truth or falsehood can be
+> clearly determined, like these examples, as a *proposition*.
+
+### Questions about Usages of the Term 'Proposition'
+
+#### Is the Sentence 'Bulhwi Cha loves himself' a Proposition?
+
+High school mathematics teachers in South Korea would answer no. On the
+contrary, it seems the authors of the entry "Propositions" in the Stanford
+Encyclopedia of Philosophy (SEP) would answer yes, judging from the following
+quotations:
+
+> E.g., if the proposition that `a` loves `b` is the ordered triple `<loving, a,
+> b>`,
+> it is distinct from the proposition that `b` loves `a`, which would be the ordered
+> triple `<loving, b, a>`. (McGrath and Frank 2024)
+
+> Is the proposition that John loves Mary different from the proposition that
+> Mary is loved by John? (ibid.)
+
+#### Is a Conjecture in Mathematics a Proposition?
+
+Goldbach's conjecture states that every even natural number greater than 2 is
+the sum of two prime numbers. We don't know whether it's true or false as of
+2024, so high school mathematics teachers in South Korea would *have to* answer
+no.
+
+However, the conjecture can be defined as a proposition in the Lean theorem
+prover as follows:
+
+```lean
+import Mathlib.Data.Nat.Prime.Defs
+
+def goldbach_conjecture : Prop :=
+  ∀ n : ℕ, Even n ∧ n > 2 → ∃ p q : ℕ, (Prime p ∧ Prime q) ∧ n = p + q
+```
+
+### My Closing Thoughts
+
+I don't think the usage of the term 'proposition' in Korean high school
+mathematics coincides with those in contemporary philosophy or interactive
+theorem provers like Lean.
+
+One can't clearly determine what the verb phrase 'clearly determine' really
+means, so Korean high school mathematics doesn't make it easier for students to
+understand the notion of a proposition.
+
+## 참고 문헌
+
+* McGrath, Matthew and Devin Frank, "Propositions", *The Stanford Encyclopedia
+of Philosophy* (Fall 2024 Edition), Edward N. Zalta & Uri Nodelman (eds.), URL
+= <https://plato.stanford.edu/archives/fall2024/entries/propositions/>.
+* 전인태, 김동재, 최은아 등. 게재일 불명. “고등학교 공통수학2.” 천재교과서. 2024년 9월 26일에
+마지막으로 접속함.
+<https://view.chunjae.co.kr/streamdocs/view/sd;streamdocsId=BbTgEmTJFvPiML1Vt8UZRczOcmO6rlK3ins3Ux5VOHA>.