In 1979, IBM’s System R — one of the first relational database systems — introduced a component that would define database architecture for the next four decades: the query optimizer.
The optimizer’s core insight was this: the SQL query a programmer writes is not the query that gets executed. The optimizer rewrites it. The rewritten query and the original query must return identical results — they are logically equivalent. But the rewritten query can be orders of magnitude faster because it exploits indexes, avoids full table scans, and minimizes intermediate result sizes.
Every major database today — PostgreSQL, MySQL, Oracle, SQL Server — runs a query optimizer. Every time you execute a SQL query, the optimizer performs logical equivalence checking. It asks: “Is this expression equivalent to that one?” If yes, and if the second form is cheaper to execute, it substitutes.
The optimizer is an automated logical equivalence checker.
This is not a trick specific to databases. The same principle appears in compilers (constant folding, dead code elimination), hardware synthesis (circuit minimization), and type systems (proof checking). Anywhere that two representations of a computation can be shown to always produce the same result, equivalence enables substitution — and substitution enables optimization.