------------------------------------------------------------------------ Subject: Axiomatic Systems vs. Natural-Deduction Systems ------------------------------------------------------------------------ Let's compare axiomatic systems with natural-deduction systems. 1. Consider the following definitions: An _axiom_ is (by definition) a tautology that we do not attempt to prove on the basis of any other propositions (i.e., an axiom is a proposition that we accept "on faith"). A _rule of inference_ is (by definition) a truth-preserving argument form that relates premises (which are assumed to be true) to a conclusion (which must be true if the premises are true). (i.e., it licenses the inference of the conclusion from the premises) When we put these together, we get a proof: A _proof_ of a proposition P (from axioms) is (by definition) a sequence of propositions such that each proposition in the sequence is either an axiom or follows from previous propositions in the sequence by a rule of inference. 2. An axiomatic logic usually has *lots* of axioms and *very few* rules of inference. A natural-deduction logic usually has *no* axioms and *lots* of rules of inference (to compensate for the lack of axioms). Typically, a natural-deduction system has a *pair* of rules for each connective: one to "introduce" the connective (so that you can infer a conclusion containing the connective) and one to "eliminate" it (so that you can infer a conclusion without that connective). Rosen's text does not use this "intro-elim" method; Fitch's system (which Jim introduced in lecture while I was away) does. 3. Here's an axiomatic system for propositional logic: Axioms: A1. (p -> (q -> p)), where p,q are any propositions i.e., a true proposition follows from anything A2. ((p -> (q -> r)) -> ((p -> q) -> (p -> r))), where p,q,r are any propositions i.e., "->" distributes over itself A3. ((-q -> -p) -> ((-q -> p) -> q)), where p,q are any propositions i.e., if you assume the opposite (-q) of what you're trying to prove, and if you can then derive a contradiction (both p and -p), then you can prove q Note that, because p,q,r can be *any* propositions, what we have here are not merely 3 axioms, but an infinite number of axioms. Rule of Inference: MP: From p and (p -> q) infer q Note that there is only 1 rule of inference. Note, too, that this system only uses 2 connectives: "-" and "->", but, as the text and HW show, that's all you need (i.e., they are functionally complete). 4. Here's a proof in this system: We'll prove the not-so-astounding fact that (A -> A) is a theorem: 1. (A -> ((A -> A) -> A)) -> ((A -> (A -> A)) -> (A -> A)) : (instance of) Axiom A2 {COMMENT: This first step is the most mind-blowing part for most people, but if you look at it carefully, you will see that it really is an instance of axiom 2! The "p" of axiom A2 corresponds to "A", and the "q" of A2 corresponds to "(A -> A)", If you're still not convinced, do a truth-table analysis of it to at least convince yourself that it is a tautology.} 2. A -> ((A -> A) -> A) : (instance of) Axiom A1 3. (A -> (A -> A)) -> (A -> A) : From 1,2, by MP 4. A -> (A -> A) : (instance of) Axiom A1 again {COMMENT: Well, it's not the same *instance* of the axiom as before, but it is another instance of the same axiom.} 5. A -> A : From 3,4 by MP Note that this is, indeed, a valid proof: It is a sequence of propositions, each of which either is an axiom or follows from previous propositions in the sequence by a rule of inference. The last proposition in the sequence is the theorem that we have proved. It all seems like much ado about nothing: a lot of techical machinery to prove something that seems almost trivially obvious and uninteresting. Yes, and that's why most practicing mathematicians and computer scientists use natural deduction. 5. So, here's a proof of the same theorem in our textbook's natural- deduction system. First, recall that we're trying to prove (A -> A). The direct-proof strategy for doing this is to assume the antecedent and then to try to prove the consequent. Assume A, and try to show A. Well, we've got A (we just assumed it). Therefore, we've shown it! End of proof! Seems downright trivial! And it is. It's not a trick: We haven't proved A; we've only proved (A -> A). And we've done it in a much simpler fashion than the complex axiomatic proof above. In fact, we didn't need any axioms, and the only official rule of inference is what Fitch-style systems call "-> introduction": If, from a temporary assumption that p, you can prove that q, then you can infer (p -> q). Our text calls this a proof strategy rather than a rule of inference.