substituting a variable in a formula (in logic)

Question

What kind of mathematical object is this substitution(is it a function or what). We assuming set of variables exist.

Answer 1

Let us construct a toy language with terms defined recursively as

$$\mathcal{T} = x \mid y \mid \mathtt{f(}t_1\mathtt{)} \mid \mathtt{g(}t_2\mathtt{,}t_3\mathtt{)} $$ where $x,y \in \mathcal{V}$ are variables and $t_1, t_2, t_3 \in \mathcal{T}$ are terms. Now we could define substitution for our toy language as any function $\phi : \mathcal{V} \to \mathcal{T}$ and extended it to whole $\mathcal{T}$ as follows: \begin{align} \phi'(x) &= \phi(x)\\ \phi'(y) &= \phi(y)\\ \phi'\Big(\mathtt{f(}t_1\mathtt{)}\Big) &= \mathtt{f(}\phi'(t_1)\mathtt{)} \\ \phi'\Big(\mathtt{g(}t_2\mathtt{,}t_3\mathtt{)}\Big) &= \mathtt{g(}\phi'(t_2)\mathtt{,}\phi'(t_3)\mathtt{)} \end{align}

As our terms are finite, it's easy to see that $\phi' : \mathcal{T} \to \mathcal{T}$ is a properly defined function that transforms terms into some other terms.

People usually don't distinguish between $\phi$ and $\phi'$ unless they need to be extra formal or extra cautious, and both of these functions are called "substitution". In other words, substituion is any function $\mathcal{V} \to \mathcal{T}$ or its extension to some bigger set of terms.

Still, this is only one particular approach, there are other ways to define substitution and there are some complications when you introduce quantifiers and other constructs, but I hope you got the general meaning.

Also, here I use "function" but in many texts on logic there are various levels of meta-languages, and to avoid confusion functions in one level are called just "functions" while on some other levels they may be called "transforms", "mappings", etc. For example, if for whatever reason we would like to call the symbol $\mathtt{f}$ a function, then we may call $\phi$ and $\phi'$ transformations.

Edit:

Let me define $\mathcal{T}$ and $\phi'$ more precisely (the index $i$ below is often called nesting depth).

\begin{align} T_0 &= \mathcal{V} \\ T_{i} &= \Big\{\mathtt{f(}t'\mathtt{)} \ \Big|\ t' \in T_j, j < i \Big\}\\ &\hspace{2pt}\cup \Big\{\mathtt{g(}t''\mathtt{,}t'''\mathtt{)} \ \Big|\ t'' \in T_j, j < i, t''' \in T_k, k < i \Big\} \\ \mathcal{T} &= \bigcup_{i \in \mathbb{N}}T_i \end{align} Now, take arbitrary function $\phi : \mathcal{V} \to \mathcal{T}$, define $\phi'_i : \left(\bigcup_{j = 0}^{i}T_j\right) \to \mathcal{T}$ as follows \begin{align} \phi'_0(t) &= \phi(t)\\ \phi'_i(t) &= \phi'_{i-1}(t) & \text{ for any }t \in \mathcal{T}_{i-1}\\ \phi'_i\Big(\mathtt{f(}t_1\mathtt{)}\Big) &= \mathtt{f(}\phi'_{i-1}(t_1)\mathtt{)} & \text{ otherwise}\\ \phi'_i\Big(\mathtt{g(}t_2\mathtt{,}t_3\mathtt{)}\Big) &= \mathtt{g(}\phi'_{i-1}(t_2)\mathtt{,}\phi'_{i-1}(t_3)\mathtt{)} &\text{ otherwise} \end{align} and finally set $\phi' = \bigcup_{i \in \mathbb{N}} \phi'_i$. Of course, there are some things to consider, moreover, please be aware that this is not the only way to define things (for example, not all recursive definitions allow such simple interpretation). On the other hand, the above constitutes a precise definition. I hope the inductive scheme behind it (which works because the nesting depth is a well-order) is apparent now, perhaps this will clear your doubts.

Edit 2:

In response to:

But there is problem I think. In theorem 8.4 function $ρ$ needs to be defined from natural number to a set $A$ (as you defined). But then function $h$ we get is also from $\mathbb{N}$ to $A$. What is range of $\mathcal{F}$ here and what will be the range of final function $h$ (here $T_i$)?

where I defined $\mathcal{F}$ as

$$\mathcal{F}(B) = \{\mathtt{f(}t'\mathtt{)} \mid t' \in B\} \cup \{\mathtt{g(}t''\mathtt{,}t'''\mathtt{)} \mid t'', t''' \in B\}.$$

What is the symbol $\mathtt{f}$ in the definition of $\mathcal{T}$ (or for that matter $\mathcal{F}$)? Is there any axiom that says I can use it? In the standard approach there are only sets or things defined using sets like $\mathbb{N}$. In other words, we have to define somehow $\mathtt{f}$ as a set, number or something similar. What we do, is that we create an informal mapping between terms and numbers, for example $$x \to 7, y \to 1, \mathtt{(} \to 2, \mathtt{)} \to 3, \mathtt{,} \to 4, \mathtt{f} \to 5, \mathtt{g} \to 6$$ would imply that $\mathtt{g(}x\mathtt{,f(}y\mathtt{,}x\mathtt{))}$ is $62745214733$. Then, when we talk about terms, we talk about specifically structured numbers, but think about them as terms. If we were to use the above mapping we get $T : \mathbb{N} \to 2^\mathbb{N}$, $\mathcal{T} \subset \mathbb{N}$ and $\mathcal{F} : 2^\mathbb{N} \to 2^\mathbb{N}$. To be compatible with Munkers (compare with the second example after theorem 8.4) set

\begin{align} \rho(f) &= \mathcal{F}\big(f(m)\big) \quad \text{ where } f : \{0,\ldots,m\} \to \mathbb{N} \\ T(0) &= \mathcal{V} \\ T(i) &= \rho\Big(T\big|_{\{0,\ldots,i-1\}}\Big) \end{align}

Edit 3:

In response to:

But we were defining terms. How do you first define $\mathcal{F}$ on $\mathcal{T}$ without knowing $\mathcal{T}$?

We do not need to know $\mathcal{T}$ to define $\mathcal{F}$, we only need to know that $\mathcal{T}⊂\mathbb{N}$.

Let $\bullet_{10}$ be the base-10 concatenation of numbers, that is, $x \bullet_{10} y = x\cdot 10^{|y|_{10}}+ y,$ where $|y|_{10}$ is the length of $y$ in base-10 notation; for example $123 \bullet_{10} 456 = 123456$. Now define $\mathcal{F} : 2^\mathbb{N} \to 2^\mathbb{N}$ as

$$\mathcal{F}(B) = \{52\bullet_{10} t' \bullet_{10} 3 \mid t' \in B\} \cup \{62\bullet_{10} t''\bullet_{10} 4 \bullet_{10} t'''\bullet_{10} 3 \mid t'', t''' \in B\}.$$

I hope this helps $\ddot\smile$

Answer 2

If I understood correctly, say you have a wff on n variables. Then substituting in a variable, you map into the collection of wffs on $(n-1)$ variables. If you substitute for all n variables, or if $n=1$, you map into a world, or interpretation for the wff. But there may not be possible worlds where the wff holds, e.g., if your wff is a contradiction.