Assume a metatheory that supports lambda-abstraction, and an object language that is merely first-order. Now let $\varphi$ denote a formula in the object language with one free variable $x$. Then we can write $\lambda x. \varphi$ in order to mean the function that accepts an expression $E$ in the object language and returns the formula $\varphi[x/E].$ Hence $\lambda x. \varphi$ works just like a predicate symbol. For example, if $P$ is a predicate symbol in the object language and we let $Q$ equal $\lambda x.\varphi$, then $\forall y(Py \rightarrow Qy)$ is a well-formed formula, despite that $Q$ is not a predicate symbol.



> 
> **Question.** What do we call functions (like $\lambda x. \varphi$) that behave like predicate symbols?
> 
> 
> 


For example, in the following sentence, what word should go in place of [///]?



> 
> Let $Q$ denote the [///] $\lambda x.\varphi.$
> 
> 
> 


Obviously, the word "function," but its not really a good fit, being far too general.



What do we call functions that behave like predicate symbols?
I would call such a thing *propositional function*.


