Full Idea
'Predicate abstraction' is a key idea. It is a syntactic mechanism for abstracting a predicate from a formula, providing a scoping mechanism for constants and function symbols similar to that provided for variables by quantifiers.
Gist of Idea
'Predicate abstraction' abstracts predicates from formulae, giving scope for constants and functions
Source
M Fitting/R Mendelsohn (First-Order Modal Logic [1998], Pref)
Book Reference
Fitting,M/Mendelsohn,R: 'First-Order Modal Logic' [Synthese 1998], p.-1