05 Logic and Proof.pdf

Logic and Proof Keunhyuk Yeom Dept. of Computer Engineering Pusan National University [email protected]  The Story So Far l Syntax versus semantics l Formal Systems u language: alphabet + grammar u inference system: axioms...

Logic and Proof Keunhyuk Yeom Dept. of Computer Engineering Pusan National University [email protected]  The Story So Far l Syntax versus semantics l Formal Systems u language: alphabet + grammar u inference system: axioms + rules of inference u theorem, proof, deduction l Semantics u interpretation u consistency (soundness), completeness 2 Computer Engineering, Pusan National University  Basic Elements Syntax (language) Semantics (meaning) Interpretation Inference system Validity (rules of reasoning) 3 Computer Engineering, Pusan National University  In the Next, l We will look at three formal systems: u Propositional logic u Predicate logic u Set theory l We will also briefly examine some of the main proof styles used for these systems u Natural deduction u Equational reasoning u Proof by contradiction u Proof by case analysis u Induction 4 Computer Engineering, Pusan National University  Propositions (명제) l A proposition is a statement that is either true or false (but not both). Examples: u Busan is the home of the Giants. u Busan is the capital of Korea. l The same proposition can often be expressed in several ways. Examples: u five is bigger than four u four is less than five u 5>4 5 Computer Engineering, Pusan National University  Propositional Logic: Syntax l Alphabet: {P, Q, R,..., Ù, Ú, Ø, Þ, Û, ^, (, )} l Grammar: 명제기호 Connectives sentence = “P” | “Q” | “R” |... | “Ø” sentence | “(” sentence “Ú“ sentence “)” | “(” sentence “Ù“ sentence “)” | “(” sentence “Þ“ sentence “)” | “(” sentence “Û“ sentence “)” u We usually drop the parentheses when the resulting sentence is unambiguous 6 Computer Engineering, Pusan National University  The Set of Propositions: PROP l PROP := the smallest closed under application of connectives: l ^ÎPROP l pi ÎPROP for all iÎN l jÎPROP Þ (Øj)Î PROP l j, yÎ PROP Þ (jÙy), (j Ú y), (j®y), (j«y)Î PROP 7 Computer Engineering, Pusan National University  The Examples of Propositions l (Øp0) l (Ø(Øp0)) l (p0 Ù (p1 Ù p2)) l (p0® (p1® p2)) l Correct expressions of Propositional Logic are full of unnecessary parenthesis. 8 Computer Engineering, Pusan National University  Abbreviation(생략) l If c=Ù, Ú, ®, p0 c p1 c p2 c … , if right associativity (p0 c (p1 c (p2 c …))) p0 Ù p1 Ù p2, p0®p1® p2, … (p0 Ù (p1 Ù p2)), (p0® (p1® p2)) In fact, Ù, Ú 은 left ® 은 right 9 Computer Engineering, Pusan National University  Operator precedence l 연산자 우선순위(operator precedence): u Ø binds more strictly than Ù, Ú, u Ù, Ú bind more strictly than ®, «. l ØØp0 for (Ø(Øp0)), l Øp0 Ù p1 for ((Øp0 ) Ù p1) l p0 Ù p1® p2 for ((p0Ù p1) ® p2), … 10 Computer Engineering, Pusan National University  Subformula(부논리식) l 직접 부(논리)식 (Immediate Subformulas) : u ^, pi 없음 u Øj j u (jÙy), (j Ú y), (j®y), (j«y) j, y l j is a subformula(부식) of y iff there is some chain j=j0, j1 ,…, jn=y, each formula being some immediate subformula of the next formula. l Subformulas of j=((p0Ù p1) ® p2) are: j itself, (p0Ù p1), p0, p1, p2. 11 Computer Engineering, Pusan National University  Propositional Logic: Semantics l The meaning of a propositional wff is given as follows: u Each primitive symbol (P, Q, R,...) is given an interpretation as a proposition (with an associated truth value) Example: P Þ “August 31, 1998 is a Thursday” u The meaning (truth or falsity) of a compound wff is determined by its subparts as specified by a set of rules (defined by standard tables): Example: p q pÞq T T T T F F (Note 1: four interpretations) F T T F F T (Note 2: this is the semantic domain) → In short, we use “truth tables” 12 Computer Engineering, Pusan National University  Semantics l 명제상수/연결자 해석 u Each Proposition ( pi ) can be T (true, 참) or F (false, 거짓). u ^ is F. u Ø, Ù, Ú, ®, « : 일항/이항 함수(Truth Tables), Øj, (jÙy), (jÚy), (j®y), (j«y), u 직접 부논리식 j, y 의 진리값에 의존하지, 의미에는 의존하지 않는다. 13 Computer Engineering, Pusan National University  Øj 의 진리표 j=T j=F Øj=F Øj=T 14 Computer Engineering, Pusan National University  Semantic Turnstyle l We write |= W if a sentence W is true for any interpretation l We write P |= W if a sentence W is true whenever a list of sentences P are true. l We say W is a semantic consequence of P. l Example: P Ù Q |= P Ú Q 15 Computer Engineering, Pusan National University  Terminology & Special Cases l A sentence of the form u A Ù B is called a conjunction ª A and B are conjuncts u A Ú B is called a disjunction ª A and B are disjuncts u A Þ B is called an implication ª A is the antecedant; B is the consequent l Some sentences always interpret to true. u these are called tautologies (that is, |= A) u example: a sentence of the form A Ú Ø A, where A is any proposition l Some sentences always interpret to false. u these are contradictions, or inconsistencies u example: a sentence of the form A Ù Ø A, where A is any proposition 16 Computer Engineering, Pusan National University  Tautology and Contradiction l jÎPROP. l Tautologies (항진): j 항진 çè For every evaluation v, [j]v =T. l Contradictions (모순): j 모순 çè For every evaluation v, [j]v =F. l Tautology conveys our intuitive idea of being “logically true”, or “true no matter what the Propositional constants are”. 17 Computer Engineering, Pusan National University  Example of Tautology l Double Negation Law: ØØj « j. l Excluded Middle(EM): j Ú Øj. l An easy exercise: check that j Ú Øj is a tautology, i.e., [jÚØj]v = True, for all valuations v:N®{T,F}. 18 Computer Engineering, Pusan National University  EM is Tautology l Proof of: Excluded Middle is a tautology. [jÚØj]v = TÚ([j]v ,[Øj]v) = TÚ([j]v,TØ([j]v)) u Case [j]v = True: [j Ú Øj]v = TÚ(True, TØ(True)) = TÚ(True, False) = True. u Case [j]v = False: [j Ú Øj]v = TÚ(False, TØ(False)) = TÚ(False, True) = True. 19 Computer Engineering, Pusan National University  jÙy (Conjunction)의 Truth Table j=T j=F y=T jÙy= T jÙy= F y= F jÙy= F jÙy= F 20 Computer Engineering, Pusan National University  Disjunction(이접) Disjunction is not exclusive(배타적). i.e., if jÚy, both j and y can be true.(j and y 둘 다 참일 수도 있다.) j=T j=F y=T jÚy= T jÚy= T y= F jÚy= T jÚy= F 21 Computer Engineering, Pusan National University  Implication (함의, 含意) l Implication은 질료적(質料的, material)이다. l 연관이 없는 두문장 j, y에 대해, j®y 참: 즉, 구성원 j, y의 진리값에만 의존. j=T j=F y=T j®y= T j®y= T y= F j®y= F j®y= T 22 Computer Engineering, Pusan National University  Propositional Calculus l To complete our system we need a set of inference rules (called a calculus, here) l But we will save that until we treat Proof systematically 23 Computer Engineering, Pusan National University  Equivalence (동치) l We augment our formal system with a new symbol l Two sentences are equivalent ( º ) iff their truth value is the same under every interpretation. l Example: (P Þ Q) º (Ø P Ú Q) l There is a collection of properties of equivalence. u These can be used in an “equational” style to do proof u Properties include the usual associative, commutative, distributive properties of the logical operators 24 Computer Engineering, Pusan National University  Equivalence l j«y j=T j=F y=T j«y=T j«y=F y=F j«y=F j«y=T 25 Computer Engineering, Pusan National University  About Proofs l There are many styles (or techniques) of proof. l One common style is called "natural deduction" l In this style a proof is constructed as a tree. l We will also be using "equational reasoning", another common style l However there are a lot of other styles that we will use as needed. 26 Computer Engineering, Pusan National University  Proof l Formal Proofs (정형증명). l Natural Deduction (자연추론): 논리식 j의 정형증명 l A formal proof of j is a tree whose root is labeled j and whose children are assumptions j1, j2, j3, … of the rule r we used to conclude j. 27 Computer Engineering, Pusan National University  Natural Deduction Rules l Rule (규칙). For each logical symbol c=^, Ù, Ú, ®, and each formula j with outermost connective c, we give: l c의 Introduction rule describing under which conditions j is true; l c의 Elimination rule describing what we may infer from the truth of j. l Elimination rules for c are justified in term of the Introduction rules for c we chose. 28 Computer Engineering, Pusan National University  Negative and Equivalence l Natural Deduction: the missing connectives. l We treat Øj, j«y, as abbreviating (j®^), (j®y)Ù(y®j), l We do not add specific rules for the connectives Ø, «. 29 Computer Engineering, Pusan National University  Proof Representation l Let j be any formula, and G be any unordered (finite or infinite) list of formulas. We use the notation G … j l abbreviated by G|- j, for: l “there is a proof of j whose assumptions are included in G”. 30 Computer Engineering, Pusan National University  Crossing Assumption(가정 지우기) l We use the notation \ G, j … y l for: “we drop/discharge zero or more assumptions equal to j from the proof of y”. 31 Computer Engineering, Pusan National University  Assumption of a Proof l Assumptions of a proof j1 j2 j3 … r -------------------------------- y are inductively defined as: all assumptions of proofs of j1, j2, j3, …, minus all assumptions we “crossed”. 32 Computer Engineering, Pusan National University  Identity Principle l Identity Principle: The simplest proof is: j having 1 assumption, j, and conclusion the same j. l We may express it by: G|-j, for all jÎG l We call this proof “The Identity Principle” (we derive j from j). 33 Computer Engineering, Pusan National University  Rules for ^ l Introduction rules: none (because ^ is always false). l Elimination rules: from the truth of ^ (a contradiction) we derive everything: ^ ---- j l If G|- ^, then G|-j, for all j 34 Computer Engineering, Pusan National University  Rules for Ù l Introduction rules: j y -------- jÙy l If G|- j and G|- y then G|- j Ù y 35 Computer Engineering, Pusan National University  Elimination Rule for Ù l Elimination rules: jÙy jÙy -------- ------- j y l If G|- j Ù y, then G|- j and G|- y 36 Computer Engineering, Pusan National University  Rules for Ú l Introduction rules: j y -------- ------- jÚy jÚy l If G|- j or G|- y, then G|- j Ú y 37 Computer Engineering, Pusan National University  Elimination Rules for Ú l Elimination rules: j … \ y … \ jÚy q q -------------------------------------- q l If G|- j Ú y and G,j|-q and G, y|-q, then G|-q l We may drop any number of assumptions equal to j (to y) from the first (from the 38 second) proof of q Computer Engineering, Pusan National University  Rules for ® l Introduction rule: \ j … y -------- j®y l If G,j |- y, then G|-j®y l We may drop any number of assumptions equal to j from the proof of y. 39 Computer Engineering, Pusan National University  Elimination Rule for ® j®y j ---------------- y l If G|-j®y and G|-j, then G |- y. 40 Computer Engineering, Pusan National University  Double Negation l The only axiom not associated to a connective, nor justified by some Introduction rule, is Double Negation(DN, 이중부정): Øj … \ ^ --- j l If G, Øj|- ^, then G|-j l We may drop any number of assumptions equal 41 to Øj from the proofComputer of j.Engineering, Pusan National University  Weakening and Substitution l Lemma (Weakening and Substitution). 1. If G|-j and GÍD, then D|-j. 2. If G|-j and G,j |-y, then G|- y. Proof. Any proof with all free assumptions in G has all free assumption in D. Replacing, in the proof of y with free assumptions all in G,j, all free assumptions j by a proof of j with all free assumptions in G. 42 Computer Engineering, Pusan National University  Propositional Calculus l To complete our formal system we need a set of inference rules (called a calculus) l One way to represent these rules is in the form: if we have proved these facts we can conclude these facts l Examples Note: A, B, C, … are AÙB A A, A Þ B meta variables, unlike A AÚB B P, Q, R,... l These are given names (respectively): Ù-elimination, Ú-introduction, Þ-elimination 43 Computer Engineering, Pusan National University  Propositional Calculus (cont.) l For each of the five propositional operators (Ù, Ú, Ø, Þ, Û) we have an introduction and elimination rule. l Following, we consider these in two batches A, B A, B Ù-introduction AÙB BÙA AÙB AÙB Ù-elimination A B Ú-introduction A A AÚ B BÚA ØØA Ø -elimination A Modus Ponens A, AÞB Þ-elimination B 44 Computer Engineering, Pusan National University  Propositional Calculus (cont.) Û-elimination AÛB AÛB AÞB BÞA Û-introduction A Þ B, B Þ A AÛB 45 Computer Engineering, Pusan National University  Examples Prove: (P Ù Q) |- (P Ú Q) Derivation: 1. P Ù Q premise 2. P Ù-elimination, 1 3. P Ú Q Ú-introduction, 2 Prove: P, P Þ Q , Q Û R |- Q Ù R Derivation:... 46 Computer Engineering, Pusan National University  Examples Prove: P Þ Q , Q Þ R |- P Þ R Prove: P Þ Q |- Ø(P Ù Ø Q) Prove: P, Ø P |- Q 47 Computer Engineering, Pusan National University  Relation Between Syntactic and Semantic Domains l Propositional Calculus is Consistent u Anything that can be proved is valid u If P |- W then P |= W l Propositional Calculus is Complete u Anything that is valid can be proven using the inference rules u If P |= W then P |- W l This allows us to shift between the two worlds l In particular we can substitute Û for º u To show |- P Û Q we can demonstrate |= P º Q l Equivalences, especially u Commutative, associative, distributive properties, De Morgan 48 rules Computer Engineering, Pusan National University  Other Useful Results Theorem : |- P Ú Ø P Derivation : (P Þ Q) |- (Ø P Ú Q) Theorem : |- (P Þ Q) Ú (Q Þ P) Contrapositive : P Þ Q |- Ø Q Þ Ø P 49 Computer Engineering, Pusan National University  Exercise l P, P Þ Q , Q Û R |- Q Ù R 1. P premise 2. P ® Q premise 3. Q 1,2 ®-E 4. Q « R premise 5. Q ® R 4 «-E 6. R 3,5 ®-E 7. Q Ù R 3,6 Ù-I 50 Computer Engineering, Pusan National University  Exercise l P Þ Q , Q Þ R |- P Þ R 1. P ® Q premise 2. Q ® R premise 3. P assumption 4. Q 1,3 ®-E 5. R 2,4 ®-E 6. P ® R 3~5 ®-I 51 Computer Engineering, Pusan National University  Exercise l P Þ Q |- Ø(P Ù Ø Q) 1. P ® Q premise 2. P Ù ØQ assumption 3. P 2 Ù-E 4. ØQ 2 Ù-E 5. Q 1,3 ®-E 6. ^ 4,5 ®-E 7. Ø(P Ù ØQ) 2~6 ®-I 52 Computer Engineering, Pusan National University  Exercise l P, Ø P |- Q 1. P premise 2. ØP premise 3. ^ 1,2 ® -E 4. Q 3 ^-E 53 Computer Engineering, Pusan National University  Exercise l P Ù Ø Q Þ R, Ø R, P |- Q 54 Computer Engineering, Pusan National University  Exercise l Let’s check that the system moves to the correct state when the alarm is on. The specification for Nuclear Power reactor System u If the operator types the ALARM command, then the subsidiary alarm will be activated and an alarm message will be written to the log file. u Whenever the subsidiary alarm is activated, the main valve is closed and shut-down is stated. u If the main valve is closed, then reactor can be regarded as being in a non-operational state. Attributes u If the ALARM command is activated, the reactor will be in a non-operational state. Verification by Proof(정리 증명) A Þ S Ù M, S Þ C Ù D, C Þ N |- A Þ N 55 Computer Engineering, Pusan National University  Exercise Let’s see the Half-Adder. S represents sum, and C represents carry. The Logic for Half-Adder is as follows: S Û ((Ø P Ù Q) Ú (P Ù Ø Q) CÛPÙQ One of attributes that we must verify is “Both sum and carry are not true”. That is, Ø(S Ù C) 회로에서 이러한 속성이 만족되는지를 보이시오. 즉, 다음을 증명하시오. (S Û ((Ø P Ù Q) Ú (P Ù Ø Q))) Ù (C Û P Ù Q) |- Ø(S Ù C) 56 Computer Engineering, Pusan National University  Predicate Logic l Sometimes we want to assert that all elements of some set (S) satisfy a common property (P). l For example if S == {Larry, Joe, Moe}, we might want to claim that all elements of S are stooges. l We could write (Larry is a stooge) Ù (Joe is a stooge) Ù (Moe is a stooge) l Alternatively we can create a template: Stooge( ) Stooge(Larry) Ù Stooge (Joe) Ù Stooge (Moe) l Stooge() is called a predicate. 57 Computer Engineering, Pusan National University  Predicates But for large sets this becomes unwieldy (or impossible). l So we use a shorthand: " x:S · Stooge(x) l Similarly, to assert the existence of an element of some set (S) that satisfies a property (P) we use $ x:S · P(x) which is shorthand for P(s1) Ú P(s2) Ú P(s3) Ú … , S = {s1, s2, s3, …} 58 Computer Engineering, Pusan National University  Predicates (cont.) l Sometimes you can assume that the sets that are quantified over are understood by context, and then not specify them examples: " x · P(x), $ x · Q(x) however, usually we will make this explicit l You can think of a predicate as a boolean valued function: when applied to an argument it returns true or false. l Predicates may have n arguments u examples: >, is-pythagorean 59 Computer Engineering, Pusan National University  Predicate Logic: Syntax l Alphabet: as with propositional logic, but includes quantifiers (", $) and · u " is called a “universal” quantifier u $ is called an “existential” quantifier l Grammar: u but note every quantified expression has a · l Can nest quantified expressions u " x · (" y · ($ z · P(x,y,z))) u usually leave out the parentheses u combine adjacent variables with same quantifier. u so this becomes " x, y · $ z · P(x,y,z) 60 Computer Engineering, Pusan National University  Scoping l Quantified variables have a scope u informal rule, extends to right to first unmatched right parenthesis, skipping over “holes” u variables not in scope of a quantifier are called “free variables” l Examples " x · P(x) Ù Q(x) Þ R(x) (" x · P(x) Ù Q(x)) Þ R(x) " x · P(x) Ù (Q(x) Þ R(x)) " x · P(x) Ù (" x · Q(x)) Þ R(x) " x · P(x) Ù " x · Q(x) Þ R(x) 61 Computer Engineering, Pusan National University  Predicate Logic: Semantics l More complex than propositional logic l Basic idea is that sentence " x:T · P(x) is true iff P is true of all values of x, and $ x:T · Q(x) is true iff Q is true for some value of x where x ranges over the set T 62 Computer Engineering, Pusan National University  Encoding English Formally l Some SE Class students like logic l SE Class students like logic l SE Class students like only logic l No SE Class student likes logic l If an SE Class student likes logic then he/she has completed Models l An SE Class student likes logic only if he/she has completed Models l Exactly one SE Class student likes Models 63 Computer Engineering, Pusan National University  Predicate Calculus l As with Propositional Logic we introduce a set of deductive rules. l Similar to situation before u Can use natural deduction style u Can also use other styles of proof l Whole system is called First Order Predicate Logic (FOPL) 64 Computer Engineering, Pusan National University  Equality l We now add one more symbol to Predicate Logic = to represent that two entities are the same. l This is equivalent to having a special predicate “equals”, but we use the more common infix notation. l Formally deferred to as First Order Predicate Logic with Equality l We also add three new axioms: A = A (reflexivity) A = B Û B = A (symmetry) A = B Ù B = C Þ A = C (transitivity) l And one new inference rule: "substitution of equals Substitution rule: m = n, S(n) for equals" S[m/n] 65 Computer Engineering, Pusan National University  Theories l We can do a lot with just logic. l But sometimes we want to introduce special axioms to describe a specific phenomenon. l Then we are interested in the consequences of those axioms (given the other rules of deduction). l These consequences are called a theory. 66 Computer Engineering, Pusan National University  Examples l Some general theories that we will encounter in this course u set theory u theory for sequences u theory for concurrent processes l Other theories we will make up on the spot to characterize a software system u example: theory of telephones for a switching system u example: theory of devices and event processing for real- time system 67 Computer Engineering, Pusan National University