PROPOSITIONAL LOGIC deals with PROPOSITIONS — statements that are either TRUE or FALSE, with no internal structure visible to the logic. SYNTAX — what counts as a sentence: ATOMIC SENTENCES a single PROPOSITION SYMBOL: P, Q, R, W₁,₃, and the fixed symbols True and False COMPLEX SENTENCES built with the five LOGICAL CONNECTIVES: ¬ NOT negation ¬P ∧ AND conjunction P ∧ Q ∨ OR disjunction P ∨ Q ⇒ IMPLIES implication P ⇒ Q ⇔ IFF biconditional P ⇔ Q PRECEDENCE, highest to lowest: ¬, ∧, ∨, ⇒, ⇔ So ¬P ∨ Q ∧ R ⇒ S reads ((¬P) ∨ (Q ∧ R)) ⇒ S. SEMANTICS — what a sentence means: A MODEL is an assignment of true or false to EVERY proposition symbol. With n symbols there are 2^n models. The TRUTH VALUE of a complex sentence in a model is computed from its parts by the truth tables: P Q │ ¬P │ P∧Q │ P∨Q │ P⇒Q │ P⇔Q ─────────┼────┼─────┼─────┼─────┼───── T T │ F │ T │ T │ T │ T T F │ F │ F │ T │ F │ F F T │ T │ F │ T │ T │ F F F │ T │ F │ F │ T │ T THE IMPLICATION ROW THAT CONFUSES EVERYONE: P ⇒ Q is TRUE whenever P is FALSE, regardless of Q. "If 2+2=5 then the moon is cheese" is TRUE in propositional logic. WHY: P ⇒ Q is equivalent to ¬P ∨ Q. It is a claim about truth values, NOT about causation. It says "it is not the case that P holds and Q fails" — and if P never holds, the claim is trivially satisfied. This is called a VACUOUS TRUTH, and forgetting it is the commonest source of confusion in exercises. KEY DEFINITIONS — these must be precise: SATISFIABLE true in at least one model UNSATISFIABLE true in no model — a CONTRADICTION e.g. P ∧ ¬P VALID true in EVERY model — a TAUTOLOGY e.g. P ∨ ¬P ENTAILMENT α ⊨ β means: in every model where α is true, β is also true. "β follows from α." EQUIVALENCE α ≡ β means α ⊨ β and β ⊨ α THE DEDUCTION THEOREM links them: α ⊨ β if and only if (α ⇒ β) is VALID AND THE REFUTATION FORM, which is what proof procedures use: α ⊨ β if and only if (α ∧ ¬β) is UNSATISFIABLE THIS SECOND FORM IS THE BASIS OF RESOLUTION: to prove something, assume its negation and derive a contradiction. MODEL CHECKING — the brute-force method: enumerate all 2^n models and check. Sound and complete, and hopeless beyond small n: 3 symbols → 8 rows 10 symbols → 1,024 20 symbols → 1,048,576 30 symbols → 1,073,741,824 PROPOSITIONAL SATISFIABILITY IS NP-COMPLETE — it was the FIRST problem proved so (Cook, 1971) — so no algorithm is known that avoids exponential worst-case behaviour.

