Mathematical logic

Mathematical logic is a discipline within mathematics, studying formal systems in relation to the way they encode intuitive concepts of proof and computation as part of the foundations of mathematics.

Technical reference

This section is not intended as a crash course in mathematical logic. There is no doubt that the bare display of concise definitions is very far from an adequate encyclopedical presentation, but sections with more amenable paragraphs shall follow soon... Likewise, the several topics will be pertinently separated as soon as it makes sense, and when and where it is found a proper place.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

First-order languages and structures

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Definition. A first-order language mathfrak{L}, is a collection of distinct typographical symbols classified as follows:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

• The equality symbol $=,$; the connectives $lor,$, $lnot,$; the universal quantifier and the parentheses $(,$, $),$.
• A countable set of variable symbols $\{v\_i\}\_\{i\; =\; 0\}^infty,$.
• A set of constant symbols .
• A set of function symbols .
• A set of relation symbols $\{R\_gamma\}\_\{gamma\; in\; Gamma\},$.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Thus, in order to specify a language, it is often sufficient to specify only the collection of constant symbols, function symbols and relation symbols, since the first set of symbols is standard. The parentheses serve the only purpose of forming groups of symbols, and are not to be formally used when writing down functions and relations in formulas.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

These symbols are just that, symbols. They don't stand for anything. They do not mean anything. However, that deviates further into semantics and linguistical issues not useful to the formalization of mathematical language, yet.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Yet, because it will indeed be necessary to get some meaning out of this formalization. The concept of model over a language provides with such a semantics.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Definition. An mathfrak{L},-structure over the language mathfrak{L},, is a bundle consisting of a nonempty set A,, the universe of the structure, together with:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

• For each constant symbol $c,$ from $mathfrak\{L\},$, an element $c^\{mathfrak\{A\}\}\; in\; A,$.
• For each $n,$-ary function symbol $f,$ from $mathfrak\{L\},$, an $n,$-ary function $f^\{mathfrak\{A\}\}\; :\; A^n\; longrightarrow\; A,$.
• For each $n,$-ary relation symbol $R,$ from $mathfrak\{L\},$, an $n,$-ary relation on $A,$, that is, a subset $R^\{mathfrak\{A\}\}\; subseteq\; A^n,$.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Often, the word model is used for that of structure in this context. However, it is important to understand perhaps its motivation, as follows.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Terms, formulas and sentences

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Definition. An mathfrak{L},-term is a nonempty finite string t, of symbols from mathfrak{L}, such that either

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

• $t,$ is a variable symbol.
• $t,$ is a constant symbol.
• $t,$ is a string of the form $f\; t\_1\; ...\; t\_n,$ where $f,$ is an $n,$-ary function symbol and $t\_1,$, ..., $t\_n,$ are terms of $mathfrak\{L\},$.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Definition. An mathfrak{L},-formula is a nonempty finite string phi, of symbols from mathfrak{L}, such that either

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

• $phi,$ is a string of the form $t\_1\; =\; t\_2,$ where $t\_1,$ and $t\_2,$ are terms of $mathfrak\{L\},$.
• $phi,$ is a string of the form $R\; t\_1\; ...\; t\_n,$ where $R,$ is an $n,$-ary relation symbol and $t\_1,$, ..., $t\_n,$ are terms of $mathfrak\{L\},$.
• $phi,$ is of the form where is an $mathfrak\{L\},$-formula.
• $phi,$ is of the form where both and are $mathfrak\{L\},$-formulas.
• $phi,$ is of the form where $y,$ is a variable symbol from $mathfrak\{L\},$ and is an $mathfrak\{L\},$-formula.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Definition. An mathfrak{L},-formula that is characterized by either the first or the second clause is called an atomic.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Definition. Let phi, be an mathfrak{L},-formula. A variable symbol x, from mathfrak{L}, is said to be free in phi, if either

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

• $phi,$ is atomic and $x,$ occurs in $phi,$.
• $phi,$ is of the form and $x,$ is free in .
• $phi,$ is of the form and $x,$ is free in or .
• $phi,$ is of the form where $x,$ and $y,$ are not the same variable symbols and $x,$ is free in .

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Definition. A sentence is a formula with no free variables.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Assignment functions

Hereafter, mathfrak{L}, will denote a first-order language, mathfrak{A}, will be an mathfrak{L},-structure with underlying universe set denoted by A,. Every formula will be understood to be an mathfrak{L},-formula.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Definition. A variable assignment function (v.a.f.) into mathfrak{A}, is a function from the set of variables of mathfrak{L}, into A,.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Definition. Let s, be a v.a.f. into mathfrak{A},. We define the term assignment function (t.a.f.) overline{s},, from the set of mathfrak{L},-terms into A,, as follows:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

• If $t,$ is the variable symbol $x,$, then $overline\{s\}(t)\; =\; s(x),$.
• If $t,$ is the constant symbol $c,$, then $overline\{s\}(t)\; =\; c^\{mathfrak\{A\}\},$.
• If $t,$ is of the form $f\; t\_1\; ...\; t\_n,$, then $overline\{s\}(t)\; =\; f^\{mathfrak\{A\}\}(overline\{s\}(t\_1),\; ...,\; overline\{s\}(t\_n)),$.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Definition. Let s, be a v.a.f. into mathfrak{A}, and suppose that x, is a variable and that a in A,. We define the v.a.f. s,, referred to as an x,-modification of the assignment funtion s,, by

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

