Я в книгах тоже

не встречал, но понимание по аналогии с

получилось адекватным.

Что интересно, именно записи

всегда можно однозначно сопоставить определениям предикатных символов, а вот запись

уже, как выше упоминалось, не любому определению функционального символа соответствует, так что, по идее, первый значок должен быть более распространён. С другой стороны, странно, что они оба довольно в ходу, потому что ведь и так будет ясно, что определяется (даже если новый символ явно не выписали — он же новый, его можно в определяющей формуле легко найти глазами). Ну ладно, против избыточности языков я ничего не имею, пусть остаётся.
