Formal Logic

1. Terms and formulas

1.1. First-order languages

Using propositional logic, one may formalize a reasoning akin to the following:

The door of the garden is open or closed. The door of the garden is not open. Therefore it is closed. $(1)$

Indeed, let the atomic proposition $O$ and $C$ stand for "the door of the garden is open" and "the door of the garden is closed", respectively. Then, the propositional content of $(1)$ may be captured by the following formula:

$(O ∨ C) → (¬ O → C)$ $(2)$

And the fact that reasoning (1) is correct may be checked by establishing that formula $(2)$ is valid.

Now, the natural language proposition "the door of the garden is open" is made of a predicate ("is open") applied to a subject ("the door of the garden"). This internal structure of an atomic proposition is not represented in formula (2). In propositional logic, indeed, atomic propositions are denoted by single symbols, and there is nothing like a notion of predicate or a notion of subject. Consequently, representing a reasoning such as the following one falls outside of the scope of propositional logic:

Every gate is open or closed. The door of the garden, which is a gate, is not open. Therefore it is closed. $(3)$

Anticipating on the notion of formula that we will introduce below, the logical content of $(3)$ may be represented by means of the following formula:

$ (∀ x. {\it\text"Gate"}(x) → ({\it\text"Open"}(x) ∨ {\it\text"Closed"}(x))) → ({\it\text"Gate"}({\it\text"door"}({\it\text"garden"})) ∧ ¬ {\it\text"Open"}({\it\text"door"}({\it\text"garden"}))) → {\it\text"Closed"}({\it\text"door"}({\it\text"garden"})) $ $(4)$

Several new ingredients are needed to accommodate such a formula. One needs a notion of term in order to denote entities (in our example ${\it\text"door"}({\it\text"garden"})$ is such a term). One also needs symbols that denote predicates (such as ${\it\text"Gate"}$, ${\it\text"Open"}$, or ${\it\text"Closed"}$). Finally, one also needs variables that range over entities (such as $x$ in our example).

The symbols that are used to denote predicates will be called the "relational symbols". In example (4), all the relational symbols are unary in the sense that they apply to only one argument. This will not always be the case. For instance, the following natural language utterance:

the friends of my friends are my friends $(5)$

might be modeled by the following formula:

$ ∀ x. ∀ y. ({\it\text"Friend"}(I,x) ∧ {\it\text"Friend"}(x,y)) → {\it\text"Friend"}(I,y) $ $(6)$

where ${\it\text"Friend"}$ is a binary relational symbol, i.e., a relational symbol that applies to two arguments. When a symbol applies to $n$ arguments, one says that the arity of the symbol is $n$. When writing formulas, we will allow for symbols of arbitrary arity. Consequently, when listing the symbols that can be used within formulas, one must specify their respective arities. This motivates the following definition.

A ranked alphabet is defined to be a pair ${\sc A} = ⟨ A, ar ⟩$ where:

$A$ is a finite set of symbols;
$ar ∈ ℕ^A$ is a function that assigns to each symbol in $A$ a natural number called "the arity of the symbol".

For instance, let consider all the relational symbols that we have used in the above examples ($2$, $4$, and $6$). They may be collected in a ranked ${\sc A} = ⟨ A, ar ⟩$ where:

$A = \{ O, C, {\it\text"Gate"}, {\it\text"Open"}, {\it\text"Closed"}, {\it\text"Friend"} \}$
$ar(O) = ar(C) = 0$, $ar({\it\text"Gate"}) = ar({\it\text"Open"}) = ar({\it\text"Closed"}) = 1$, $ar({\it\text"Friend"}) = 2$.

Let ${\sc A} = ⟨ A, ar ⟩$ be a ranked alphabet. By a slight abuse of notation, we will use ${\sc A}$ to refer to both the ranked alphabet itself, and its set of symbols. Accordingly, we will write $a∈{\sc A}$ for $a∈A$.

