I know only logics whose predicates and functions accept terms as arguments and all the modal operators are defined at the logical level and only modal operators and connectives can accept sentences (propositions, formulas) as arguments, usual functions and predicates cannot do this.
But are there efforts to create logics with user-defined modal operators, effectively - logics which allow users to define functions (e.g. to act as polyadic modal operators) that can accept sentences (propositions, formulas) as arguments and that allow users to define (and fine-tune) non-logical axioms on such user-defined functions?
Such feature would be essential for formal semantics of natural language. Of course, the verb BELIEVE(subject, sentence) can be modeled as a usual modal operator in doxastic logic, but there can be many more shades of belief modality e.g. subject, web tense, degrees of belief strength and so on. Clearly to capture all those possibilities one should move the definition of modal operators from the logical language to the non-logical language (where the usual functions reside).
So - are there efforts to define and research such logics?
I am aware of the book https://www.springer.com/gp/book/9783319225562 "Toward Predicate Approaches to Modality" whose opening chapter states, that modality could be modeled as the predicate on the sentence name (sic! - sentence name)! I am still studying this book, maybe it will provide a solution for me.
In another forum, I received a suggestion to have a look in modal type theory, where this difference between function and modal operator disappears...