Logical Entailment - Stanford Logic Group

1 1 Logical EntailmentComputational LogicLecture 3 Michael Genesereth Autumn 20102 Logical ReasoningLogical Reasoning relates premises and conclusion does not say whether conclusion is true in general says conclusion true whenever premises are trueLeibnitz: The intellect is freed of all conception ofthe objects involved, and yet the computation yieldsthe correct : Math may be defined as the subject inwhich we never know what we are talking about norwhether what we are saying is EntailmentA set of premises logically entails a conclusion (written as |= ) if and only if every interpretationthat satisfies the premises also satisfies theconclusion.{p} |= (p q){p} |# (p q){p, q} |= (p q)4 Logical Entailment Logical Equivalence{p} |= (p q){p q)} |# pAnalogy in arithmetic: inequalities rather than equations35 Truth Table MethodWe can check for Logical Entailment by comparingtables of all possible the first table, eliminate all rows that do not the second table, eliminate all rows that do notsatisfy the the remaining rows in the first table are a subset ofthe remaining rows in the second table, then thepremises logically entail the p logically entail (p q)?

2 PqTTTFFTFF pqTTTFFTFF47 ExampleDoes p logically entail (p q)?Does {p,q } logically entail (p q)? pqTTTFFTFF pqTTTFFTFF8 ExampleIf Mary loves Pat, then Mary loves it is Monday, then Mary loves Pat or it is Monday, does Mary love Quincy?FFFTFF TTF TFT TTTqpmFFFTFFFTFTTF TFT TTTqpm59 Logical Entailment and SatisfiabilityTheorem: |= if and only if { } that |= . If an interpretation satisfies ,then it must also satisfy . But then it cannot satisfy . Therefore, { } is that { } is unsatisfiable. Then everyinterpretation that satisfies must fail to satisfy , it must satisfy . Therefore, |= .Upshot: We can determine Logical Entailment bydetermining : {(p q), (m p q)} |= (m q)?Or: Is {(p q), (m p q), (m q)} unsatisfiable?

3 FFFTFFFTFTTFFFTTFTFTTTTTqpm611 ProblemThere can be many, many interpretations for aPropositional that, for a language with n constants, thereare 2n possible there are many constants among premisesthat are irrelevant to the conclusion. Much : Proofs12 PatternsA pattern is a parameterized expression, anexpression satisfying the grammatical rules of ourlanguage except for the use of meta-variables(Greek letters) in place of various subparts of Pattern: ( )Instance:p (q p)Instance:(p r) ((p q) (p r))713 rules of InferenceA rule of inference is a rule of reasoningconsisting of one set of sentence patterns, calledpremises, and a second set of sentence patterns,called conclusions. 14 Rule InstancesAn instance of a rule of inference is a rule in whichall meta-variables have been consistently replaced byexpressions in such a way that all premises andconclusions are syntactically legal slipperywetslippery(p q) rp qrraining wetrainingwetp (q r)pq r815 Sound rules of InferenceA rule of inference is sound if and only if the premisesin any instance of the rule logically entail Ponens (MP)Modus Tolens (MT)Equivalence Elimination (EE)Double Negation (DN) 16 Proof (Version 1)A proof of a conclusion from a set of premises is asequence of sentences terminating in the conclusionin which each item is either:1.

4 A premise2. the result of applying a rule of inference to earlieritems in it is raining, the ground is wet. When theground is wet, it is slippery. It is raining. Prove thatit is :1, :2,418 ErrorNote: rules of inference apply only to top-levelsentences in a proof. Sometimes works butsometimes !No! wetMP: 1,21019 ExampleHeads you win. Tails I lose. Suppose the coincomes up tails. Show that you mMP:2, mEE:48. m :8,620 Axiom SchemataFact: If a sentence is valid, then it is true under allinterpretations. Consequently, there should be a proofwithout making any assumptions at : (p (q p)) is a valid : Prove (p (q p)).Solution: We need some rules of inference withoutpremises to get axiom schema is sentence pattern construed as arule of inference without and SchemataAxiom Schemata as rules of Inference ( ) rules of Inference as Axiom Schemata ( ) ( )Note: Of course, we must keep a least one rule ofinference to use the schemata.

