Stuck on basics: How to prove that {subst($\alpha$,s)} is well defined? 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.
 A: 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])$.
