What the theorem shows is that there are statements that can be formulated within the standard axiom system for arithmetic but which cannot be proved true or false within that system.

It is also possible to represent values of cells as True and False .

And in 1963 Alan Robinson suggested the idea of resolution theorem proving, in which one constructs ¬ theorem ∨ axioms , then typically writes this in conjunctive normal form and repeatedly applies rules like ( ¬ p ∨ q) ∧ (p ∨ q)  q to try to reduce it to False , thereby proving given axioms that theorem is True .