Aristotle could say "all" and "some" of one class; Boole could turn a class into 0 or 1. Neither could say "everyone loves someone" — a claim about a relation with two nested "everys". In 1879 Frege built the missing machinery: bound variables and the quantifiers ∀ and ∃. And it is runnable: fix a tiny world of four things, draw a relation between them, and every quantified sentence becomes decidable by finite search. Down the center, data flows — the world and the sentence go in, the engine searches, TRUE/FALSE comes out. The blue team builds and defends it; the red team tries to break it.
source Frege, Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens (Halle: Nebert, 1879) — archive.org/details/11388662. Rendered, not quoted.
A quantifier over a finite domain is just a loop. ∀x φ = φ holds for every element — an AND over the four rows. ∃y φ = φ holds for at least one — an OR. Nesting them, order and all, is the whole engine:
For the current relation R, per element e of {a,b,c,d}:
| e | ∃y R(e,y) loves someone | ∀x R(x,e) loved by all | R(e,e) self |
|---|
∀x∃y is "every row has a green"; ∃y∀x is "some column is all green". They are not the same — that gap is Frege's discovery.
the-syllogism (Aristotle) reasons about classes; the-algebra (Boole) turns each class into a 0 or 1. Both are trapped in one level of generality — a single subject, a single predicate.
"Everyone loves someone" needs a two-place relation and two quantifiers whose order matters. No syllogism, no Boolean equation can state it. Frege's 1879 bound variable is the hinge: it lets a name be quantified twice over. Each sphere is the next one's premise — this is the one that finally escapes the frame.
The blue team's live check: re-evaluate the engine on reference worlds whose answers are known cold, and confirm each. If red tampers with a quantifier, this badge is where it shows.
Two inputs feed the engine. (1) The domain: a finite world of four things, D = {a, b, c, d}. (2) The relation: a 4×4 truth table R(x,y) — read it as "x loves y". A cell lit means the pair holds; you edit it below.
On top of that, a sentence built from ∀, ∃, the variables x,y, and the atom R(x,y). Truth is not stored anywhere — it is computed by searching every x and y in D. Four things means at most sixteen atoms to check: small enough to decide by hand, which is exactly why it is a good witness.
R(x,y) — "x loves y". Row = x (lover), column = y (loved). Click to toggle.
Toggle any cell or pick any sentence — the verdict is searched over D on the spot, never looked up.
What the machine produces, proven: for any of the 65,536 possible relations R and any of the four sentences, a TRUE/FALSE decided by finite search — cross-checked against an independent brute force over the whole 4-element domain. The current verdict is above; the guarantee that the search is correct is the output.
The blue team's witness (left) confirms the engine on known worlds live; the red team (right) tries to make it lie.
This toy also cheats on scale: over a finite domain every quantified sentence is decidable by brute force. Over an infinite domain that guarantee collapses — first-order validity is only semi-decidable (Church, Turing, 1936). The machine is honest about being finite.
"∀x∃y and ∃y∀x say the same thing." Cut. They are the whole point of the distinction — the engine shows a world where the first is true and the second false. Order of quantifiers is not decoration.
"Frege founded logic on a solid ground." Cut. His later system's unrestricted comprehension was inconsistent — Russell's paradox (1902) broke it. The quantifier survives; the naive set theory did not.
"Frege alone invented quantification." Kept, corrected. Frege 1879 was first, but C. S. Peirce and O. H. Mitchell reached quantifiers independently (~1883). Priority, not sole authorship.
The red team's move: swap the two quantifiers in sentence (1) so the engine computes ∃x∀y instead of ∀x∃y. The blue team's witness (window 7) knows ∀x∃y is TRUE on the identity world — it is watching.
Swap the quantifiers and formula (1) computes ∃x∀y. On the identity world "everyone loves someone" is genuinely true, but "someone loves everyone" is false — the witness recomputes, disagrees with known truth, and turns red. Nothing is faked; the attack is real and it is caught.