5 By convention, weretain Modus Ponens. ( ) 22 Valid Axiom SchemataA valid axiom schema is a sentence pattern denotingan infinite set of sentences, all of which are Introduction (II): ( )ImplicationDistribution (ID):( ( )) (( ) ( ))1223 Proof (Official Version)A proof of a conclusion from a set of premises is asequence of sentences terminating in the conclusionin which each item is either:1. a premise2. An instance of an axiom schema3. the result of applying a rule of inference to earlieritems in ProofWhenever p is true, q is true. Whenever q is true, r istrue. Prove that, whenever p is true, r is rPremise3.(q r) (p (q r)) (q r)MP:3,25.(p (q r)) ((p q) (p r))ID6.(p q) (p r)MP:5, rMP:6,11325 Mendelson AxiomatizationII: ( )ID:( ( )) (( ) ( ))CR:( ) (( ) )Note: Mendelson s system assumes there are only twooperators, viz.

6 And . Fortunately, all sentences inPropositional Logic can be reduced to equivalent sentenceswith these operators by applying the following rules .( ) (( ) ( ))( ) ( ) ( ) ( ) ( ) ( )26 Kleene AxiomatizationII: ( )ID:( ( )) (( ) ( ))AI: ( ( ))AE1:( ) AE2:( ) OI1: ( )OI2: ( )OE:( ) (( ) ( ))CM:( ) (( ) )DN:( )Note: Kleene s system assumes there are only four operators,viz. , , , and .1427 Standard Axiom SchemataII: ( )ID:( ( )) (( ) ( ))CR:( ) (( ) )EQ:( ) ( )( ) ( )( ) (( ) ( ))OQ: ( ) ( )( ) ( )( ) ( )28 Meredith Axiomatization(((( ) ( )) ) ) (( ) ( ))1529 ProvabilityA conclusion is said to be provable from a set ofpremises (written |- ) if and only if there is a finiteproof of the conclusion from the premises using onlyModus Ponens and a complete Logical axiomatization( Mendelson, Kleene, Standard, Meredith).

7 30 Soundness and CompletenessSoundness: Our proof system is sound, if theconclusion is provable from the premises, then thepremises propositionally entail the conclusion.( |- ) ( |= )Completeness: Our proof system is complete, if thepremises propositionally entail the conclusion, then theconclusion is provable from the premises.( |= ) ( |- )1631 Truth Tables and ProofsThe truth table method and the proof method succeedin exactly the same large problems, the proof method often takes fewersteps than the truth table method. However, in theworst case, the proof method may take just as many ormore steps to find an answer as the truth table , proofs are much smaller than thecorresponding truth tables. So writing an argument toconvince others does not take as much Theorem: |- ( ) if and only if { } |.

8 Substitution Theorem: |- ( ) and |- , then itis the case that |- .Chaining Theorem: If |- ( ) and |- ( ),then |- ( ).1733 Proof Without MetatheoremsProblem: {p q, q r} |- (p r)? rPremise3.(q r) (p (q r)) (q r)MP:3,25.(p (q r)) ((p q) (p r))ID6.(p q) (p r)MP:5, rMP:6,134 Proof Using Deduction TheoremProblem: {p q, q r} |- (p r)? :1, :2,41835TA Appeasement RulesWhen we ask you to show that something is true, youmay use we ask you to give a formal proof, it meansyou should write out the proof as defined we ask you to give a formal proof usingcertain rules of inference or axiom schemata, itmeans you should do so using only those rules ofinference and axiom schemata and no ReasoningIn deduction, the conclusion is true whenever thepremises are : pConclusion: (p q)Premise: pNon-Conclusion: (p q)Premises: p, qConclusion: (p q)