Consider example ($4$) again. The formal language that is used to express the atomic propositions (e.g., ${\it\text"Open"}({\it\text"door"}({\it\text"garden"}))$) is called a first-order language. Such a language is made of to kinds of symbols: symbols that are used to express propositions (such as ${\it\text"Open"}$ or ${\it\text"Closed"}$), and symbols that are used to express entities (such as ${\it\text"garden"}$ or ${\it\text"door"}$). As we already mentioned, a symbol of the first kind is called a relational symbol. As for the symbols of the second kind, they are called the functional symbols. Accordingly, a first-order language is completely specified by the set of functional symbols and the set of relational symbols upon which it is built.

A first-order language signature is defined to be a pair $⟨ {\sc F}, {\sc R} ⟩$ where:

${\sc F}$ is a ranked alphabet the symbols of which are called "the functional symbols";
${\sc R}$ is a ranked alphabet the symbols of which are called "the relational symbols".

For instance, the first-order language signature upon which is built example (4) is the pair $⟨ {\sc F}, {\sc R} ⟩$ such that:

${\sc F} = ⟨ \{{\it\text"garden"},\text" "{\it\text"door"}\},\text" " \{({\it\text"garden"},\text" "0),\text" "({\it\text"door"},\text" "1)\} ⟩$
${\sc R} = ⟨ \{{\it\text"Gate"},\text" "{\it\text"Open"},\text" "{\it\text"Closed"}\},\text" " \{({\it\text"Gate"},1),\text" "({\it\text"Open"},1),\text" "({\it\text"Closed"},1)\} ⟩$

1.2. Terms and atomic formulas.

We can now define formally what are the terms and the atomic formulas built upon a first-order language signature.

Let $\sc X$ be a countable set of variables, and let $⟨ {\sc F}, {\sc R} ⟩$ be a first-order language signature. The set of terms built upon this set of variables and this signature is inductively defined as follows:

every variable $x ∈ {\sc X}$ is a term;
every $c ∈ {\sc F}$ such that $ar(c) = 0$ is a term;
if $f ∈ {\sc F}$ is such that $ar(f) = n$ (with $n>0$), and if $t_1, ..., t_n$ are terms, so is $f(t_1, ..., t_n)$.

The set of atomic formulas built upon that same signature is then defined as follows:

every $A ∈ {\sc R}$ such that $ar(A) = 0$ is an atomic formula;
if $R ∈ {\sc R}$ is such that $ar(R) = n$ (with $n>0$), and if $t_1, ..., t_n$ are terms, then $R(t_1, ..., t_n)$ is an atomic formula.

According to the above definition, we can see that "${\it\text"garden"}$" and "${\it\text"door"}({\it\text"garden"})$" are terms, while "${\it\text"Closed"}({\it\text"door"}({\it\text"garden"}))$" is an atomic proposition.

1.3. Formulas

The notion of atomic proposition being defined, we may now give the definition of a formula.

The set of formulas of predicate logic built upon a set of variables ${\sc X}$ and a first-order language signature $⟨ {\sc F}, {\sc R} ⟩$ is inductively defined as follows:

Every atomic proposition built upon ${\sc X}$ and $⟨ {\sc F}, {\sc R} ⟩$ is a formula.
$⊥$ is a formula.
$⊤$ is a formula.
If $α$ is a formula, so is $(¬α)$.
If $α$ and $β$ are formulas, so is $(α ∧ β)$.
If $α$ and $β$ are formulas, so is $(α ∨ β)$.
If $α$ and $β$ are formulas, so is $(α → β)$.
If $x∈{\sc X}$ and if $α$ is formulas, then $(∀ x. α)$ is a formula.
If $x∈{\sc X}$ and if $α$ is formulas, then $(∃ x. α)$ is a formula.

