Predicate calculus of arbitrarily high finite order. M.W. Bunder (1983) Archiv für mathematische Logik und Grundlagenforschung