 Following is a Hilbert-style formalism \(\mathbf{H–IQC}\) from Kleene [1952] (cf. Troelstra and van Dalen [1988]) for intuitionistic first-order predicate logic. The language \(L\) of \(\mathbf{H–IQC}\) has predicate letters \(P, Q(.), \ldots\) of all arities and individual variables \(x, y, z, \ldots\) (with or without subscripts \(1, 2, \ldots\)), as well as symbols \(\oldand, \vee , \rightarrow , \neg , \forall , \exists\) for the logical connectives and quantifiers, and parentheses (, ). The atomic (or prime) formulas of \(L\) are expressions such as \(P, Q(x), R(x, y, x)\) where \(P, Q({.}), R({.}{.}{.})\) are \(0\)-ary, \(1\)-ary and \(3\)-ary predicate letters respectively; that is, the result of filling each blank in a predicate letter by an individual variable symbol is a prime formula. The (well-formed) formulas of \(L\) are defined inductively as follows: