Propositional logic¶
Algae is a tool for proving things, so before we prove anything we need a shared idea of what the things we prove are made of. This chapter is a quick refresher on classical propositional logic — the algebra of true/false statements. There’s no editor here and no Algae syntax; it’s just the ground the rest of the tutorial stands on. If it’s familiar, skim it.
A proposition is a statement that is either true (T) or false
(F). Write bare propositions with letters A, B, C. From simple
propositions we build compound ones with four connectives, and each
connective is defined completely by a truth table — what it does for every
combination of truth values of its parts.
Negation: ¬ (not)¶
¬A (“not A”) flips the truth value: it’s true exactly when A is
false.
|
|
|---|---|
T |
F |
F |
T |
Conjunction: ∧ (and)¶
A ∧ B (”A and B”) is true only when both halves are true.
|
|
|
|---|---|---|
T |
T |
T |
T |
F |
F |
F |
T |
F |
F |
F |
F |
Disjunction: ∨ (or)¶
A ∨ B (”A or B”) is true when at least one half is true. This is
the inclusive or — A ∨ B is still true when both are.
|
|
|
|---|---|---|
T |
T |
T |
T |
F |
T |
F |
T |
T |
F |
F |
F |
Implication: → (implies)¶
A → B (”A implies B”, or “if A then B”) is the one that
surprises people. It is false in exactly one case: when the premise A is
true but the conclusion B is false. Whenever A is false, A → B is
true regardless of B — a promise with a false premise is never broken.
|
|
|
|---|---|---|
T |
T |
T |
T |
F |
F |
F |
T |
T |
F |
F |
T |
A note on spelling
This chapter uses the conventional logic symbols. Three of them are exactly
how Algae writes them: ∧ (ASCII /\), ∨ (ASCII \/), and ¬
(ASCII ~). Implication is the exception: Algae reserves → for
function types, so it writes implication as ⇒ (ASCII =>). From the
next chapter on we use Algae’s spellings — read ⇒ as the → from the
table above.
Why truth tables aren’t enough¶
Truth tables decide propositional logic: to check whether a formula is always
true, you could grind through every row. But two things make that a dead end for
real proofs. First, the tables blow up — n letters means 2ⁿ rows.
Second, and more importantly, the moment we add variables and quantifiers
(“for every number n …”) there are infinitely many rows and no table to
grind.
So instead of computing truth values, Algae proves statements the way mathematicians do: by inference rules — small, fixed steps like “to prove a conjunction, prove each half” that chain together into a proof. Those rules, and how the kernel checks a chain of them, are the subject of the next chapter.