Some logicians write Rabc to mean the application of the predicate R to the terms a,b, and c. Others write R(a,b,c). We prefer the latter. The Colin Howson book uses a notation like R(a,b,c) for the application of a predicate R to the arguments or terms a, b, c. It employs the upper case letters A-Z, perhaps followed by subscripts, to be predicates, so, for example, R, S₁, T₁2 are all predicates. The software supports this.
But the software makes an extension. Often, when working informally, authors will write Red(x) to mean that the predicate Red is applied to the variable x.
The software will accept this also (with these new style of predicates also optionally followed by subscripts). So Red, Soft₁, Tiger₁2 are all predicates. The rule or convention here is that the first letter of a predicate is upper case, then any sequence of upper or lower case letters can follow, and the predicate can be completed with subscripts. So 'AVeryLongPredicate' is a predicate.
A similar approach is applied to constant terms or functions, only this time, the term must start with a lower case letter ie [a--v]. So aFunctionAppliedToATerm(aTerm) is a perfectly good term of the form f(a).
Variables, though, consist of lower case [w-z] only, optionally followed by subscripts [ie there can be no sequence of upper or lower case letters in between].
So the argument. Socrates is a man, All men are mortal, therefore, Socrates is mortal can be symbolized
M(s), ∀x(M(x)→M₂(x)) ∴ M₂(s)
But, the software will also accept
Man(socrates), ∀x(Man(x)→Mortal(x)) ∴ Mortal(socrates)