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

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?

• Would you have a reference where the two different descriptions are used? This might help provide an answer. Commented Feb 6, 2019 at 13:23
• @FrankHubeny I've added references to wikipedia pages that make this distinciton Commented Feb 6, 2019 at 14:05
• Propositional calculus is just one form of first order logic, (standard) predicate calculus is another, so are natural deduction and sequent calculus. They differ by syntax of expressions, axioms, inference rules, etc. Commented Feb 6, 2019 at 18:54

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.