Propositional Logic

1Propositions and the knowledge base

A proposition is a claim that is definitely true or false: 'the ground is wet', 'this transfer exceeds the limit'. No third value and no matter of degree — that severity is a design choice, and it is what will later make guarantees possible.

Commands, questions and open formulas ('x > 3' with x unbound) are not propositions: there is no truth value to reason about.

A knowledge base (KB) is a set of propositions a system has accepted as true — its committed picture of the world. Everything in this topic and the next is machinery for one question: given what the KB accepts, what else must be true? The word 'must' is the whole subject.

2Four connectives, fixed meanings

Compound claims are built from atomic ones by four connectives, each with one fixed meaning that never depends on subject matter: \neg p (not), p \wedge q (and), p \vee q (or), p \to q (if-then).

A rules engine treats 'over limit implies block' exactly as it treats 'rain implies wet' — the machinery sees the shape of the claim, never its topic. That indifference is the feature: it is what lets one evaluator serve every domain.

Precedence mirrors arithmetic: \neg binds tightest, then \wedge, then \vee, then \to; parentheses override all of it.

3Worlds and models

A world (an interpretation) assigns true or false to every atom — one complete way things could be. Two atoms, rain and wet, give exactly four worlds; n atoms give 2^n.

A model of a formula is a world that makes the formula true. 'Model' is a technical word here and a load-bearing one: satisfiability, validity and — next lesson — entailment are all statements about which worlds are models of what.

The exponential count is not a footnote. It is why brute-force reasoning dies around thirty atoms, why SAT solvers exist, and why the enumeration procedure in the next topic is a definition of correctness before it is a practical algorithm.

Figure. Every box is one complete way things could be: an assignment of true or false to each atom. Formulas do not create worlds; they carve this fixed set into models and non-models.

4The conditional, precisely

'If p then q' is a promise about one specific failure: it is false exactly when p is true and q is false, and true in every other world.

The rows that surprise everyone are the false-premise rows. 'If it rained, the ground is wet' is not broken by a dry sunny day — nothing was promised about days without rain. A rule you have never triggered is a rule you have never broken.

This is why p \to q says exactly what \neg p \vee q says, and why a knowledge base full of rules stays true in worlds where no rule fires. Safety rules in deployed systems inherit the same reading: a limit that never triggered was never violated.

Figure. The full truth table for p \to q, one row per world: a single row falsifies it — true premise, false conclusion — and both false-premise rows come out true, because an untriggered promise is an unbroken one.

Reading the arrow

1. A promise, not a causep \to q claims only this: you will not find p true with q false. No causation and no relevance — just that one excluded combination.
2. One way to break itFind a world with p true and q false. That world, and only that world, falsifies the conditional.
3. Untriggered is unbrokenIn every world where p is false the promise was never tested, so it stands — the two rows that read strangest in the table.

Coding lab. Print the truth table for p -> q runs in the app, with checks on your output.

5Evaluating a formula in a world

A formula gets its truth value from a world by recursion: look the atoms up, then apply the connective tables from the inside out. There is no judgement anywhere in the procedure — which is the point, since that is what lets a program do it.

The shape of the computation is the formula's own parse tree: values enter at the leaves and one value comes out at the root.

Everything later — model checking, satisfiability, the entailment lab in the next topic — is this loop run over many worlds. Make it reflexive on one world first.

Figure. The parse tree of the formula 'if rain then wet, and not rain', evaluated bottom-up in the world rain = false, wet = true: atom values enter at the leaves, each connective applies its table, and a single value leaves the root.

Inside out

1. Atoms firstThe world hands every atom its value: here rain = false, wet = true.
2. Connectives nextEach connective combines already-known values by its table: the conditional comes out true (false premise) and the negation comes out true.
3. Root lastThe top connective combines the two: true AND true — the formula holds, so this world is one of its models.

6Satisfiable, valid, unsatisfiable

Three classes cover every formula. Satisfiable: true in at least one world. Valid (a tautology): true in every world. Unsatisfiable: true in none.

The classes interlock: \varphi is valid exactly when \neg\varphi is unsatisfiable, so one honest check buys the other. Every later reduction of the shape 'to prove it, refute its negation' is this line.

Deciding satisfiability is SAT — the first problem ever proved NP-complete. Modern SAT solvers nonetheless crack industrial instances with millions of clauses, which is why hardware and software verification tools encode 'can my system reach a bad state?' as a satisfiability question.