There’s really one zeroeth order logic. We saw a few different languages, differing in precisely which Boolean operators they allowed, and different sets of axioms and rules of inference, but any statement expressible in one of these languages was also expressible in any of the others and the translated version was a theorem in the new system if and only if the original version was a theorem in the old system, although I don’t claim this is obvious.
First order logic is not as not as unified as zeroeth order logic. There are concepts which appear in some varieties of first order logic but which are absent in others, and aren’t even expressible in them. An example is the concept of equality. Some variants of first order logic have an “=” symbol and axioms or rules of inference governing its use. Others don’t have an “=” symbol. This isn’t like zeroeth order logic though, where some variants have a “⊃” symbol and others don’t, but can express the same meaning with a combination of other symbols. First order logic without equality is simply incapable of expressing the notion of equality with any combination of symbols. If you want to use first order logic as the foundation for a subject with a notion of equality, like arithmetic, then you need to add axioms or rules of inference to deal with the “=” symbol, just as you to with, for example, the “+” symbol. If you use first order logic with equality then you don’t have to do this, since “=” already belongs to the logic, just like Boolean operators or quantifiers.
Unfortunately, even where different variants of first order logic use the same language they may differ in the interpretations they allow, and therefore in which statements are considered valid, i.e. true in all interpretations. One important point of contention is whether all parameters are assumed to refer to actually existing objects of the appropriate type. If you decide that they are, and build a system for arithmetic on top of it in the way that we will, allowing numerical expressions to be substituted for parameters in any valid statement from first order logic, then you have to be very careful to make sure that every expression your language allows you to write down will always refer to a number no matter what numerical values are assigned to its variables. Unfortunately that means you have to avoid introducing things like a division sign, since \({ m / n }\) won’t exist for some choices of \({ m }\) and \({ n }\).
Most logic textbooks introduce a form of logic without equality but with existential presuppositions, i.e. with the tacit assumption that every parameter refers to some existing object of the appropriate type. When I say that this assumption is tacit I mean that it’s not made explicit but the axioms and rules of inference are not sound if it’s violated.
Mathematicians rarely specify the underlying logic of their systems but if you look at what they do you’ll see that the foundation is usually a logic with equality and without existential presuppositions. They won’t introduce extra axioms or rules of inference for “=”, just as they don’t for Boolean operators or for quantifiers. They will introduce symbols like “/” despite the fact that this allows us to write down expressions which may not refer to any existing object.
If I were writing a text where logic was the main subject of study rather than mostly a foundation for other theories I might discuss several different variants of first order logic and explore their differences but we don’t have time for that and so I’ll pick one, the one closest to actual mathematical practice: first order logic with equality and without existential presuppositions. This introduces extra complications into the logic, compared to a logic without equality and with existential presuppositions, but makes using as a foundation for other theories both easier and safer. The specific system described below is in essence due to Jaakko Hintikka.