Why is first-order logic defined as a collection of formal systems?

Question

I think I understand what a formal system is and what formal languages are. But I have trouble grasping why first-order logic is referred to as a collection of formal systems whereas propositional calculus is considered just a formal system. What makes the difference? What is the reason behind this definition? What does "a collection of formal systems" mean?

Answer 1

FOL is the "natural" logic environment to formalize mathematical theories.

Propositional calculus, instead, is only a "toy": it is based on a very simplified "model" of language that is not useful to develop interesting theories, but can be used efficiently to study the basic properties of a formal system : consistency, completeness, etc.

With FOL we have the "logical engine", i.e. the language with axioms and rules, and we usually study it in a similar way to the study of propositional calculus, in order to understand the basic meta-logic properties.

But, in addition to it, we are interested to add to the "logical engine" suitable non-logical constants, like ∈ ("in"), the binary relation of set theory, or + and × ("plus" and "times"), the basic arithmetical operations, with suitable axioms that govern their behaviour.

Thus, according to the specific mathematical symbols and axioms introduced, we have different formal mathematical theories : first order arithmetic, first-order set theory, and so on, all based on the same underlying logic : first-order predicate calculus with equality.

---

See also List of first-order theories.