Talk:First-order logic/Technical reference

From Wikipedia, the free encyclopedia

Contents

[edit] Technical reference

Main article: First-order logic

[edit] First-order languages and structures

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

  1. The equality symbol =\,; the connectives \lor\,, \lnot\,; the universal quantifier \forall\, and the parentheses (\,, )\,.
  2. A countable set of variable symbols \{v_i\}_{i = 0}^\infty\,.
  3. A set of constant symbols \{c_\alpha\}_{\alpha \in \Alpha}\,.
  4. A set of function symbols \{f_\beta\}_{\beta \in \Beta}\,.
  5. 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 linguistic 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:

  1. For each constant symbol c\, from \mathfrak{L}\,, an element c^{\mathfrak{A}} \in A\,.
  2. For each n\,-ary function symbol f\, from \mathfrak{L}\,, an n\,-ary function f^{\mathfrak{A}} : A^n \longrightarrow A\,.
  3. 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.

[edit] 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 \lnot(\alpha)\, where \alpha\, is an \mathfrak{L}\,-formula.
  • \phi\, is of the form (\alpha \lor \beta)\, where both \alpha\, and \beta\, are \mathfrak{L}\,-formulas.
  • \phi\, is of the form (\forall y)(\alpha)\, where y\, is a variable symbol from \mathfrak{L}\, and \alpha\, 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 \lnot(\alpha)\, and x\, is free in \alpha\,.
  • \phi\, is of the form (\alpha \lor \beta)\, and x\, is free in \alpha\, or \beta\,.
  • \phi\, is of the form (\forall y)(\alpha)\, where x\, and y\, are not the same variable symbols and x\, is free in \alpha\,.

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

[edit] 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[x|a]\,, referred to as an x\,-modification of the assignment function s\,, by

s[x|a](v) = \begin{cases} s(v) & \mbox{if } v \ne x \\ a & \mbox{if } v = x \end{cases} \,

[edit] 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[s]\,, 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 \lnot(\alpha)\, and \mathfrak{A}\mbox{ }\not\models\mbox{ }\alpha[s]\,.
  • \phi\, is of the form (\alpha \lor \beta)\, and \mathfrak{A} \models \alpha[s]\, or \mathfrak{A} \models \beta[s]\,.
  • \phi\, is of the form (\forall y)(\alpha)\, and for each element a \in A\,, \mathfrak{A} \models \alpha[s[y|a]]\,.

Definition. Let \phi\, be formula and suppose that \mathfrak{A} \models \phi[s]\, 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[s]\, 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}\,.

[edit] 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 \varnothing \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.

[edit] 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 \lnot(\alpha)\,, then \phi_t^x\, is defined to be the formula \lnot(\alpha_t^x)\,.
  • If \phi\, is of the form (\alpha \lor \beta)\,, then \phi_t^x\, is defined to be the formula (\alpha_t^x \lor \beta_t^x)\,.
  • If \phi\, is of the form (\forall y)(\alpha)\,, 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 (\forall y)(\alpha_t^x)\,.

[edit] 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 \lnot(\alpha)\, and t\, is substitutable for x\, in \alpha\,.
  • \phi\, is of the form (\alpha \lor \beta)\, and t\, is substitutable for x\, in both \alpha\, and \beta\,.
  • \phi\, is of the form (\forall y)(\alpha)\, and either
    • x\, is not a free variable in \phi\,.
    • y\, does not occur in t\, and t\, is substitutable for x\, in \alpha\,.

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.