s(v) = egin{cases}

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

s(v) & mbox{if } v e x \

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

a & mbox{if } v = x

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

end{cases}

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

,

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Logical satisfaction

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Definition. Let phi, be formula and suppose s, is a v.a.f. into mathfrak{A},. We say that mathfrak{A}, satisfies phi, with assignment s,, and write mathfrak{A} models phi,, if either:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

• $phi,$ is of the form $t\_1\; =\; t\_2,$ and $overline\{s\}(t\_1)\; =\; overline\{s\}(t\_2),$.
• $phi,$ is of the form $R\; t\_1\; ...\; t\_n,$ and $(overline\{s\}(t\_1),\; ...,\; overline\{s\}(t\_n))\; in\; R^\{mathfrak\{A\}\},$.
• $phi,$ is of the form and .
• $phi,$ is of the form and or .
• $phi,$ is of the form and for each element $a\; in\; A,$, .

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Definition. Let phi, be formula and suppose that mathfrak{A} models phi, for every v.a.f. s, into mathfrak{A},. Then we say that mathfrak{A}, models phi,, and write mathfrak{A} models phi,.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Definition. Let Phi, be a set of formulas and suppose that mathfrak{A} models phi, for every formula phi in Phi, then we say that mathfrak{A}, models Phi,, and write mathfrak{A} models Phi,.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

In the case that phi, is a sentence, that is, a formula with no free variables, the existence of a single v.a.f. for which mathfrak{A} models phi, immediately implies that mathfrak{A} models phi,.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Definition. Let phi, be a sentence and suppose that mathfrak{A} models phi,. Then we say that phi, is true in mathfrak{A},.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Logical implication and truth

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Definition. Let Psi, and Phi, be sets of formulas. We say that Psi, logically implies Phi,, and write Psi models Phi,, if for every structure mathfrak{A},, mathfrak{A} models Psi, implies mathfrak{A} models Phi,.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

As a shortcut, when dealing with singletons, we often write Psi models phi, instead of Psi models {phi},.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Definition. Let phi, be a formula and suppose that arnothing models phi,. Then we say that phi, is universally valid, or simply valid, and in this case we simply write models phi,.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

To say that a formula phi, is valid really means that every mathfrak{L},-structure mathfrak{A}, models phi,.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Definition. Let phi, be a sentence and suppose that models phi,. Then we say that phi, is true.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Variable substitution

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Definition. Let u, be a term and suppose x, is a variable and t, is another term. We define the term u_t^x,, read u, with x, replaced by t,, as follows:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

• If $u,$ is the variable symbol $x,$, then $u\_t^x,$ is defined to be the term $t,$.
• If $u,$ is a variable symbol other than $x,$, then $u\_t^x,$ is defined to be the term $u,$.
• If $u,$ is a constant symbol, then $u\_t^x,$ is defined to be the term $u,$.
• If $u,$ is of the form $f\; t\_1\; ...\; t\_n,$, then $u\_t^x,$ is defined to be the term $f\; \{t\_1\}\_t^x\; ...\; \{t\_n\}\_t^x,$.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Definition. Let phi, be a formula and suppose x, is a variable and t, is a term. We define the formula phi_t^x,, read phi, with x, replaced by t,, as follows:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

• If $phi,$ is of the form $t\_1\; =\; t\_2,$, then $phi\_t^x,$ is defined to be the formula $\{t\_1\}\_t^x\; =\; \{t\_2\}\_t^x,$.
• If $phi,$ is of the form $R\; t\_1\; ...\; t\_n,$, then $phi\_t^x,$ is defined to be the formula $R\; \{t\_1\}\_t^x,\; ...,\; \{t\_n\}\_t^x,$.
• If $phi,$ is of the form , then $phi\_t^x,$ is defined to be the formula .
• If $phi,$ is of the form , then $phi\_t^x,$ is defined to be the formula .
• If $phi,$ is of the form , then
• if $x,$ and $y,$ are the same variable symbol, $phi\_t^x,$ is defined to be the formula $phi,$.
• else, $phi\_t^x,$ is defined to be the formula .

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Substitutability

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Definition. Let phi, be a formula and suppose x, is a variable and t, is a term. We say that t, is substitutable for x, in phi,, if either:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

• $phi,$ is atomic.
• $phi,$ is of the form and $t,$ is substitutable for $x,$ in .
• $phi,$ is of the form and $t,$ is substitutable for $x,$ in both and .
• $phi,$ is of the form and either
• $x,$ is not a free variable in $phi,$.
• $y,$ does not occur in $t,$ and $t,$ is substitutable for $x,$ in .

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

The notion of substitutability of terms for variables corresponds to that of the preservation of truth after substitution is carried out in terms or formulas. Strictly speaking, substitution is always allowed, but substitutability will be imperative in order to yield a formula which meaning was not deformed by the substitution.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~