Definition:Substitution (Mathematical Logic)

From ProofWiki
Jump to: navigation, search

Definition

Mapping

Let $S$ be a set.

Let $f: S^t \to S$ be a mapping.

Let $\left\{{g_1: S^k \to S, g_2: S^k \to S, \ldots, g_t: S^k \to S}\right\}$ be a set of mappings.

Let the mapping $h: S^k \to S$ be defined as:

$h \left({s_1, s_2, \ldots, s_k}\right) = f \left({g_1 \left({s_1, s_2, \ldots, s_k}\right), g_2 \left({s_1, s_2, \ldots, s_k}\right), \ldots, g_t \left({s_1, s_2, \ldots, s_k}\right)}\right)$


Then $h$ is said to be obtained from $f, g_1, g_2, \ldots, g_k$ by substitution.


The definition can be generalized in the following ways:

  • It can apply to mappings which operate on variously different sets.
  • Each of $g_1, g_2, \ldots, g_t$ may have different arities. If $g$ is a mapping of $m$ variables where $m > k$, we can always consider it a mapping of $k$ variables in which the additional variables play no part. So if $g_i$ is a mapping of $k_i$ variables, we can take $k = \max \left\{{k_i: i = 1, 2, \ldots, t}\right\}$ and then each $g_i$ is then a mapping of $k$ variables.


Partial Function

Let $f: \N^t \to \N$ be a partial function.

Let $\left\{{g_1: \N^k \to \N, g_2: \N^k \to \N, \ldots, g_t: \N^k \to \N}\right\}$ be a set of partial functions.

Let the partial function $h: \N^k \to \N$ be defined as:

$h \left({n_1, n_2, \ldots, n_k}\right) \approx f \left({g_1 \left({n_1, n_2, \ldots, n_k}\right), g_2 \left({n_1, n_2, \ldots, n_k}\right), \ldots, g_t \left({n_1, n_2, \ldots, n_k}\right)}\right)$

where $\approx$ is as defined in Partial Function Equality.


Then $h$ is said to be obtained from $f, g_1, g_2, \ldots, g_k$ by substitution.


Note that $h \left({n_1, n_2, \ldots, n_k}\right)$ is defined only when:

  • All of $g_1 \left({n_1, n_2, \ldots, n_k}\right), g_2 \left({n_1, n_2, \ldots, n_k}\right), \ldots, g_t \left({n_1, n_2, \ldots, n_k}\right)$ are defined
  • $f \left({g_1 \left({n_1, n_2, \ldots, n_k}\right), g_2 \left({n_1, n_2, \ldots, n_k}\right), \ldots, g_t \left({n_1, n_2, \ldots, n_k}\right)}\right)$ is defined.