The above definition extends Definition 1 in two different ways. First of all it relies on a richer notion of atomic proposition, of which the notion of atomic proposition used in Definition 1 is a particular case (indeed, the propositional case amounts to considering only nullary relational symbols, i.e., relational symbols of arity $0$). Then, it introduces two new kinds of formulas: $(∀ x. α)$, and $(∃ x. α)$. Formulas of these kinds are called quantified formulas, and the symbols "$∀$" and "$∃$" are respectively called the universal quantifier and the existential quantifier. Intuitively, a formula of the form $(∀ x. α)$ asserts that every entity (say $x$) satisfies the property $α$. For instance, a sentence such as "all the gates are open" can be formulated as follows:

$$ (∀ x. {\it\text"Gate"}(x) → {\it\text"Open"}(x)) $$

By contrast, a formula of the form $(∃ x. α)$ asserts that some entity satisfies the property $α$. Accordingly, the sentence "there is at least one gate that is closed" can be expressed by the following formula:

$$ (∃ x. {\it\text"Gate"}(x) ∧ {\it\text"Closed"}(x)) $$

Definition 22 being an extension of Definition 1, the notational conventions introduced in Section 1.3 of Chapter I are still in order. In addition to these, we consider new conventions related to the quantified formula. We do not write the brackets surrounding a formula that is directly embedded in a quantified formula. For instance, we write $(∀ x. α ∧ β)$ for $(∀ x. (α ∧ β))$. When several quantifiers of the same nature follow each other, we write only once the corresponding quantification symbol, followed by the sequence of the quantified variables, i.e., we write $(∃ x_1 x_2 ... x_n. α)$ for $(∃ x_1. (∃ x_2. ... (∃ x_n. α)...))$. Using all these conventions, a formula such as:

$$ (∀ x.(∀ y.(∃ z. (P(x,y) → (A(z,x) ∧ A(z,y)))))) $$

may be written as:

$$ ∀ x y. ∃ z. P(x,y) → (A(z,x) ∧ A(z,y)) $$

1.4. Free and bound variables

An important notion in logic, and more generally in mathematics, is the one of "free" and "bound" variables. Usually, a variable is a placeholder that stands for an arbitrary value and that can possibly be replaced by some specific value. For instance, if one writes:

$x + x = 2 × x$

one may particularize this equation by substituting some value for $x$:

$3 + 3 = 2 × 3$

Such a variable, for wich a value may be substituted, is called a free variable. By contrast, in a quantified formula $∀ x. \alpha$, variable $x$ may not be replaced by some specific value. It does not correspond to a placeholder but rather to a kind of conventional name that is bound to some agreed range of values. As an illustration, consider the following sentence: "each student has a registration number". Its meaning can be modeled by the following formula:

$∀ x. {\it \text"student"}(x) → (∃ y. {\it \text"number"}(y) ∧ {\it \text"registration"}(x,y))$

This formula may be paraphrased as follows: every student (call her or him $x$) is such that there exists a number (say $y$) such that the registration number of $x$ is $y$. This paraphrase stresses that $x$ and $y$ are just conventional names, respectively bound to the set of students and to the set of numbers. Now, clearly, if one substitutes for $x$ and $y$ some specific value, one just obtains a nonsensical expression:

$∀ {\bo\text"Joan"}. {\it \text"student"}({\bo\text"Joan"}) → (∃ 237. {\it \text"number"}(237) ∧ {\it \text"registration"}({\bo\text"Joan"},237))$

This distinction between free and bound variables is not proper to logic but appears in other domains of mathematics. For instance, in the following equation:

$$∑↙{i=1}↖n i={n^2 + n}/2$$

variable $n$ is free while variable $i$ is bound. Indeed, replacing $n$ by some specific value yields a particular case of the equation:

$$∑↙{i=1}↖5 i={5^2 + 5}/2$$

On the other hand, substituting some value for $i$ resulsts in a nonsensical expression:

$$∑↙{5=1}↖n 5 = {n^2 + n}/2$$

Now, concerning free and bound variables, an important point is worth noting. In order to be precise, one should not speak about free and bound variables but about free and bound occurrences of variables. For instance, in expression $i + ∑↙{i=1}↖n i$ the first occurrence of $i$ is free (for it is not in the scope of the binding operator $∑$), the second occurrence is binding occurrence, and the third occurrence is bound.

