diff --git a/docs/glossary/glossary.txt b/docs/glossary/glossary.txt index acfce2a..66fb794 100644 --- a/docs/glossary/glossary.txt +++ b/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 …일 때 그리고 그럴 때만 diff --git a/docs/ko/notes/chapter03/propositional-connectives.md b/docs/ko/notes/chapter03/propositional-connectives.md new file mode 100644 index 0000000..3ef3ea3 --- /dev/null +++ b/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`, 동등에 대한 역방향 긍정 논법) diff --git a/docs/omegat/project_save.tmx b/docs/omegat/project_save.tmx index 77c1459..e93f4bb 100644 --- a/docs/omegat/project_save.tmx +++ b/docs/omegat/project_save.tmx @@ -4,6 +4,111 @@
+ + + (<g1>False.elim</g1>, also known as <g2>ex falso quodlibet (EFQ)</g2> or <g3>the principle of +explosion</g3>) + + + [<g1>False.elim</g1>, <g2>엑스 팔소 세퀴투르 쿠오들리베트(ex falso quodlibet, EFQ)</g2> 또는 <g3>폭발 원리</g3>] + + + + + (<g2>True.intro</g2>) + + + (<g2>True.intro</g2>) + + + + + (<g3>And.left</g3>) + + + (<g3>And.left</g3>) + + + + + (<g3>And.right</g3>) + + + (<g3>And.right</g3>) + + + + + (<g3>Iff.mp</g3>, modus ponens for iff) + + + (<g3>Iff.mp</g3>, 동등에 대한 긍정 논법) + + + + + (<g3>Iff.mpr</g3>, reversed modus ponens for iff) + + + (<g3>Iff.mp</g3>, 동등에 대한 역방향 긍정 논법) + + + + + (<g3>Or.inl</g3>) + + + (<g3>Or.inl</g3>) + + + + + (<g3>Or.inr</g3>) + + + (<g3>Or.inr</g3>) + + + + + (<g3>refutation by contradiction</g3>) + + + (<g3>모순에 따른 부인</g3>) + + + + + (<g4>And.intro</g4>) + + + (<g4>And.intro</g4>) + + + + + (<g4>Iff.intro</g4>) + + + (<g4>Iff.intro</g4>) + + + + + (<g4>modus ponens</g4>) + + + (<g4>긍정 논법[모더스 포넨스]</g4>) + + + + + (<g5>Or.elim</g5>, also known as <g6>proof by cases</g6>) + + + (<g5>Or.elim</g5>, <g6>경우에 따른 증명</g6>) + + (McGrath and Frank 2024) @@ -68,6 +173,54 @@ end Question34 <g1>fun (s : String) (n : Nat) ↦ String.drop s n</g1> + + + <g1>p → q</g1> follows from <g2>p ↔ q</g2>. + + + <g2>p ↔ q</g2>에서 <g1>p → q</g1>가 도출된다. + + + + + <g1>p ∨ q</g1> follows from <g2>p</g2>. + + + <g2>p</g2>에서 <g1>p ∨ q</g1>가 도출된다. + + + + + <g1>p ∨ q</g1> follows from <g2>q</g2>. + + + <g2>q</g2>에서 <g1>p ∨ q</g1>가 도출된다. + + + + + <g1>p</g1> follows from <g2>p ∧ q</g2>. + + + <g2>p ∧ q</g2>에서 <g1>p</g1>가 도출된다. + + + + + <g1>q → p</g1> follows from <g2>p ↔ q</g2>. + + + <g2>p ↔ q</g2>에서 <g1>q → p</g1>가 도출된다. + + + + + <g1>q</g1> follows from <g2>p ∧ q</g2>. + + + <g2>p ∧ q</g2>에서 <g1>q</g1>가 도출된다. + + <x1/> @@ -217,6 +370,30 @@ same? 2장 퀴즈 + + + Conjunction + + + 연언 + + + + + Contraposition: <g1>¬q → ¬p</g1> is the contraposition of the implication <g2>p → q</g2>. + + + 대우(對偶): <g1>¬q → ¬p</g1>는 함의 <g2>p → q</g2>의 대우이다. + + + + + Conversion: <g1>q → p</g1> is the converse of the implication <g2>p → q</g2>. + + + 역: <g1>q → p</g1>는 함의 <g2>p → q</g2>의 역이다. + + Define a constant of each type listed below. @@ -261,6 +438,22 @@ identifier with an actual definition. 각 <g1>sorry</g1> 식별자를 실제 정의로 바꿔 다음의 두 세계 다형적 함수를 정의하라. + + + Definition in Lean: <g1>¬p</g1> is defined to be <g2>p → False</g2>. + + + 린에서의 정의: <g1>¬p</g1>는 <g2>p → False</g2>로 정의된다. + + + + + Disjunction + + + 선언 + + E.g., if the proposition that <g1>a</g1> loves <g2>b</g2> is the ordered triple <g3><loving, a, @@ -272,6 +465,62 @@ triple <g6><loving, b, a></g6>. 예를 들어, <g1>a</g1>가 <g2>b</g2>를 사랑한다는 명제가 순서세짝 <g3><사랑함, a, b></g3>라면, <g4>b</g4>가 <g5>a</g5>를 사랑한다는 명제는 순서세짝 <g6><사랑함, b, a></g6>이 될 것이고, 이 두 명제는 별개이다. + + + Elimination rule: <g1>q</g1> follows from <g2>p</g2> and <g3>p → q</g3>. + + + 제거 규칙: <g2>p</g2>와 <g3>p → q</g3>에서 <g1>q</g1>가 도출된다. + + + + + Elimination rule: <g1>r</g1> follows from <g2>p ∨ q</g2>, <g3>p → r</g3>, and <g4>q → r</g4>. + + + 제거 규칙: <g2>p ∨ q</g2>, <g3>p → r</g3>, <g4>q → r</g4>에서 <g1>r</g1>가 도출된다. + + + + + Elimination rule: a contradiction follows from <g1>p</g1> and <g2>¬p</g2>. + + + 제거 규칙: <g1>p</g1>와 <g2>¬p</g2>에서 모순이 도출된다. + + + + + Elimination rule: any proposition follows from a contradiction. + + + 제거 규칙: 모순에서 임의의 명제가 도출된다. + + + + + Elimination rules + + + 제거 규칙 + + + + + Equivalence + + + 동등 + + + + + Falsity + + + 거짓 + + Fix the definition of the dependent @@ -418,6 +667,70 @@ theorem provers like Lean. 저는 한국 고등학교 수학에서 '명제' 용어가 쓰이는 방법이 동시대 철학에서의 용법이나 린 같은 상호 작용 정리 증명기에서의 용법과 일치한다고 생각하지 않습니다. + + + Implication + + + 함의 + + + + + Introduction rule: <g1>True</g1> is true. + + + 도입 규칙: <g1>True</g1>는 참이다. + + + + + Introduction rule: <g1>p ↔ q</g1> follows from <g2>p → q</g2> and <g3>q → p</g3>. + + + 도입 규칙: <g2>p → q</g2>와 <g3>q → p</g3>에서 <g1>p ↔ q</g1>가 도출된다. + + + + + Introduction rule: <g1>p ∧ q</g1> follows from <g2>p</g2> and <g3>q</g3>. + + + 도입 규칙: <g2>p</g2>와 <g3>q</g3>에서 <g1>p ∧ q</g1>가 도출된다. + + + + + Introduction rule: if <g1>q</g1> follows from <g2>p</g2>, then <g3>p → q</g3> holds. + + + 도입 규칙: <g2>p</g2>에서 <g1>q</g1>가 도출되면, <g3>p → q</g3>가 성립한다. + + + + + Introduction rule: if a contradiction follows from <g1>p</g1>, then <g2>¬p</g2> holds. + + + 도입 규칙: <g1>p</g1>에서 모순이 도출되면, <g2>¬p</g2>가 성립한다. + + + + + Introduction rules + + + 도입 규칙 + + + + + Inversion: <g1>¬p → ¬q</g1> is the inverse of the implication <g2>p → q</g2>. + + + 이(裏): <g1>¬p → ¬q</g1>는 함의 <g2>p → q</g2>의 이이다. + + Is Goldbach's Conjecture a Proposition? @@ -541,6 +854,52 @@ of Philosophy</g1> (Fall 2024 Edition), Edward N. Zalta & Uri Nodelman = <x2/>. + + + Meaning: given <g1>p : Prop</g1>, the proposition <g2>¬p</g2> stands for "It is not the case +that <g3>p</g3>." + + + 뜻: <g1>p : Prop</g1>가 주어져 있을 때, 명제 <g2>¬p</g2>는 "<g3>p</g3>가 아니다."라는 뜻이다. + + + + + Meaning: given <g1>p q : Prop</g1>, the proposition <g2>p → q</g2> stands for "If <g3>p</g3>, then +<g4>q</g4>." + + + 뜻: <g1>p q : Prop</g1>가 주어져 있을 때, 명제 <g2>p → q</g2>는 "<g3>p</g3>이면 <g4>q</g4>이다."라는 뜻이다. + + + + + Meaning: given <g1>p q : Prop</g1>, the proposition <g2>p ↔ q</g2> stands for "<g3>p</g3> if and +only if <g4>q</g4>" (often abbreviated as "<g5>p</g5> iff <g6>q</g6>"). + + + 뜻: <g1>p q : Prop</g1>가 주어져 있을 때, 명제 <g2>p ↔ q</g2>는 "<g3>p</g3>일 때 그리고 그럴 때만 <g4>q</g4>이다."(흔히 "<g5>p</g5> iff <g6>q</g6>"라고 축약함)라는 뜻이다. + + + + + Meaning: given <g1>p q : Prop</g1>, the proposition <g2>p ∧ q</g2> stands for "Both <g3>p</g3> and +<g4>q</g4>." + + + 뜻: <g1>p q : Prop</g1>가 주어져 있을 때, 명제 <g2>p ∧ q</g2>는 "<g3>p</g3>이고 <g4>q</g4>이다."라는 뜻이다. + + + + + Meaning: given <g1>p q : Prop</g1>, the proposition <g2>p ∨ q</g2> stands for "Either <g3>p</g3> or +<g4>q</g4>." + + + 뜻: <g1>p q : Prop</g1>가 주어져 있을 때, 명제 <g2>p ∨ q</g2>는 "<g3>p</g3>이거나 +<g4>q</g4>이다."라는 뜻이다. + + My Closing Thoughts @@ -549,6 +908,128 @@ of Philosophy</g1> (Fall 2024 Edition), Edward N. Zalta & Uri Nodelman 제 결론 + + + Name in Lean: <g1>And</g1> + + + 린에서의 이름: <g1>And</g1> + + + + + Name in Lean: <g1>False</g1> + + + 린에서의 이름: <g1>False</g1> + + + + + Name in Lean: <g1>Iff</g1> (abbreviation of "if and only if") + + + 린에서의 이름: <g1>Iff</g1> ['…일 때 그리고 그럴 때만(if and only if)'의 준말] + + + + + Name in Lean: <g1>Not</g1> + + + 린에서의 이름: <g1>Not</g1> + + + + + Name in Lean: <g1>Or</g1> + + + 린에서의 이름: <g1>Or</g1> + + + + + Name in Lean: <g1>True</g1> + + + 린에서의 이름: <g1>True</g1> + + + + + Names: conjunction, logical and + + + 이름: 연언, 논리적 AND, 논리곱 + + + + + Names: disjunction, logical or + + + 이름: 선언(選言), 논리적 OR, 논리합 + + + + + Names: equivalence, logical biconditional, material biconditional + + + 이름: 동등, 논리적 쌍조건문, 내용적 쌍조건문 + + + + + Names: falsity, false proposition, empty proposition + + + 이름: 거짓, 거짓 명제 + + + + + Names: implication, material implication, material conditional, logical +conditional + + + 이름: 함의, 내용적 함의, 내용적 조건문, 논리적 조건문 + + + + + Names: negation, logical not + + + 이름: 부정, 논리적 NOT + + + + + Names: truth, true proposition + + + 이름: 참, 참 명제 + + + + + Necessary condition: <g1>p → q</g1> also stands for "<g2>p</g2> only if <g3>q</g3>," that is, <g4>q</g4> +is a necessary condition for <g5>p</g5> to be true. + + + 필요조건: <g1>p → q</g1>는 "<g3>q</g3>일 때만 <g2>p</g2>이다."라는 뜻, 다시 말해 <g4>q</g4>는 <g5>p</g5>가 참이기 위한 필요조건이라는 뜻이다. + + + + + Negation + + + 부정 + + Note that you can type the less-than-or-equal-to sign <g1>≤</g1> with <g2>\le</g2>. @@ -557,6 +1038,14 @@ of Philosophy</g1> (Fall 2024 Edition), Edward N. Zalta & Uri Nodelman 작거나 같음 부호 <g1>≤</g1>는 <g2>\le</g2>로 입력할 수 있음을 유념하라. + + + Notes on Implication + + + 함의에 관한 첨언 + + On the @@ -579,11 +1068,19 @@ understand the notion of a proposition. "명확하게 판별하다"라는 동사구가 무슨 뜻인지는 명확하게 판별할 수 없습니다. 그래서 한국 고등학교 수학에서의 명제 개념은 학생들이 이해하기 더 쉽지 않습니다. + + + Propositional Connectives + + + 명제 연결사 + + Propositional Logic - + 명제 논리 @@ -932,6 +1429,62 @@ then check the value of each expression. 아래에 나열된 식에 있는 밑줄을 각각 적절한 유형으로 바꾼 다음, 그 식의 값을 확인하라. + + + Rule of inference + + + 추론 규칙 + + + + + Rules of inference + + + 추론 규칙 + + + + + Symbol: <g1>¬</g1> (read as "not") + + + 기호: <g1>¬</g1> ["낫(not)"이라고 읽음] + + + + + Symbol: <g1>→</g1> (read as "implies") + + + 기호: <g1>→</g1> ("함의"라고 읽음) + + + + + Symbol: <g1>↔</g1> (read as "if and only if") + + + 기호: <g1>↔</g1> ("동등" 또는 "쌍조건문"이라고 읽음) + + + + + Symbol: <g1>∧</g1> (read as "and") + + + 기호: <g1>∧</g1> ["앤드(and)" 또는 "그리고"라고 읽음] + + + + + Symbol: <g1>∨</g1> (read as "or") + + + 기호: <g1>∨</g1> ["오어(or)"라고 읽거나 "또는"이라고 읽음] + + The Usages of the Term 'Proposition' @@ -975,6 +1528,22 @@ false. 다음 코드에 오류가 있다. + + + Truth + + + 참 + + + + + Truth and Falsity + + + 참과 거짓 + + Use the <g1>#check</g1> command to give the type of each expression listed below.