Refutable in something small

The middle that is not excluded has a completeness theorem in it: the constructive system proves exactly what holds in every Heyting algebra. Read as a decision procedure that is useless — every Heyting algebra is not a thing anybody checks.

What makes it a procedure is a second property, and it is not implied by the first.

The property, stated #

A logic has the finite model property when every formula it does not prove fails in some finite model. For the constructive system that means: a formula is a theorem exactly when it takes the top value at every valuation in every finite Heyting algebra.

The forward direction is the completeness theorem restricted. The other direction is the content: a non-theorem has a finite counterexample, so checking finitely many finite algebras is enough.

That turns the completeness theorem into a procedure. Given a formula, search algebras in increasing size; if one refutes it, it is not a theorem; and the property guarantees the search terminates on non-theorems. To decide theorems as well, a bound is needed — and there is one: a formula in $n$ variables that fails anywhere fails in an algebra of size bounded by a function of $n$, so the search can stop.

The search, run #

The figures build every order on up to four points, form the algebra of its downward-closed subsets, and evaluate each formula at every valuation. Twenty-three algebras, of sizes from two to eight, and the answers are exact.

Excluded middle fails in the smallest non-Boolean algebra there is, the three-element chain. Double negation removal fails in the same one, which is no surprise — the excluded middle records that the two are equivalent. The weak law needs five elements, and the algebra that does it has two incomparable atoms.

And three negations collapsing fails nowhere. That is the control and it is the important row: the formula is a theorem of the constructive system, so no algebra can refute it, and a search reporting a refuter would mean the algebras were built wrongly. A decision procedure needs to be right about theorems as well as non-theorems, and a search that only ever found counterexamples would be untested.

The figures also check what “smallest” means: for the refuted formulas, every algebra smaller than the one found is checked to validate the formula. Without that the search would be reporting the first refuter it happened to try.

What the smallest refuter says about the formula #

The size of the smallest refuting algebra is a measurement of the formula, and it is worth reading rather than passing over.

Excluded middle needs three elements: one element strictly between the bottom and the top is enough for $p \vee \neg p$ to fall short. That makes it the easiest non-theorem to refute, which matches its being the strongest of the candidate axioms — a strong axiom fails in almost everything.

The linearity axiom needs an algebra with two incomparable elements, so its smallest refuter is larger. And an axiom that fails only in algebras with a particular shape needs an algebra of that shape, so its smallest refuter is as large as the shape requires.

So the smallest refuter’s size is a rough measure of how weak the axiom is. A weak axiom holds in many algebras, so the search has to go further to find one where it fails. That is a coarse instrument and it orders the candidates correctly on the cases drawn, which is about as much as a single number can be asked to do.

It also says something about the search’s cost. The number of orders on $n$ points grows very fast — one, three, nineteen, two hundred and nineteen — so each extra point the search needs is expensive, and an axiom whose smallest refuter has ten elements is out of reach of the method entirely.

Why finite algebras suffice #

The proof of the property is a construction and its shape is worth knowing, because it says where the finiteness comes from.

Suppose a formula fails in some Heyting algebra. Only finitely many subformulas are involved, so only finitely many elements of the algebra are named by the failure — the values of the subformulas at the failing valuation. Those elements do not form a subalgebra, since the operations may leave the set. The construction is to take the finite set of elements they generate under the operations, and to show that if this is not finite, a quotient of it is: the filtration argument, which collapses the algebra along an equivalence that respects the finitely many subformulas.

What comes out is a finite algebra in which the same formula fails, with size bounded by a tower in the number of subformulas — and the finite algebras it produces are the downsets of finite orders, which is what every finite Heyting algebra is. The bound is enormous and its existence is the whole point — a bound of any size makes the search terminate, and the practical procedures do not use it.

The same argument works on frames rather than algebras and is easier to picture there. A Kripke model refuting a formula can be collapsed by identifying stages that agree on every subformula; there are finitely many subformulas, so finitely many classes, and the quotient is a finite frame refuting the same formula.

What the property is worth, and what it is not #

