Proving that nothing is allowed

A refutation proves that a system allows nothing. Its degree says how much it holds at once.

From John Cullen’s knotlab guide

Refutations. When a system allows no state at all, a refutation is a proof of that fact: a sequence of steps, each of them following from the rules, that ends in a contradiction. Proof systems differ in what one step may do, and the cost that matters here is how much a single step must hold at once.

Proofs by algebra. Algebra gives the proof system that the next lesson uses.

Rules become equations. Each variable x obeys x·x = x, so its only values are 0 and 1. A clause becomes a product that is 0 exactly when the clause holds: ¬A ∨ ¬B ∨ c becomes A·B·(1 − c) = 0, since the product is 1 at 110 and 0 everywhere else.
A Nullstellensatz refutation multiplies each equation by some polynomial and adds the results so that everything cancels except the number 1. No state can make every equation 0 and the sum 1, so nothing is allowed. Its degree is the largest degree among the products it adds: roughly, the most variables it must multiply together in one term. A refutation of low degree sees the contradiction through small windows. Classical: the Nullstellensatz proof system (Beame, Impagliazzo, Krajíček, Pitassi and Pudlák 1996).
The numbers matter. The coefficients come from a field: a number system with addition, subtraction, multiplication and division, such as the rational numbers or arithmetic mod a prime. A field has characteristic 2 when 1 + 1 = 0 in it, as in arithmetic mod 2, which is the arithmetic of parity. The rational numbers, and arithmetic mod 3 or mod 5, have other characteristics.