1Lecture 9 • 16.825 Techniques in Artificial IntelligenceLogic Miscellanea• Completeness and Incompleteness• Equality• ParamodulationLogic is a huge subject. It includes esoteric mathematical and philosophical arguments as well as hard-core engineering of knowledge representations and efficient inference algorithms. I’m going to use this lecture to cover a set of random topics in logic that, even if you don’t understand them exactly, it’s good to know a little bit about.The paramodulation rule will also be important to homework 2.2Lecture 9 • 2Completeness and DecidabilityComplete: If KB ² α then KB ` α • If it’s entailed, there is a proofSemi-decidable: • If there’s a proof, we’ll halt with it• If not, maybe halt, maybe notWe found that resolution for propositional logic was sound and complete. Recall that a proof system is complete if whenever a conclusion is entailed by some premises, it can be proved from those premises.3Lecture 9 • 3Completeness and DecidabilityComplete: If KB ² α then KB ` α • If it’s entailed, there is a proofSemi-decidable: • If there’s a proof, we’ll halt with it• If not, maybe halt, maybe notGödel’s Completeness Theorem: There exists a complete proof system for FOLGodel proved a completeness theorem for first-order logic: There exists a complete proof system for FOL. But, living up to his nature as a very abstract logician, he didn’t come up with such a proof system; he just proved one existed.4Lecture 9 • 4Completeness and DecidabilityComplete: If KB ² α then KB ` α • If it’s entailed, there is a proofSemi-decidable: • If there’s a proof, we’ll halt with it• If not, maybe halt, maybe notGödel’s Completeness Theorem: There exists a complete proof system for FOLRobinson’s Completeness Theorem: Resolution refutation is a complete proof system for FOLThen, Robinson came along and showed that resolution refutation is sound and complete for FOL.5Lecture 9 • 5Completeness and DecidabilityComplete: If KB ² α then KB ` α • If it’s entailed, there is a proofSemi-decidable: • If there’s a proof, we’ll halt with it• If not, maybe halt, maybe notGödel’s Completeness Theorem: There exists a complete proof system for FOLRobinson’s Completeness Theorem: Resolution refutation is a complete proof system for FOLFOL is semi-decidable: if the desired conclusion follows from the premises then eventually resolution refutation will find a contradiction.This makes first-order logic semi-decidable. If the answer is “yes”, that is, if there is a proof, then the theorem prover will eventually halt and say so. But if there isn’t a proof, it might run forever! (unlike in the propositional case, in which it is guaranteed that if there isn’t a proof, resolution will eventually stop).6Lecture 9 • 6Adding ArithmeticSo, things are relatively good with regular first-order logic. And they’re still fine if you add addition to the language. But if you add addition and multiplication, it starts to get weird!7Lecture 9 • 7Adding ArithmeticGödel’s Incompleteness Theorem: There is no consistent, complete proof system for FOL + Arithmetic. Either there are sentences that are true, but not provable or there are sentences that are provable, but not true.Godel also had an incompleteness theorem, which says that there is no consistent, complete proof system for FOL plus arithmetic. (Consistent is the same as sound). Either there are sentences that are true, but not provable, or there are sentences that are provable, but not true. It’s not so good either way.8Lecture 9 • 8Adding ArithmeticGödel’s Incompleteness Theorem: There is no consistent, complete proof system for FOL + Arithmetic. Either there are sentences that are true, but not provable or there are sentences that are provable, but not true.Arithmetic gives you the ability to construct code-names for sentences within the logic.P = “P is not provable.”Here’s the roughest cartoon of how the proof goes. Arithmetic gives you the ability to construct code names for sentences within the logic, and therefore to construct sentences that are self-referential. This sentence, P, is sometimes called the Godel-sentence. P is “P is not provable”.9Lecture 9 • 9Adding ArithmeticGödel’s Incompleteness Theorem: There is no consistent, complete proof system for FOL + Arithmetic. Either there are sentences that are true, but not provable or there are sentences that are provable, but not true.Arithmetic gives you the ability to construct code-names for sentences within the logic.P = “P is not provable.”• If P is true: it’s not provable (incomplete)• If P is false: it’s provable (inconsistent)If P is true, then P is not provable (so the system is incomplete). If P is false, then P is provable (so the system is inconsistent). Too bad!10Lecture 9 • 10EqualityWe need to talk a bit about equality. So far we've been doing proofs in a language with predicates and functions, but no equality statements. When we talked about the definition of first-order logic we put equality in our language, so the question is what do you do in resolution, if you have equality, if you want to talk about things being equal to each other.11Lecture 9 • 11Equality∀ x. x = x∀ xy. x=y → y = x∀ xyz. x=y Æ y = z → x = zOne solution is to just treat equality like any other relation and give axioms that specify how it has to work. So, for instance, equality is an equivalence relation, which means it’s symmetric, reflexive, and transitive. We can say that in logic like this.12Lecture 9 • 12Equality∀ x. x = x∀ xy. x=y → y = x∀ xyz. x=y Æ y = z → x = z∀ xy. x=y → (P(x) ↔ P(y))etc., etc., etc., …But then, very sadly, you need more than that. You need to say, for every predicate P, for all X and Y if X = Y then (P(X) if and only if P(Y)). The idea is that you should be able to substitute equals for equals into any context. That doesn’t follow from our equality axioms, and so we’d have add a new axiom for every predicate in our language that says it’s okay to substitute equals into it. That could get to be pretty tedious.13Lecture 9 • 13ParamodulationNeed one more rule to deal with resolution and equality.So what typically happens is that people build special inference procedures for equality into the proof procedure, so in resolution there's a rule called paramodulation. I'll