What exactly is a first-order logic?

Question

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?

Answer 1

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.

Answer 2

First order predicate logic is based on propositional logic (which is also called 0th order predicate logic).

The Logical Operators of Propositional (0th-Order Predicate) Logic:

• Negation: ~
• Conjunction: ^
• Inclusive disjunction: V
• Material implication (/conditional): -->
• Material equivalence (/biconditional): <-->

First-Order Logic (FOL) includes all the operators of propositional logic, and adds to them the following 3 operators:

• ∃: existential quantifier: ∃x: there exist(s) some x (such that)
• ∀: universal quantifier: ∀x: all x's (i.e., every x).
• =: identity

Identity (=) helps us symbolize

1. At least statements: ex., There are at least 2 numbers
2. At most statements: ex., There are at most 2 numbers
3. Exactly statements: ex., There are eactly 2 numbers.
4. Definite descriptions: "The king of France is bald".

∃xG(x): some x exists such that it is a G(), where G(x): = "x is a god." = "Some god exists"

∀xG(x): every x is such that it is a G(). = "Every god" / "All gods"

In summary:

• ~∃x: no x
• ∃x: some x
• ∀x: all x's (or every x)
• ~∀x: not all x's (or not every x)

where x is a predicate variable, can refer to anything in the domain of discourse (domain: the set of all persons).

where G() is a predicate, where G(x) is a propositional variable.