Stuck on basics: How to prove that {subst($\alpha$,s)} is well defined?

Question

So I feel like this is a really basic point that I'm missing and I can't really manage to prove that: So I have a substitution function $s: Var \rightarrow WFF$ and a subst function: $WFF \times WFF^{Var} \rightarrow (Symb \cup Var)$ I'm pretty sure it's a well known function so I'm not writing it's inductive definition.

I need to prove that for every $s$ and $\alpha$ exits a single $\beta$ s.t $subst(\alpha,s) = \beta$ I know i need to prove first that it exists and than that's it's uniqe. But i'm not sure how, I think my main problem with this is that it's defined inductively.

Answer 1

HINT

First of all, we need the recursive definition of substitution into a term. See

• Dirk van Dalen, Logic and Structure (5th ed - 2013), page 60 :

Definition 3.3.9 Let $s, t$ be terms, then $s[t/x]$ is defined by:

(i) $y[t/x] := y$ if $y \ne x$ and $y[t/x] := t$ if $y = x$

$\ \ \ \ \ c[t/x] := c$

(ii) $f(t_1,\ldots, t_p)[t/x] := f(t_1[t/x],\ldots, t_p[t/x])$.

Then we use it in the definition of substitution into a formula; the relevant clauses are :

Definition 3.3.10 $\varphi[t/x]$ is defined by:

(i) [...] $P(t_1,\ldots, t_p)[t/x] := P(t_1[t/x],\ldots, t_p[t/x])$,

$\ \ \ \ (t_1 = t_2)[t/x] := t_1[t/x] = t_2[t/x]$, for atomic formulae

(ii) $(\varphi \square \psi)[t/x] := \varphi[t/x] \square \psi[t/x]$, where $\square$ stands for the usual binary connectives : $\land, \lor, \rightarrow$

$\ \ \ \ (\lnot \varphi)[t/x] := \lnot \varphi [t/x]$

(iii) $(∀y \varphi)[t/x] := ∀y(\varphi)[t/x]$ if $x \ne y$, $∀y \varphi$, if $x = y$.

---

With this "machinery" in place, what is the function subst ?

Here we need the details about your function $s$ ...

Without them, we can consider each term $\tau$ as a function $\tau : Var \to Term$, defined according to Def.3.3.9 above, i.e. $\tau(x)= \sigma[\tau/x]$.

Having $\tau$, we can use it in the definition of $subst$ according to Def.3.3.10 above.

If $\alpha$ is atomic, i.e. $\alpha := P(t_1,\ldots, t_p)$, then $\beta := subst(\alpha, \tau) := P(t_1[\tau/x],\ldots, t_p[\tau/x])$, and the same for $\alpha := (t_1 = t_2)$, with $\beta := (t_1[\tau/x] = t_2[\tau/x])$.