It gives decidability and not a usable algorithm. The bound from filtration is a tower of exponentials, so the search it licenses is not run. Practical decision procedures for this logic use proof search with loop checking instead, and they are still far more expensive than the classical case’s truth table — the problem is complete for polynomial space, against the classical case’s being in nondeterministic polynomial time.

It is not automatic. Plenty of logics lack it. The continuum of logics records that there are intermediate logics that are undecidable, and a logic without the finite model property has no search of this kind at all. So the property is a fact about this particular system rather than a consequence of having algebraic semantics.

And it does not survive quantifiers, which is the sharp limit and the subject of the section after next. Nor does it say anything about the intermediate logics that continuum holds: each of those has its own class of algebras, and whether a finite one suffices is a separate question with a separate answer for each.

How much room one variable has #

Before the limit, a measurement of how much structure the system has, and it is startling.

Classically there are exactly four formulas in one variable up to equivalence: $\bot$, $p$, $\neg p$, $\top$ — since a formula in one variable is a function from two truth values to two, and there are four. A truth table settles it, exactly as the syllogism’s 256 forms are settled by exhaustion.

Constructively there are infinitely many. That is Rieger and Nishimura’s theorem, from 1949 and 1960, and the figure measures a lower bound: generate formulas by nesting, separate them with the finite algebras, and count the classes. The count passes four immediately and keeps climbing.

The formulas doing it are the ones the classical reading collapses. $\neg\neg p$ is not $p$; $\neg\neg p \to p$ is not $\top$; $p \vee \neg p$ is not $\top$; and each of those can be combined with the others to give something new. The classes form a lattice — the Rieger–Nishimura lattice — which is infinite and has a completely explicit description, alternating between two infinite chains.

So the system is infinitely richer than the classical one at one variable. That is worth having beside the decidability: the logic is decidable and it is not small, and the two facts sit together because decidability is about a procedure terminating rather than about there being few things to decide.

Where the property fails #

Add quantifiers and everything above stops.

Intuitionistic predicate logic is undecidable. So is the classical predicate logic, which is Church and Turing’s theorem, and the constructive version inherits the undecidability through the double-negation translation the excluded middle describes: a classical formula is provable exactly when its translation is, so a decision procedure for one gives one for the other — which is the translation working as a reduction rather than as an interpretation.

And the finite model property fails too, separately and more sharply. There are formulas of intuitionistic predicate logic that fail in some model and fail in no finite one, so no search over finite structures decides even the non-theorems. The classical predicate logic has the same failure for the same reason: a formula can be satisfiable only in infinite structures.

That is the price an earlier essay records as the trade the whole field is organised around — “expressive power for decidability” — arriving here with the finite model property as the thing lost. The propositional system has it, is decidable, and cannot express a relation; the predicate system can express relations, lacks the property, and is undecidable.

The classical case, for comparison #

It is worth setting the classical decision problem beside this one, because the two are decidable for reasons that look alike and are not.

Classically, a formula in $n$ variables is a theorem exactly when it takes the value true in the one two-element algebra at all $2^n$ valuations. So the class of models needed is a single algebra, the search is over valuations rather than algebras, and the procedure is a truth table — which is the object a formula as a corner of a cube is about.

Constructively, one algebra will not do: no finite Heyting algebra validates exactly the theorems, because any single algebra validates some non-theorem. So the search has to range over algebras as well as valuations, and the finite model property is what bounds the first range.

That is the difference between the two decision problems and it is why one is in nondeterministic polynomial time and the other is complete for polynomial space. Both are decidable; one decides by evaluating a formula many times in a fixed structure, and the other by evaluating it in many structures.

The comparison also explains why the constructive system has infinitely many formulas in one variable and the classical one has four. Four is the number of functions from a two-element set to itself; infinitely many is what happens when the structures are not fixed, and a formula can differ from another in some algebra and not in the two-element one.

What the pictures cannot show #

