We consider a logical system in which the second order terms can be also used as first order terms. As a consequence, predicates can be taken as arguments of another predicate. In other words, a predicate can refer to predicates. The proposed framework seems very different from the tradition of formal logic which has been developped since Aristotle, where the distinction between the predicates and the individuals are essential. While in the traditional (Aristotelean) logical language a typical and basic sentence is of the form, e.g., Love(Socrates, Phaidon) "Socrates loves Phaidon", in our proposed language we could also express e.g., Love(Socrates, Love), Socrates "loves (the idea of) love", (which can be also express as Love(Socrates, λx, y. Love(x, y) by the usual η-conversion), or a sentence Love(God, λx ∀y Love(x, y)), "God loves (the idea of) loving everyone", or a predicate on x such as Love(x, λy Love(x, y)), "x loves x's own love". The purpose of this note is to give some proof-theoretic properties of the proposed logic; in particular, the strong normalizability is shown by slightly modifying Girard's strong normalizability proof for the traditional higher order logic. The use of this proposed logical language for the analysis of "self-references" and "intensionality" as Well as a connection with natural language semantics is discussed in Okada", and the connection with mobile communication processes and with linear logic are discussed in Okada.