As a consequence of the fact that a bound variable is only a kind of conventional name, one may agree on some other convention without changing the meaning of the expression in which the bound variable occurs. For instance, the two expressions $∑↙{i=1}↖n i$ and $∑↙{j=1}↖n j$ have exactly the same meaning. Back to our student registration number example, one could have express the meaning of the sentence as follows:

$∀ u. {\it \text"student"}(u) → (∃ v. {\it \text"number"}(v) ∧ {\it \text"registration"}(u,v))$

The operation of changing the name of a bound variable is called renaming. From now on, we will consider that two formulas that can be obtained one from the other by renaming are syntactically equivalent.

Let us now give some definitions that will be useful in the sequel. We first define the set of variables occurring in a term.

The set of variables occurring in a term $t$, in notation ${\it \text"Var"}(t)$, is inductively defined as follows:

${\it \text"Var"}(x) = \{x\}$, for $x ∈ {\sc X}$
${\it \text"Var"}(c) = ∅$, for $c ∈ {\sc F}$ with $ar(c) = 0$
${\it \text"Var"}(f(t_1, ..., t_n)) = {\it \text"Var"}(t_1) ∪ ... ∪ {\it \text"Var"}(t_n)$, where $f ∈ {\sc F}$ with $ar(f) = n$.

We now define the set of variables occurring free in a formula.

The set of variables occurring free in a formula $α$, in notation $FV(α)$, is inductively defined as follows:

$FV(R(t_1, ..., t_n)) = {\it \text"Var"}(t_1) ∪ ... ∪ {\it \text"Var"}(t_n)$
$FV(⊥) = ∅$
$FV(⊤) = ∅$
$FV(¬α) = FV(α)$
$FV(α ∧ β) = FV(α) ∪ FV(β)$
$FV(α ∨ β) = FV(α) ∪ FV(β)$
$FV(α → β) = FV(α) ∪ FV(β)$
$FV(∀ x. α) = FV(α) ∖ \{ x \}$
$FV(∃ x. α) = FV(α) ∖ \{ x \}$

Let $x$ be a variable, and $t$ be a term. The term obtained by substituting $t$ for the occurrences of $x$ in a term $u$, in notation $u[x≔t]$, is inductively defined as follows:

$x[x≔t] = t$
$y[x≔t] = y$, for $y ∈ {\sc X}$ and $y≠x$
$c[x≔t] = c$, for $c ∈ {\sc F}$ with $ar(c) = 0$
$f(t_1, ..., t_n)[x≔t] = f(t_1[x≔t], ..., t_n[x≔t])$, where $f ∈ {\sc F}$ with $ar(f) = n$.

Finally, we define the notion of substituting a term for the free occurrences of variable.

Let $x$ be a variable, and $t$ be a term. The formula obtained by substituting $t$ for the free occurrences of $x$ in a formula $α$, in notation $α[x≔t]$, is inductively defined as follows:

$R(t_1, ..., t_n)[x≔t] = R(t_1[x≔t], ..., t_n[x≔t])$
$⊥[x≔t] = ⊥$
$⊤[x≔t] = ⊤$
$(¬α)[x≔t] = (¬α[x≔t])$
$(α ∧ β)[x≔t] = (α[x≔t] ∧ β[x≔t])$
$(α ∨ β)[x≔t] = (α[x≔t] ∨ β[x≔t])$
$(α → β)[x≔t] = (α[x≔t] → β[x≔t])$
$(∀ y. α)[x≔t] = (∀ y. α[x≔t])$, where $x≠y$ and $y ∉ {\it \text"Var"}(t)$
$(∃ y. α)[x≔t] = (∃ y. α[x≔t])$, where $x≠y$ and $y ∉ {\it \text"Var"}(t)$

Remark that the proviso that appears in clause 8 and 9 can always be satisfied by renaming.