Chromatic Fantasy & Feud & Topic VII — The Propositional Calculus

Core idea

The propositional calculus is the first formal system in the book powerful enough to capture real logical reasoning. Its alphabet contains symbols for atomic propositions (P, Q, R), parentheses, and five logical connectives: negation (~), conjunction (∧), disjunction (∨), implication (⊃), and biconditional (≡). Its axioms and inference rules are designed so that the theorems are exactly the tautologies — sentences true under every assignment of truth values to the atoms.

The system is sound (every theorem is a tautology) and complete (every tautology is a theorem) — a result for propositional logic that gives, in miniature, the goal Hilbert hoped to achieve for all of mathematics. The miracle is that the system achieves both promises. The disappointment, to be deferred until Topic IX, is that no analogous system achieves both for arithmetic. Propositional logic is too weak to talk about itself, which is exactly why it can be both consistent and complete.

Hofstadter's argument: The propositional calculus is the high-water mark of the formal-system program: a system whose syntactic theorems coincide exactly with its semantic truths. Topic IX will reveal that this match is unique to weak systems. For the moment, marvel at what it shows is possible.

Why it matters

The connectives and their semantics

Each connective has a fixed truth-table semantics:

• ~P is true when P is false.
• P ∧ Q is true when both are true.
• P ∨ Q is true when at least one is true.
• P ⊃ Q is true unless P is true and Q is false (this is material implication, the source of countless undergraduate frustrations).
• P ≡ Q is true when both have the same truth value.

A tautology is a sentence true under every assignment of truth values to its atoms — P ∨ ~P (excluded middle), (P ∧ Q) ⊃ P (conjunction projection), (P ⊃ Q) ⊃ ((Q ⊃ R) ⊃ (P ⊃ R)) (hypothetical syllogism). The propositional calculus has the same theorems as truth-table tautology, but proves them by syntactic manipulation rather than truth-table inspection. For long formulas with many atoms, truth tables become exponential; proofs can stay polynomial. This is the engineering motivation.

The inference rules

Hofstadter uses a small set of inference rules that include modus ponens (the central rule: from P and P ⊃ Q infer Q), the fantasy rule (Hofstadter's term for what logicians call conditional proof — start a "fantasy" with an assumption, derive consequences, exit by writing assumption ⊃ conclusion), the carry-over rule (anything proved in an outer fantasy can be used in an inner fantasy), the rule of detachment for biconditionals, and rules for managing negations (double negation, de Morgan).

The "fantasy rule" is pedagogically central. To prove P ⊃ Q, you open a fantasy by writing "suppose P," derive Q from P and the system's other axioms, then close the fantasy with P ⊃ Q. This is how mathematicians actually argue — suppose for contradiction, suppose P holds, consider the case where — and the fantasy rule makes it formal. Fantasies can be nested: a fantasy inside a fantasy.

Soundness and completeness for propositional logic

Soundness: if a sentence is a theorem of the calculus, then it is a tautology. Easy to prove — verify that each axiom is a tautology and that each inference rule preserves tautology-ness.

Completeness: if a sentence is a tautology, then it is a theorem of the calculus. Harder, but provable (the standard proof uses Henkin's argument or a normal-form decomposition). The combined result is that the syntactic notion of "theorem" exactly matches the semantic notion of "truth in every model" for propositional logic.

This is a stunning fact. It means that propositional reasoning is mechanizable: a computer can, in principle, decide whether any propositional formula is a tautology by trying proofs (though the decision problem is NP-complete in the worst case, so practical decidability requires heuristics). Hilbert wanted this for arithmetic. Topic IX will show why he could not have it.

The Chromatic Fantasy & Feud as a meta-dialogue

The Chromatic Fantasy & Feud dialogue plays on the word "fantasy" — Bach wrote a Chromatic Fantasy and Fugue (BWV 903); Hofstadter has been about to formalize the "fantasy rule" of propositional logic; and the dialogue is itself a kind of nested-context game in which Achilles and the Tortoise argue about a piece of music inside their conversation. The dialogue ends with the characters debating whether you can have a meaningful fantasy that contains a contradiction — a meta-question that will be sharpened when we get to Gödel.

Why this system is safe to be both consistent and complete

The propositional calculus has one property that arithmetic lacks: it cannot quantify over its own propositions. You can write P and Q but you cannot write "for all propositions X, X ∨ ~X holds" — that would require a quantifier ranging over propositions, which propositional logic does not have. First-order logic adds quantifiers over individuals (predicate calculus is also sound and complete for predicates over individuals, by Gödel's completeness theorem of 1929). Second-order arithmetic adds quantifiers over sets of individuals (and is no longer complete — Gödel's incompleteness theorem of 1931). The added expressive power of quantification over sets is what breaks the promise. Propositional logic stays safe by staying small.

Key takeaways

Mental model

Copy sourceZoom

Practical application

The propositional calculus is the formal counterpart of everyday inference. Train yourself to map ordinary reasoning onto its skeleton.

1. Identify the atomic propositions. A proposition is a statement that can be true or false: "the patient has fever," "the bridge is overloaded," "the deploy succeeded." Pick atomic propositions for the statements that vary independently in the argument.

2. Identify the connectives. Translate "and," "or," "if-then," "not," "if and only if" into ∧, ∨, ⊃, ~, ≡. Watch for vague connectives that hide the structure: "because" usually means ⊃; "unless" means ~A ⊃ B or equivalently A ∨ B.

3. Check if the argument form is a tautology. Replace the atoms with letters and see if the resulting formula is true under every assignment. If yes, the argument form is valid. If not, find an assignment that falsifies it — that is your counterexample.

4. Beware material implication's traps. P ⊃ Q is true whenever P is false — which means "if pigs fly then 2 + 2 = 5" is a true propositional sentence. The propositional calculus's "implication" is weaker than natural-language "if-then"; many real arguments depend on a stronger reading. When the natural-language argument seems valid but the formal version is not, suspect that the implication is doing more work than material implication can carry.

Example

Consider a security argument: "Either the password is correct or access is denied. The password is not correct. Therefore access is denied." Atomic propositions: P = "password correct," D = "access denied." Premises: P ∨ D, ~P. Conclusion: D. This is the propositional form of disjunctive syllogism, and the calculus proves the corresponding tautology ((P ∨ D) ∧ ~P) ⊃ D.

Now consider a security argument that looks the same but is not: "Either the password is correct or access is denied. Access is denied. Therefore the password is not correct." Premises: P ∨ D, D. Conclusion: ~P. The propositional form is ((P ∨ D) ∧ D) ⊃ ~P. Is this a tautology? Try the assignment P = true, D = true. The premises are both true; the conclusion ~P is false. So the argument form is invalid — even though the premises sound reasonable, you cannot conclude ~P from them.

The mistake in the second argument is the "inclusive or": P ∨ D allows both. The argument is treating it as exclusive (P xor D), which would make the inference valid. Translating into the calculus catches this; everyday intuition often does not. Most logical errors in software, in legal reasoning, in policy debates, are detected only by writing out the inference in propositional form and checking for a tautology.

The propositional calculus is, at bottom, a tool for checking whether what you have just argued is actually valid. The fact that it can do this and be both sound and complete is one of the foundational results of modern logic — and a measure against which Topic IX's incompleteness theorem will land with its full weight.

Related lessons