deduction proof system imps home page自然演绎证明系统小鬼主页课件

Natural Deduction System for First Order Logic Student: Wei Lei Instructor: W. M. Farmer Department of Computing and Software McMaster University, Hamilton, CA Contents Natural Deduction Natural Deduction Proof Rules of First Order logic Axioms of Natural Deduction System Reference Natural Deduction Natural deduction was invented by G. Gentzen in 1934. The idea was to have a system of derivation rules that as closely as possible reflect the logical steps in an informal rigorous proof. For each connective there is an introduction rule (except conjunction, which has two) which can be seen as a definition of which conditions must be satisfied for the proposition to be true. Natural Deduction tries to follow the natural style of reasoning. Most of the proof consists of forward reasoning, i.e. deriving conclusions, deriving new conclusions from these conclusions, etc. Occasionally hypotheses are introduced or dropped. A derivation is a tree where the nodes are the rules and the leafs are the assumptions of the derivation. The root of the tree is the conclusion of the derivation. An assumption may be discharged by a rule in the derivation; that an assumption A is discharged in a derivation is denoted by A. Natural Deduction Proof Definition. A natural deduction proof is a finite tree whose leaves are formula (over the alphabet ,) and which is built by using the rules. Example: p q, r |= p r Proof: p q e p r i p r Rules of First Order logic If we have a derivation of B from the assumption A, we may derive AB and discharge the assumption A: A I B A B Given derivations of A B and A, we can conclude B: A B A E B For conjunction, the introduction rule tells us that if we have derivations of A and B, then we can conclude A B: A B I A B Rules of First Order logic There are two elimination rules for conjunction: A B E1 A A B E2 B We can infer a disjunction if we know one of the disjuncts. Hence there are two introduction rules for the disjunction: A V I1 A V B B V I2 A V B Rules of First Order logic The elimination rule for disjunction is slightly more complicated to formulate. We must make use of the fact that we know AVB but not necessarily which of A and B it is that holds. A B A V B C C VE C Rules for : A A A I E A Rules of First Order logic Rules for : A B A B E1 E2 AB BA AB BA I A B Rules for : A A A B E B B I A B Rules of First Order logic Rules for : x: X P(x) x is a new object of type X E Px:=t P(X) I x: X P(x) The notation Px := t means intelligent replacement. Also we have rules for equality: Equality reflexivity Equality replacement Axioms of Natural Deduction System Example of an axiomatic system of natural deduction Name Of System: AS Let A,B denote statements. Undefined terms: , Axiom(conjunction C): A,B; therefore A B Axiom(simplification1 S1): A B; therefore A Axiom(simplification2 S2): A B; therefore B Axiom(double negation1 DN1): ( A); therefore A Axiom(double negation2 DN2): A; therefore ( A) Axiom(Conjunctive Syllogism CS): A,(A B); therefore B Definition: A V B = ( A B) Definition: If A then B = (A B) Definition: A if only if B = (if A then B) (if B then A) Notice that the axioms were not framed using any of the definitions. Axioms of Natural Deduction System Whether or not AS is complete. That is, the question as to whether or not AS contains enough axioms in order for a reasoning agent to figure out all possible natural deductions (memory limitations aside), can be raised. If the answer is yes, then the system is said to be complete. It turns out that AS is complete, but proving so is rather difficult. Reference i John M. Anderson and Henry W.Johnstone, Jr. Natural Deduction, The Logical Basis of Axiom Systems. Wadsworth publishing company, inc. Belmont, California:1962 ii Dirk