이산수학(Discrete Mathematics)  증명 전략 (Proof Strategy) 2012년 봄학기 강원대학교 컴퓨터과학전공 문양세

Proof Strategy (review “Methods of Proof”) Sequences and Summations Overview 3.1 Proof Strategy Proof Strategy (review “Methods of Proof”) Sequences and Summations Mathematical Induction Recursive Definitions and Structural Induction Recursive Algorithms

추론 규칙(rules of inference) 용어(Terminology) (1/3) 3.1 Proof Strategy 정리(theorem) 정리란 참(true)으로 밝혀진 명제이다. A statement that has been proven to be true. 공리(axiom, postulates) 증명된 정리 혹은 증명하고자 하는 정리의 가정/명제이다. (증명이 불필요한) Assumptions (often unproven) defining the structures about which we are reasoning. (예: n이 짝수라면 n = 2k라 나타낼 수 있다.) 추론 규칙(rules of inference) 논리적으로 유효한 주장(logically valid deductions)을 사용하여, 가정을 결론으로 이끌어가는 증명의 과정이다. Patterns of logically valid deductions from hypotheses to conclusions.

용어(Terminology) (2/3) 보조정리(lemma) 따름정리(corollary) 3.1 Proof Strategy 보조정리(lemma) 다른 정리를 증명하는데 사용하는 간단한 정리이다. A minor theorem used as a stepping-stone to proving a major theorem. “복잡한 내용이 정리이고, 간단한 내용이 보조정리”를 의미하는 것은 아님에 유의! 따름정리(corollary) 어떤 정리가 증명되면, 이에 의하여 자연스럽게 증명되는 정리이다. A minor theorem proved as an easy consequence of a major theorem.

용어(Terminology) (3/3) 가설(conjecture) 이론(theory) 3.1 Proof Strategy 가설(conjecture) 증명되지는 않았지만 참으로 믿어지는 명제이다. A statement whose truth values has not been proven. (A conjecture may be widely believed to be true, regardless.) 이론(theory) 주어진 공리(axiom)으로부터 증명이 가능한 모든 정리(theorem)의 집합이다. The set of all theorems that can be proven from a given set of axioms.

추론 규칙 (Inference Rules) (1/2) 3.1 Proof Strategy 추론 규칙의 의미 주어진 가정(antecedent)이 참(true)일 때, 결론(consequent)가 참이라는 패턴 “x = 3”(= p)이면, “x + 1 = 4”(= q)이다. 상기 예에서 p(가정)가 참이면, q(결론)은 참이 된다. 추론 규칙의 표기 antecedent 1 antecedent 2 … 가정  consequent 결론 “”은 “therefore”를 의미한다.