The search runs over orders on at most four points, which is twenty-three algebras of at most eight elements. A formula needing a larger algebra to refute it would be reported as having none found and called a theorem, which would be wrong — so the figures are honest only for formulas whose refuters are small, and the ones drawn are chosen accordingly.

That is a real limitation and it is the shape of every exhaustive search in this collection. What the figure establishes is the answer for the formulas and algebras it covers; the procedure’s correctness is the filtration bound, which is a tower of exponentials and not a number any search reaches.

And the count of formulas in one variable is a lower bound at every depth. Two formulas the finite algebras agree on may still be separated by a larger algebra, so each bar is a floor rather than the count; the infinitude is a theorem and the bars are what a search can see of it.

The lattice the one-variable formulas make #

The infinitude of one-variable formulas has a structure and it is worth describing, because an infinite set of classes with no pattern would be less interesting than one with a pattern.

Order the classes by implication: $A \le B$ when $A \to B$ is a theorem. The resulting lattice starts at $\bot$ and $p$, and above them it splits: $\neg p$ and $\neg\neg p$ are incomparable, their join and meet give two more, and the pattern repeats — at each level two incomparable classes whose join and meet feed the next level, converging upward on $\top$.

Explicitly, the classes are generated by the formulas $g_1 = p$, $g_2 = \neg p$, and $g_{n+2} = g_{n+1} \to g_n$, which alternate between the two sides of the lattice. The whole of it is described by that recursion, and the infinitude is the statement that no two of the $g_n$ are equivalent.

So the answer is not merely “infinitely many” but a lattice with a three-line description, which is the situation the classical case’s four is a degenerate version of. Setting the lattice’s negations equal to their double negations collapses it to four classes, and that collapse is what excluded middle does.

The topological reading is the one the figure shows. In the algebra of open sets of a line, the formulas $g_n$ applied to a set with several holes give a strictly increasing family of open sets, and the increase does not stop — which is the same infinitude seen in a model rather than in a syntax.

Still open: how large a refuter has to be #

The filtration bound is a tower and the truth is much smaller, and how much smaller is not settled.

For a formula in $n$ variables the known upper bounds on the smallest refuting algebra are exponential in the number of subformulas, and the known lower bounds are much weaker. Closing that gap would be a statement about the logic’s complexity and is related to the exact complexity of the decision problem, which is known to be complete for polynomial space and whose practical difficulty is not well characterised.

The related question concerns the intermediate logics. Some have the finite model property and some do not, and no characterisation of which is available; there are logics known to be decidable without having it and logics known to lack it and be undecidable. The map of which properties imply which across the continuum these logics form is incomplete in most directions.

And the one-variable case’s tidiness does not extend. The lattice of formulas in one variable is completely described; in two variables the lattice is infinite, is not known to have any similarly explicit description, and its structure is a subject in its own right.

What a bound would have to look like #

One more remark on the filtration bound, because its size is the gap between the theory and the practice.

The bound is a tower of exponentials in the number of subformulas, and the algebras that actually refute the formulas anybody writes down have a handful of elements. So the guarantee and the observation are many orders apart, and nothing in the argument closes the gap: filtration collapses an arbitrary refuting algebra and has no way to know that a small one exists.

A better bound would need a construction rather than a collapse — a way of building a small refuter from the formula’s structure instead of shrinking whatever refuter happens to be available. For the propositional system such constructions are known in special cases and not in general, which is why the practical procedures abandon the algebras altogether and search for proofs instead.

What made a semantics into a procedure #

A completeness theorem says a system proves what holds in a class of models. On its own that is a statement about the system’s reach and not a way of deciding anything, because the class is infinite and its members may be too.

The finite model property is the second ingredient and it is what makes the theorem operational. A non-theorem with a finite counterexample can be refuted by a search, and a search that terminates is a decision procedure. The property is not implied by completeness, has to be proved separately, and fails for closely related systems.

Which suggests the question to ask of any semantics. Not is the system complete for this class — that is the first thing anybody proves — but does a failure have a small witness. If it does, the semantics is a procedure; if it does not, the semantics is a description, and the decision problem needs a different idea entirely.