# What exactly is a first-order logic?

Can someone explain in simple terms what exactly is a first-order logic?

From my amateur standpoint, I think that first-order logic is a some kind of a system of symbols and general logical rules and operations defined on that set of symbols in such a way that a first-order logic has some expressional "power" (that is, some statements can be represented in first-order logic and some theorems about first-order logic can be deduced).

However, when it comes to theorems, that is where I am stuck, because, basically, I do not know what exactly can be proved in first-order logic, including theorems about statements in first-order logic and about compound statements, and also theorems about first-order logic itself.

So, can someone here give, in as simple as possible terms, an explanation and description of a first-order logic? Preferably, as short as possible one.

Also, is there only one first-order logic or there are many first-order logics, each differing from all the other in axioms that are used to build such a theory?

• First order logic is a logic equivalent to a predicate calculus, a formal system with connectives and quantifiers, where one can only quantify over non-logical variables, but not over predicates. Some logical laws and rules of inference govern possible deductions. More broadly, systems built over it (by adding non-logical axioms) are called first order, e.g. Peano arithmetic and ZFC set theory. Jun 15 '19 at 6:38
• Jun 15 '19 at 7:55

FOL is the natural logic environment to formalize mathematical theories.

The basic characteristic of predicate calculus is the use of quantifiers : first-order logic is predicate calculus where quantification is restricted to individual variables (variables ranging over "objects") and quantification over predicate variables (i.e. variables ranging over "properties") is not allowed.

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 syntax of 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.

When we study "pure" FOL, we define the derivability relation (), where :

⊢ φ means : "formula φ is derivable in the calculus", and Γ ⊢ φ means : "formula φ is derivable in the calculus form the set Γ of assumptions".

With it we prove the fundamental Soundness and Completeness Theorem :

Γ ⊢ φ iff Γ ⊨ φ, where the symbol means semantic consequence.

In addition to the study of "pure" predicate logic, 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 mathematical theories; when the collection of axioms is the first-order version of Peano's axioms, we have PA, i.e. first-order theory of arithmetic.

The same for ZF, i.e. Zermelo-Fraenkel Set Theory.

Unfortunately, not all interesting mathematical properties are expressible with FOL; see Second-order and Higher-order Logic.

• You might want to define the ⊨ symbol before using it. Jun 18 '19 at 16:59