$A[t/x]$ in formal logic I have been trying to understand some first-order logic, but it's basically seeming like randomly-generated nonsense.
$ A \equiv ( \exists y \enspace \lnot Q(x,y)\lor \forall z Q(x,z))$ where $t\equiv c,$
so $A[t/x] \equiv  ( \exists y \enspace \lnot Q(c,y)\lor \forall z Q(c,z)).$
$ A \equiv ( \exists y \enspace \lnot Q(x,y)\lor \forall z Q(x,z))$ where $t\equiv y,$
so $A[t/x] \equiv  ( \exists y \enspace \lnot Q(x,y)\lor \forall z Q(y,z)).$
Why did we arbitrarily choose to substitute in for t in some parts of the formulae but not in others?
 A: *

*

$ A \equiv ( \exists y \enspace \lnot Q(x,y)\lor \forall z Q(x,z))$ where $t\equiv c,$ so $A[t/x] \equiv  ( \exists y
    \enspace \lnot Q(c,y)\lor \forall z Q(c,z)).$
$ A \equiv ( \exists y \enspace \lnot Q(x,y)\lor \forall z Q(x,z))$ where $t\equiv y,$ so $A[t/x] \equiv  ( \exists y
\enspace \lnot Q(x,y)\lor \forall z Q(y,z)).$
Why did we arbitrarily choose to sub in for t in some parts but not
others?

Now, $A[t/x]$
typically denotes
the result of replacing all free occurrences of the variable $x$ in
formula $A$ with term $t.$ As such, the third occurrence of $x$ in
the above exerise would technically have been changed from $$\exists y
\enspace \lnot Q(x,y)$$ to $$\exists y \enspace \lnot Q(y,y),$$ even
if it turns out that $t$ (here $y$) is not freely substitutable
for $x$ in $A.$
Since the author declined to make the third substitution, they must
be defining $A[t/x]$ as the result of replacing every free
occurrence of the variable $x$ in formula $A$ with term $t$ in
which such a replacement results in no variable in $t$ becoming
bound.


*If the goal is to get rid of every occurrence of $x$ without
causing any trouble, we can write:
$$ A \equiv ( \exists y \enspace \lnot Q(x,y)\lor \forall z
Q(x,z))\\A[y/x] \equiv  ( \exists z \enspace \lnot Q(y,z)\lor
\forall z Q(y,z)).$$
