If you are new to logic, you can skip this. It is an explanation of the notation we are going to use and why.
The various logical systems can use Rabc or R(a,b,c) to symbolize the application of the predicate R to the arguments a, b, c. Often, when working informally, authors and Users would like to write Red(x) to mean that the predicate Red is applied to the variable x. We can do this within the formal system only if we choose the R(a,b,c) style of notation (because you have to be able to tell when the predicate stops and when the arguments start).
So we will use the R(a,b,c) style.
With quantifiers, one might have brackets around them or not eg. (∀x) (∃x) or ∀x ∃x . There does not seem to be any reason to have extra parantheses, there are more than enough parantheses in these formulas anyway. So we will go with the bracket-free style.
And for the propositional connectives we'll use ~, &, v, →, ≡ . There are not many arguments pro or con here. We're looking for a balance between what can be understood, what can be typed from a keyboard, and what is most common or a standard. The parsers in the software will read and parse correctly any alternatives; but when they write back to you, they'll do so with these symbols.
So, here is a typical formulas
The software employs the upper case letters A-Z, perhaps followed by subscripts, to be predicates, so, for example, R, S₁, T₁2 are all predicates.
But the software permits an extension.
The software allows us to write Red(x) to mean that the predicate Red is applied to the variable x (and these new style of predicates can also optionally be 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)