Finite forbidden-pattern axiomatization (source code)

= Finite forbidden-pattern axiomatization

If failure of a property has a finite witness, one can often axiomatize the property by a universal sentence forbidding each possible finite witness. Compactness supplies finite witnesses when failure is expressed by inconsistency of an associated theory.