 We require that the rules of inference, and the definitions of meaningful formulas and axioms, be constructive; that is, for each rule of inference there shall be a finite procedure for determining whether a given formula \(B\) is an immediate consequence (by that rule) of given formulas \(A_1, \ldots, A_n\) and there shall be a finite procedure for determining whether a given formula \(A\) is a meaningful formula or an axiom. (Gödel 1934, 346)