doc: translate propositional-connectives.md

Add the Korean translation of the note about propositional connectives.

docs/glossary/glossary.txt

@@ -118,3 +118,28 @@ ordered triple	순서세짝
 conjecture	추측
 Goldbach's conjecture	골드바흐의 추측
 interactive theorem prover	상호 작용 정리 증명기
+truth	참
+falsity	거짓
+rule of inference	추론 규칙
+introduction rule	도입 규칙
+elimination rule	제거 규칙
+ex falso quodlibet	엑스 팔소 세퀴투르 쿠오들리베트
+principle of explosion	폭발 원리
+propositional connective	명제 연결사
+symbol	기호
+refutation by contradiction	모순에 따른 부인
+contradiction	모순
+conjunction	연언
+disjunction	선언(選言)
+implication	함의
+material implication	내용적 함의
+conditional	조건문
+modus ponens	긍정 논법[모더스 포넨스]
+necessary condition	필요조건
+conversion	역
+inversion	이(裏)
+contraposition	대우(對偶)
+equivalence	동등
+biconditional	쌍조건문
+abbreviation	준말
+if and only if	…일 때 그리고 그럴 때만

docs/ko/notes/chapter03/propositional-connectives.md

@@ -0,0 +1,86 @@
+# 명제 논리
+
+## 참과 거짓
+
+### 참
+
+* 이름: 참, 참 명제
+* 린에서의 이름: `True`
+* 추론 규칙
+  - 도입 규칙: `True`는 참이다. (`True.intro`)
+
+### 거짓
+
+* 이름: 거짓, 거짓 명제
+* 린에서의 이름: `False`
+* 추론 규칙
+  - 제거 규칙: 모순에서 임의의 명제가 도출된다.
+  [`False.elim`, *엑스 팔소 세퀴투르 쿠오들리베트(ex falso quodlibet, EFQ)* 또는 *폭발 원리*]
+
+## 명제 연결사
+
+### 부정
+
+* 이름: 부정, 논리적 NOT
+* 린에서의 이름: `Not`
+* 기호: `¬` ["낫(not)"이라고 읽음]
+* 뜻: `p : Prop`가 주어져 있을 때, 명제 `¬p`는 "`p`가 아니다."라는 뜻이다.
+* 린에서의 정의: `¬p`는 `p → False`로 정의된다.
+* 추론 규칙
+  - 도입 규칙: `p`에서 모순이 도출되면, `¬p`가 성립한다.
+  (*모순에 따른 부인*)
+  - 제거 규칙: `p`와 `¬p`에서 모순이 도출된다.
+
+### 연언
+
+* 이름: 연언, 논리적 AND, 논리곱
+* 린에서의 이름: `And`
+* 기호: `∧` ["앤드(and)" 또는 "그리고"라고 읽음]
+* 뜻: `p q : Prop`가 주어져 있을 때, 명제 `p ∧ q`는 "`p`이고 `q`이다."라는 뜻이다.
+* 추론 규칙
+  - 도입 규칙: `p`와 `q`에서 `p ∧ q`가 도출된다. (`And.intro`)
+  - 제거 규칙
+    + `p ∧ q`에서 `p`가 도출된다. (`And.left`)
+    + `p ∧ q`에서 `q`가 도출된다. (`And.right`)
+
+### 선언
+
+* 이름: 선언(選言), 논리적 OR, 논리합
+* 린에서의 이름: `Or`
+* 기호: `∨` ["오어(or)"라고 읽거나 "또는"이라고 읽음]
+* 뜻: `p q : Prop`가 주어져 있을 때, 명제 `p ∨ q`는 "`p`이거나
+`q`이다."라는 뜻이다.
+* 추론 규칙
+  - 도입 규칙
+    + `p`에서 `p ∨ q`가 도출된다. (`Or.inl`)
+    + `q`에서 `p ∨ q`가 도출된다. (`Or.inr`)
+  - 제거 규칙: `p ∨ q`, `p → r`, `q → r`에서 `r`가 도출된다.
+  (`Or.elim`, *경우에 따른 증명*)
+
+### 함의
+
+* 이름: 함의, 내용적 함의, 내용적 조건문, 논리적 조건문
+* 기호: `→` ("함의"라고 읽음)
+* 뜻: `p q : Prop`가 주어져 있을 때, 명제 `p → q`는 "`p`이면 `q`이다."라는 뜻이다.
+* 추론 규칙
+  - 도입 규칙: `p`에서 `q`가 도출되면, `p → q`가 성립한다.
+  - 제거 규칙: `p`와 `p → q`에서 `q`가 도출된다. (*긍정 논법[모더스 포넨스]*)
+
+#### 함의에 관한 첨언
+
+* 필요조건: `p → q`는 "`q`일 때만 `p`이다."라는 뜻, 다시 말해 `q`는 `p`가 참이기 위한 필요조건이라는 뜻이다.
+* 역: `q → p`는 함의 `p → q`의 역이다.
+* 이(裏): `¬p → ¬q`는 함의 `p → q`의 이이다.
+* 대우(對偶): `¬q → ¬p`는 함의 `p → q`의 대우이다.
+
+### 동등
+
+* 이름: 동등, 논리적 쌍조건문, 내용적 쌍조건문
+* 린에서의 이름: `Iff` ['…일 때 그리고 그럴 때만(if and only if)'의 준말]
+* 기호: `↔` ("동등" 또는 "쌍조건문"이라고 읽음)
+* 뜻: `p q : Prop`가 주어져 있을 때, 명제 `p ↔ q`는 "`p`일 때 그리고 그럴 때만 `q`이다."(흔히 "`p` iff `q`"라고 축약함)라는 뜻이다.
+* 추론 규칙
+  - 도입 규칙: `p → q`와 `q → p`에서 `p ↔ q`가 도출된다. (`Iff.intro`)
+  - 제거 규칙
+    + `p ↔ q`에서 `p → q`가 도출된다. (`Iff.mp`, 동등에 대한 긍정 논법)
+    + `p ↔ q`에서 `q → p`가 도출된다. (`Iff.mp`, 동등에 대한 역방향 긍정 논법)