Above we spoke of a first-order language appropriate for a structure \(\langle\bD, \bR_1, \ldots, \bR_n\rangle\), enhanced with clauses, but these clauses were only shown via examples. Here is a proper definition. The Lower Predicate Calculus with Reflection (LPCR) for \(\langle\bD, \bR_1, \ldots, \bR_n\rangle\) is the language built up using the machinery of ordinary first-order logic with equality, together with the following formation clause. If \(\phi_0\), \(\phi_1\), …, \(\phi_k\) are formulas and \(P_1\), …, \(P_k\) are (new) auxiliary relation variables, the following is a formula.