To perform a first-order substitution, first rename each conflicting bound variable to a fresh name, then replace the designated free occurrences. The fresh names must avoid the formula's relevant free names and all names in the inserted first-order term. For instance, substituting for in requires renaming the binder, producing rather than . The latter would change the intended meaning by capturing .
First-order substitution 2026-10-25
Replacing every free occurrence of variable in a first-order formula by a first-order term . Bound occurrences of are left alone. The operation requires either that be free for substitution at those occurrences or that conflicting bound variables first be renamed, as in capture-avoiding first-order substitution.
Free for substitution 2026-10-25
A first-order term is free for substitution for a variable in a first-order formula when no free variable of becomes bound after replacing a free occurrence of . Equivalently, at every free occurrence to be replaced, none of its enclosing quantifiers binds a variable appearing in . The test depends on occurrences and scopes, not merely on which variable names appear anywhere in the formula.
Write . The kernel density estimator with bandwidth is
Sufficient conditions are that be a nonnegative symmetric probability density function with and finite nonzero second moment , and that , . Symmetry and the second-moment assumption give . The expectation is a convolution:
Taylor's theorem with integral remainder gives
The zeroth-order term integrates to , and the first-order term vanishes. The second derivative is bounded and continuous, so dominated convergence, with dominating function proportional to , yields
Combining this with the supplied leading variance gives the asymptotic mean squared error
When and , its derivative is . It changes sign exactly once, giving the pointwise optimal kernel bandwidth
Positivity of is needed for this positive interior optimum. The printed condition alone does not ensure it. For instance, is a normalized bounded probability density function with bounded continuous square-integrable second derivative, but and . At this point the displayed leading variance vanishes and the two-term AMSE has no positive interior minimizer; finer variance terms are needed to determine an appropriate bandwidth. The formal formula there gives zero, which does not satisfy the bandwidth assumptions.
For integrated error, the same expansion holds in : translation continuity of applied to the integral remainder gives
Indeed Minkowski's integral inequality bounds the norm of the difference, divided by , by the integral of ; each translated difference tends to zero and is bounded by . This proves the claimed integrated bias expansion without assuming a uniform pointwise remainder over the whole real line.
If , direct integration of the variance gives
The last term is because is bounded and integrable, hence square integrable, and convolution with a probability density function does not increase its norm. It is negligible compared with . Thus the asymptotic mean integrated squared error and its minimizer are
Here : otherwise the continuous second derivative vanishes everywhere, making affine, impossible for a probability density function on the whole real line.
Now take the standard normal density . Differentiation gives . Gaussian integration gives
The kernel constants cancel from the bandwidth ratio. At ,
Put . The logarithmic derivative of is . On the function increases, giving its minimum at , with value one. On it decreases up to and then increases, giving its minimum . Thus the global minimizers are , and the normal-density local-to-global bandwidth ratio is
The ratio diverges at the two inflection points , where the second-order pointwise bias approximation vanishes and needs a higher-order replacement.
Figure 1.
Normal-density pointwise bandwidth relative to the integrated-error optimum; minima at plus and minus square root of five
. Details.
Let be the reduced product by a proper filter on a set. Its underlying equivalence relation is when . Operations are interpreted coordinatewise, and a relation holds of the classes exactly when its coordinate truth set belongs to .
Evaluation of a first-order term commutes with passage to the quotient, by mathematical induction on terms. Consequently the desired equivalence holds for every atomic formula, including logical equality. For a formula and representatives , write .
For logical conjunction, . The filter on a set axioms give
Thus the induction hypothesis transfers a conjunction in both directions.
For existential quantification, first suppose . Choose a representative of a witness. Induction gives , and this set is contained in . Upward closure therefore gives .
Conversely, suppose . For each , choose a coordinate witness , and choose an arbitrary element of outside . These simultaneous choices use the axiom of choice, as does the usual product construction. Then , so that truth set belongs to . Induction gives , providing the required witness. Therefore
for every primitive positive formula. The exam's tame formulas are exactly this fragment, built using logical conjunction and existential quantification. No ultrafilter dichotomy was used.