I'm reading a chapter on axiomatic theories for predicate logic, which has three axiomatic schemes. One of them is:
$\forall x \varphi \rightarrow [t/x]\varphi$ (in which the term t is free for x in $\varphi$)
What does this mean, and can I see an example?
It just means that if $ \forall x \phi (x) $ is true then for any element in the domain $ \phi(that element) $ is true.
so if:
all numbers are greater than $a$ then 5 (being an element of the domain) is greater than $a$. (and the same for every other element in the domain)
in predicate logic we generally assume that the domain is not empty (otherwise you get "free logic" ) but mostly we do not specify what is inn them.
Hope this helps
In general, an axiom schema is a set of formulae. So
$$∀xφ→[t/x]φ$$
is notation for a set of formulae, call it $\Phi.$
Actually, there isn't quite enough information in the question to decide what the elements of $\Phi$ are, but lets assume for arguments sake that your signature includes a unary predicate symbol $P$ and two unary function symbols $f$ and $g$.
Then to obtain an element of $\Phi$, we choose a formula $\varphi$ in our language, say $P(f(x))$, and we choose a term $t$, say $g(x)$, and we substitute everything in. In this case, we deduce that:
$$∀x(P(f(x))→[g(x)/x]P(f(x)) \in \Phi$$
We're not quite done, because we have to remove the square brackets. Basically, the idea is that $[g(x)/x]$ denotes the result of putting $g(x)$ everywhere you see $x$. So
$$∀x(P(f(x))→P(f(g(x))) \in \Phi.$$
In particular, $\Phi$ is (by definition) the set of all formulae that can be obtained in this way, by making an appropriate choice of $\varphi$ and $t$. Actually, there's a caveat; we're not allowed to choose $t$ to equal a term like $\forall x P(x)$ in which $x$ is a bound variable.
The formmula :
$\forall x \varphi \rightarrow [t/x] \varphi$ (in which the term $t$ is free for $x$ in $\varphi$)
is more often written as :
$\forall x \varphi \rightarrow \varphi[t/x]$.
In order to correctly understand the symbolism, we need three "concepts" : substitution, instantiation and free substitution.
(1) Substitution
First we need to understand how to "read" correctly the $\varphi[t/x]$ part: the symbol is to be understood as the formula that you obtain from $\varphi$ substituting the term $t$ in place of the variable $x$.
Assume the first-order language for arithmetic, based on individual variables ($x, y, ...$), predicates ($=$, $\le$), function symbols ($+$, i.e. the "sum", and $\times$, i.e. the "product") and terms (like $0$ and $1$, i.e. the "names" for the numbers 0 and 1).
Let $\varphi$ the formula :
$x + 1 = 1$.
Using $0$ as the term $t$, when we perform the substitution in the above formula we get :
$0 + 1 = 1$;
this one is the $\varphi[t/x]$.
(2) Instantiation
Now consider a new formula in our language :
$\forall x (0 \le x)$;
this formula means that "all numbers are greater or equal than 0".
If we apply the schema you are asking for, we get :
$\forall x (0 \le x) \rightarrow (0 \le 1)$.
The logical axiom schema formalize the intuitive principle that "if a property $P$ holds for everything, it holds for each single thing".
In our example, we have that the (true) sentence "all numbers are greater or equal than 0" implies the true consequence "1 is greater or equal than 0".
We have "instantiated" the sentence $\varphi$, i.e. $0 \le x$ substituting the term $1$ (that is $t$) in place of the variable $x$, getting $\varphi[1/x]$, i.e. $0 \le 1$.
(3) Free substitution
We must take into account that $\varphi$ can be a "complex" formula and that it may contains other quantifiers, like :
$\forall x\exists y (x = y) \rightarrow \exists y (0 = x)$.
In this case, we have performed the substitution of the term $0$ in place of $x$.
We need a last concept; we said that terms (like $0$ and $1$) behaves like "names" for objects (numbers).
We may have also "complex" terms, like $0+1$ (it is another name for the number 1), and also so-called "open" tarms, i.e. terms with free variables, like $x +1$ (in this case, we can use the symbol $t(x)$).
An "open" term will denote an object when we will assign to the free variable $x$ a value; i.e., if we perform a substitution in the term $t$; in other words, when we put $1$ in place of $x$, we will obtain the term $t[1/x]$.
With the example above, this substitution will give us $1 + 1$, that is term without free variables ("closed"); in this case it is a "name" for the number 2.
Now go back to our formula : $\forall x\exists y (x = y)$.
What happens if we perform the substituion $y+1$ (an "open" term) in place of the variable $x$ ?
We will have :
$\forall x\exists y (x = y) \rightarrow \exists y (x = y)[y+1/x]$
i.e.
$\forall x\exists y (x = y) \rightarrow \exists y (y+1 = y)$.
What happened ? That form the (trivial but) true arithmetical law that "for each number there exists a number equal to it" (simply use the number itself) we can deduce the false statement that "there exists a number that is equal to itself 'plus 1' ".
The fallacy has been caused by the substitution of the term $y+1$ in $\varphi$; due to the fact that the formula $\varphi$ contains the quantifier $\exists y$, the substitution has the effect that the variable $y$ of the term $t(y)$ used in the substitution has been "captured" by the quantifier $\exists y$.
In order to prevent this kind of fallacy, we put on the axiom schema the restriction that :
the term $t$ used in the substitution is free for $x$ in $\varphi$.
This means exactly that the term $t$ must not contain variables that are quantified in the formula $\varphi$.