추론 규칙 (Inference Rules) (2/2) 3.1 Proof Strategy 각 추론 규칙은 “항진 명제인 함축(implication)”에 해당한다. ant.1 ant.2 …  con. 에 해당하는 tautology는 “((ant.1  ant.2  … )  con.”이다.

추론 규칙 종류 Rule of inference Tautology Name p  p  q p  (p  q) 3.1 Proof Strategy Rule of inference Tautology Name p  p  q p  (p  q) Addition p  q  p (p  q)  p Simplification q  p  q ((p)  (q))  (p  q) Conjunction p  q  q (p  (p  q))  q Modus ponens (긍정논법) (the mode of affirming) ¬q  ¬p (¬q  (p  q))  ¬p Modus tollens (부정논법) (the mode of denying) q  r  p  r ((p  q)  (p  r))  (p  r) Hypothetical syllogism p  q ¬p ((p  q)  ¬p)  q Disjunctive syllogism ¬p  r  q  r ((p  q)  (¬p  r))  (q  r) Resolution

Formal Proofs Format Proof의 정의 예제 6 (in $1.5) 3.1 Proof Strategy Format Proof의 정의 Formal proof란 주어진 가정(antecedent)에 기반하여 추론 규칙을 적용한 일련의 단계(step)를 거쳐서 결론(consequent)을 도출하는 과정이다. 증명(proof)은 주어진 모든 가정이 true일 때 결론이 true임을 보이는 과정이다. 예제 6 (in $1.5) 다음 가정이 “We will be home by sunset.”이라는 결론을 도출함을 보여라. “It is not sunny this afternoon and it is colder than yesterday.” “If we will go swimming, then it is sunny this afternoon.” “If we do not go swimming, then we will take a canoe trip.” “If we take a canoe trip, then we will be home by sunset.” 풀이 p = “It is sunny this afternoon.” q = “It is colder than yesterday.” r = “We will go swimming.” s = “We will take a canoe trip.” t = “We will be home by sunset.” 단계 과정 이유 1 ¬p  q 가정 2 ¬p 단계 1의 simplification 3 r  p 4 ¬r 단계 2, 3 기반의 Modus tollens 5 ¬r  s 6 s 단계 4, 5 기반의 Modus ponens 7 s  t 8 t 단계 6, 7 기반의 Modus ponens

Inference Rules for Quantifiers (1/2) 3.1 Proof Strategy Quantifier를 포함하는 추론 규칙 Universal instantiation xP(x)가 주어졌을 때, xP(x)이 true라면, domain에 속하는 임의의 값(요소) c에 대해서 P(c)가 true임을 보이는데 사용되는 추론 규칙이다. Universal generalization xP(x)가 주어졌을 때, domain에 속하는 모든 값(요소) c에 대해서 P(c)가 true이면, xP(x)가 true임을 보일 때 사용되는 추론 규칙이다. Existential instantiation xP(x)가 주어졌을 때, xP(x)가 true라면, domain안에 P(c)를 true로 하는 값(요소) c가 적어도 하나 이상 있다는 것을 나타내는 추론 규칙이다. Existential generalization xP(x)가 주어졌을 때, 특정 값(요소) c에 대해서 P(c)가 true이면, xP(x)이 true라는 추론 규칙이다.

Inference Rules for Quantifiers (2/2) 3.1 Proof Strategy Quantifier 사용 명제의 추론 규칙 정리 Rule of inference Tautology Name xP(x)  P(c) xP(x)  P(c) Universal instantiation P(c) for an arbitrary c P(c) for an arbitrary c  xP(x) Universal generalization xP(x)  P(c) for some c xP(x)  P(c) for some c Existential instantiation P(c) for an some c P(c) for an some c  xP(x) Existential generalization

Proof Methods (자세한 내용은 노트 05 참조) 3.1 Proof Strategy 함축(implication) p  q의 증명을 위하여, 다음 방법들을 사용한다. Direct proof: Assume p is true, and prove q. Indirect proof: Assume ¬q, and prove ¬p. (대우의 증명에 해당) Vacuous proof: Prove ¬p by itself. (가정이 false임을 증명) Trivial proof: Prove q by itself. (결론이 항시 true임을 증명) Proof by cases: To prove (p1  p2  ....  pn)  q, prove ((p1  q)  (p2  q)  ....  (pn  q)) Proof by Contradiction: A method for proving p. Assume ¬p, and prove some proposition q is contradiction (i.e., q is always false.) Then, ¬pF, which is only true if ¬p=F Thus, p is true.  주어진 가정(p)을 부정(false)했을 때 항상 false가 되는 명제 q가 있음을 보이면, p의 가정이 잘못되었으므로 p는 true가 된다.

Forward & Backward Reasoning (1/2) - skip 3.1 Proof Strategy Forward Reasoning (전진 추론) 주어진 가정 및 알려진 정리 등을 사용하여 결론을 도출해 가는 방법 Example: Let n  N, such that n is not divisible by 2 or 3. Then, n2−1 is divisible by 24. Since n is not divisible by 2 or 3, it follows that n = 6k + 1 or 6k + 5. (6k, 6k + 2, 6k + 3, and 6k + 4 are divisible by 2 or 3.) Case 1: (n = 6k + 1) n2 − 1 = ((6k + 1)2 − 1) = (36k2 + 24k) = 12(3k + 1)k 12(3k + 1)k is divisible by 24 since (3k + 1)k is even. Case 2: (n = 6k + 5) n2 − 1 = (n + 1)(n − 1) = (6k + 6)(6k + 4) = 12(k + 1)(3k + 2) 12(k + 1)(3k + 2) is divisible by 24 since (k + 1)(3k + 2) is even. Therefore, n2 − 1 is divisible by 24.

Forward & Backward Reasoning (2/2) - skip 3.1 Proof Strategy Backward Reasoning (후진 추론) 결론(q)에서 출발하여 가정(p)이 참임을 이끌어 가는 방법 Example: Let a,b  R, with ab. Then (a+b)/2 > . Conclusion is true if (a + b) > , which is true if (a + b)2 > 4ab, which is true if a2 + 2ab + b2 > 4ab, which is true if a2 − 2ab + b2 > 0, which is true if (a − b)2 > 0, which is true. 상기 예제를 Forward Reasoning으로 증명하는 경우 (a − b)2 > 0  a2 − 2ab + b2 > 0  a2 + 2ab + b2 > 4ab  (a + b)2 > 4ab  (a + b) >  (a+b)/2 >

가설과 증명 (Conjecture & Proof) 3.1 Proof Strategy 가설의 형식화 가능한 많은 형태의 증거에 기초하여 가설을 형식화한다. 기존 정리나 명제를 사용하여 원하는 가설을 만들어내거나, 직관이나 결과가 성립한다는 믿음에 기초하여 가설을 만들어 낸다. 가설의 증명 가설이 형식화되면 목표는 이를 증명하는 것이다. 증명하게 되면, 가설은 정리가 된다. 증명하지 못하면, 가설은 결국 가설로 남게 된다. 예제 가설: a > 2이고 n이 양의 정수이면, an − 1은 합성수이다. (예: 32 − 1 = 8 = 23) (누군가가 직관(뛰어난 통찰력)을 사용하여 이런 가설을 생각했다 하자.) 증명: an − 1 = (a − 1)(an-1 + … + a + 1) 1 < (a − 1) < an − 1이므로, a − 1은 an − 1의 인수이고, 결국 an − 1은 합성수이다.  결과적으로, 상기 가설은 정리가 된다.

가설과 반례 (Conjecture & Conterexample) 3.1 Proof Strategy 가설에 대한 반례 그럴듯한 가설을 제시하였는데, 이의 증명이 어려운 경우, 반례를 생각하게 된다. 반례를 들 수 있으면, 그 가설은 false가 되어 정리가 되지 못한다. 예제 (Leonhard Euler) 가설: n  3인 모든 정수 n에 대해서, n − 1개의 양의 정수들의 n 제곱의 합은 어떤 수의 n제곱이 될 수 없다. (예: n = 3, a3 + b3을 만족하는 c3은 없다.) 반례 1(n = 4): 95,8004 + 217,5194 + 414,5604 = 422,4814 (1988, Noam Elkies) 반례 2(n = 5): 275 + 845 + 1105 + 1335 = 1445 (1966, Lander & Parkin) 나머지는 밝혀진 반례가 없다. 그렇다면, 다른 경우(예: n  6)에 대해서는 가설이 혹시 참이 아닐까?

유명한 가설들 (1/2) 페르마(Fermat)의 마지막 정리 방정식 3.1 Proof Strategy 페르마(Fermat)의 마지막 정리 방정식 가설: xn + yn = zn은 n > 2인 정수일 때, xyz  0인 x, y, z에 대해 해를 갖지 않는다. n = 3인 경우에 대해서는 Euler에 의해 증명됨 n = 4인 경우에 대해서는 Fermat에 의해 증명됨 나머지에 대해서는 타원 곡선 이론이라는 매우 복잡한 정수론 분야에 의해서 1990년대에 Andrew Wiles에 의해 비로소 증명됨 (350년 만에 증명됨) 비로소, 페르마의 마지막 방정식은 가설에서 정리가 되었다.

유명한 가설들 (2/2) 골드바흐(Christian Goldbach) 가설: n > 2인 짝수 n은 두 소수의 합이다. 3.1 Proof Strategy 골드바흐(Christian Goldbach) 가설: n > 2인 짝수 n은 두 소수의 합이다. 예: 4 = 2 + 2, 6 = 3 + 3, 8 = 5 + 3, 10 = 7 + 3, 12 = 7 + 5, … 컴퓨터 이전: 백만 단위까지 증명 (by hand) 컴퓨터 이후: 4∙1014까지 증명(2002년 중반) 아직(?) 증명되지는 않았으나 대부분 수학자는 true라 믿고 있음 유사 가설: n > 2인 짝수 n은 적어도 6개의 소수의 합으로 표현됨 (1995, Ramare 증명)

The Halting Problem (정지 문제) (1/2) - skip 3.1 Proof Strategy Alan Turing discovered in the 1930’s that there are problems unsolvable by any algorithm. (튜링은 “어떠한 알고리즘으로도 풀 수 없는 문제가 있음”을 밝혔다.) The desired function is H(P,I) = the truth value of the statement “Program P, given input I, eventually halts”. (H(P,I) = “프로그램 P와 P의 입력 I가 주어졌을 때, 이 프로그램 P가 정지하는지”의 여부를 판단하는 함수) 튜링은 이러한 함수 H(P,I)가 존재하지 않음을 증명하였다. Implies general impossibility of predictive analysis of arbitrary computer programs. (임의의 프로그램에 대한 예측 분석이 일반적으로 불가능함을 의미한다.)

The Halting Problem (정지 문제) (2/2) - skip 3.1 Proof Strategy 정지 문제의 증명 (by contradiction) H(P,I) = 주어진 Program P와 입력 I에 대해서, 만일 P가 정지하면 “정지”를 출력하고, 그렇지 않으면(만일 P가 무한루프이면) “무한루프”를 출력한다. K(P) = 주어진 Program P에 대해서 H(P,P)가 “정지”를 출력하면, 무한루프를 수행하고, H(P,P)가 “무한루프”를 출력하면, 정지한다. H(K,K) = (H(P,I)의 입력으로 P = K와 I = K를 주는 경우) H(K,K)가 “정지”를 출력하면, K(K)는 무한루프를 수행한다.  모순!  H()는 출력으로 Program K가 정지한다고 하였는데, 실제 K는 무한루프를 수행하므로 모순이다. H(K,K)가 “무한루프”를 출력하면, K(K)는 정지한다.  모순!  H()는 출력으로 Program K가 무한루프를 수행한다 하였는데, 실제 K는 정지하므로 모순이다. 결국, 정지 문제를 해결하는 H(P,I)는 존재하지 않는다!