I'm studying 1st order logic (with identity) and proved that
lemma) If P is a formula and t' is a term and for any occurrences of variables of t' in P[t'/x] isn't bounded, then $$(\forall xP \rightarrow P[t'/x])$$ is a tautology.
After that, I wondered whether $$(\forall xP \rightarrow P[t'/x])$$ can be a contradiction.
(The difference between lemma and this question is that it isn't required that the occurrence of a variable in t' can be bounded in P[t'/x])
For making $(\forall xP \rightarrow P[t'/x])$ a contradiction, then $\forall xP$ should be a tautology(i.e. P is a tautology) and P[t'/x] should be a contradiction.
So, I tried to find a predicate formula P, term t', and variable x such that P is a tautology but P[t'/x] is a contradiction where P[t'/x] is a formula obtained by replacing all free occurrences of x in P by t'.
e.g.) P is a $~(\forall z x=y \rightarrow (\exists yR(y)->\exists x R(f(x, z))))$, then P[z/y] is $~(\forall z x=z \rightarrow ( \exists yR(y) \rightarrow \exists x R(f(x, z))))$, and P[g(w)/x] is $~(\forall z g(w)=z \rightarrow (\exists yR(y) \rightarrow \exists x R(f(x, z))))$ where R is a 1-place relation symbol and f is a 2-place function symbol, g is a 1-place function symbol.
Some basic definitions of terminologies are common in many books, but some are not.
So, for being more specific, in my question, I will specify some definitions of
There are countably many variable symbols, function symbols, relation symbols. constant symbols in a Language.
For any variable symbol x and any formula P, $\exists xP$ and $\forall xP$ are also formulas and the for any variable in $\exists xP$ or $\forall xP$ and (the quantifier that binds the occurrence of the variable) is (the quantifier of the smallest subformula of $\exists xP$ or $\forall xP$ such that the occurrence of the variable is bounded.)
e.g.)$\exists z ~x=y$ is a formula. $\forall y\exists x\exists y\forall x x=y \rightarrow R(x, y)$ means (semantically) there is a y such that for all x, x=y, then R(x, y) (And the occurrences of x and y in R(x, y) are not bounded by any quantifier).
I found some formula P and P[t'/x] such that P[t'/x] is a tautology and P isn't tautology. (Also, P isn't a contradiction and P[t'/x] is a contradiction.)
P : $\exists z x=y$
P[z/y] : $\exists z x=z$ (tautology)
P : $\exists x\forall z$ ~x=y
P[z/y] : $\exists x\forall z$ ~x=z (contradiction)
P : $(\forall z y=z \rightarrow \forall x x=y)$ (tautology)
P[z/y] : $(\forall z z=z \rightarrow \forall x x=z)$ (not tautology)
(So, at least if P need not be a tautology, P[t'/x] can be a contradiction.
And it's possible that (P->P[t'/x]) isn't a tautology although P is a tautology. )
And the topic is equivalent to that "There is a formula P, term t', variable x such that P is a contradiction and P[t'/x] is a tautology."
So, Is it possible that P is a tautology but P[t'/x] is a contradiction? If not, how can it be proved?