THE STANDARD INFERENCE RULES. Each is sound: if the premises are true, the conclusion must be. MODUS PONENS α ⇒ β, α ────────── β MODUS TOLLENS α ⇒ β, ¬β ─────────── ¬α AND-ELIMINATION α ∧ β ───── α AND-INTRODUCTION α, β ───── α ∧ β OR-INTRODUCTION α ───── α ∨ β UNIT RESOLUTION α ∨ β, ¬β ─────────── α RESOLUTION α ∨ β, ¬β ∨ γ ─────────────── α ∨ γ HYPOTHETICAL SYLLOGISM α ⇒ β, β ⇒ γ ─────────────── α ⇒ γ TWO FALLACIES that look like rules and are not — knowing these is worth marks: AFFIRMING THE CONSEQUENT from α ⇒ β and β, concluding α. INVALID. Counterexample: α false, β true satisfies both premises and falsifies the conclusion. "If it rains the ground is wet; the ground is wet; therefore it rained" — the sprinkler was on. DENYING THE ANTECEDENT from α ⇒ β and ¬α, concluding ¬β. INVALID, by the same model. THE LOGICAL EQUIVALENCES — needed for converting to normal form: DE MORGAN ¬(α ∧ β) ≡ ¬α ∨ ¬β ¬(α ∨ β) ≡ ¬α ∧ ¬β IMPLICATION α ⇒ β ≡ ¬α ∨ β ELIMINATION CONTRAPOSITION α ⇒ β ≡ ¬β ⇒ ¬α BICONDITIONAL α ⇔ β ≡ (α ⇒ β) ∧ (β ⇒ α) ELIMINATION DOUBLE NEGATION ¬¬α ≡ α DISTRIBUTIVITY α ∧ (β ∨ γ) ≡ (α ∧ β) ∨ (α ∧ γ) α ∨ (β ∧ γ) ≡ (α ∨ β) ∧ (α ∨ γ) COMMUTATIVITY, as expected for ∧ and ∨ ASSOCIATIVITY CONVERTING TO CONJUNCTIVE NORMAL FORM (CNF) — a conjunction of clauses, each clause a disjunction of literals. Required by resolution. THE PROCEDURE, in order: 1. eliminate ⇔ using biconditional elimination 2. eliminate ⇒ using α ⇒ β ≡ ¬α ∨ β 3. move ¬ inwards using De Morgan and double negation, so negations apply only to atoms 4. distribute ∨ over ∧ 5. flatten nested ∧ and ∨ WORKED CNF CONVERSION of (P ∨ Q) ⇒ R: step 2: ¬(P ∨ Q) ∨ R step 3: (¬P ∧ ¬Q) ∨ R De Morgan step 4: (¬P ∨ R) ∧ (¬Q ∨ R) distribute RESULT: two clauses, {¬P, R} and {¬Q, R}. Note that CNF conversion can cause EXPONENTIAL GROWTH in the worst case from step 4 — which is why practical tools use the Tseitin transformation, introducing new variables to keep the result linear in size. RESOLUTION — the single complete inference rule for PL: from (ℓ₁ ∨ … ∨ ℓₖ) and (m₁ ∨ … ∨ mₙ) where ℓᵢ and mⱼ are COMPLEMENTARY literals, infer the disjunction of all the remaining literals. RESOLUTION IS REFUTATION-COMPLETE: it can always derive a contradiction from an unsatisfiable set of clauses. So to prove KB ⊨ α: 1. convert KB ∧ ¬α to CNF 2. apply resolution repeatedly 3. if the EMPTY CLAUSE is derived, KB ⊨ α 4. if no new clauses can be derived and no empty clause appeared, KB ⊭ α A WORKED PROOF. KB: (1) P ⇒ Q (2) Q ⇒ R (3) P. Prove R. CNF of KB: {¬P, Q}, {¬Q, R}, {P} negate the goal: {¬R} resolve {¬P, Q} with {P} → {Q} resolve {Q} with {¬Q, R} → {R} resolve {R} with {¬R} → { } the EMPTY CLAUSE CONTRADICTION FOUND, therefore KB ⊨ R. ∎ THE EMPTY CLAUSE IS THE POINT: a clause is a disjunction, and a disjunction of nothing is false. Deriving it means the assumed premises cannot all hold. HORN CLAUSES — the restricted case that is efficient: A HORN CLAUSE has AT MOST ONE POSITIVE LITERAL. A DEFINITE clause has exactly one. Written as implications, definite clauses look like P₁ ∧ P₂ ∧ … ∧ Pₙ ⇒ Q which is the natural form of a rule. WHY IT MATTERS: inference with Horn clauses is decidable in TIME LINEAR IN THE SIZE OF THE KNOWLEDGE BASE, using FORWARD CHAINING or BACKWARD CHAINING. That is the difference between intractable and cheap, and it is why Prolog and every rule-based expert system are built on Horn clauses.

TWO DIRECTIONS OF REASONING with definite clauses: FORWARD CHAINING — DATA-DRIVEN Start from the known facts. Whenever all the premises of a rule are satisfied, add its conclusion. Repeat until the query appears or nothing more can be added. ✔ derives everything derivable, so it answers many queries at once ✘ may derive a great deal that is irrelevant to the query BACKWARD CHAINING — GOAL-DRIVEN Start from the query. Find rules concluding it, and try to prove their premises, recursively. ✔ touches only what is relevant to the query ✔ this is how Prolog works ✘ may re-derive the same subgoal repeatedly without memoisation, and can loop on recursive rules WORKED, on a small rule base: R1: A ∧ B ⇒ C R2: C ∧ D ⇒ E R3: A ⇒ D FACTS: A, B. QUERY: E? FORWARD: A, B known → R1 fires → add C A known → R3 fires → add D C, D known → R2 fires → add E. ✓ derived C, D, E — three new facts, all needed here BACKWARD: goal E → R2 needs C and D goal C → R1 needs A and B → both known ✓ goal D → R3 needs A → known ✓ therefore E. ✓ the SAME work here, because everything was relevant. In a knowledge base with 500 rules where only 3 matter, forward chaining would fire hundreds of irrelevant rules and backward chaining would touch 3. THE LIMITATIONS OF PROPOSITIONAL LOGIC — the reason first-order logic exists: 1. NO STRUCTURE INSIDE A PROPOSITION. "Socrates is a man" is a single symbol with no visible parts, so the logic cannot see that it is about Socrates or about men. 2. NO QUANTIFICATION, and this is the decisive failure. "All men are mortal" cannot be stated. It must be expanded into one sentence per man: Man(Socrates) ⇒ Mortal(Socrates) Man(Plato) ⇒ Mortal(Plato) … WITH n INDIVIDUALS AND m PREDICATES, a single quantified statement needs up to n SEPARATE SENTENCES, and a statement about pairs needs n². For 1,000 individuals, "everyone loves someone" would need 1,000,000 propositions to express what first-order logic says in eight symbols. AND IF THE DOMAIN IS INFINITE OR UNKNOWN, no finite expansion exists at all. 3. NO WAY TO REFER TO OBJECTS, so no functions and no equality. "The father of John" has no expression. 4. NO GENERALISATION. Learning that one bird flies tells the logic nothing about other birds, because there is no connection between the symbols. WHAT PL KEEPS, and it is not nothing: · DECIDABLE — satisfiability is always determinable, though NP-complete · a COMPLETE and practical proof procedure (resolution, DPLL, CDCL) · genuinely enormous practical scale in SAT solvers FIRST-ORDER LOGIC BUYS EXPRESSIVENESS AND PAYS WITH DECIDABILITY: FOL is only SEMI-decidable — if a sentence is entailed, a proof procedure will find it eventually, but if it is not, the procedure may never terminate. THAT IS THE EXPRESSIVENESS/TRACTABILITY TRADE-OFF ONCE MORE, in its sharpest form.