 Let us consider an example of how a particular formula would be found to be either satisfiable or its negation provable, following Gödel’s method: Consider φ = ∀x0∃x1ψ(x0, x1), where ψ(x0, x1) is quantifier-free. We show that this is either refutable or satisfiable. We make the following definitions: