|Description: Alternate definition of
proper substitution. Note that the occurrences
of a given variable are either all bound (𝑥, 𝑦) or all free
(𝑡). Also note that the definiens uses
only primitive symbols.
It is obtained by applying twice Tarski's definition sb6 2417
valid for disjoint variables, so we introduce a dummy variable 𝑦 to
isolate 𝑥 from 𝑡, as in dfsb7 2443 with respect to sb5 2418.
This double level definition will make several proofs using it appear as
doubled. Alternately, one could often first prove as a lemma the same
theorem with a DV condition on the substitute and the substituted
variables, and then prove the original theorem by applying this lemma
twice in a row.
A drawback compared with df-sb 1868 is that this definition uses a dummy
variable and therefore requires a justification theorem, which requires
some of the auxiliary axiom schemes.
Once this is proved, more of the fundamental properties of proper
substitution will be provable from Tarski's FOL system, sometimes with
the help of specialization sp 2041, of the substitution axiom ax-12 2034,
and of commutation of quantifiers ax-11 2021; that is, ax-13 2234 will often
be avoided. (Contributed by BJ,