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?