An unintended change of binding caused by moving or substituting a term beneath a binder. In first-order logic, substituting $y$ for the free $x$ in $\forall yS(x,y)$ without renaming would yield $\forall yS(y,y)$, incorrectly binding the substituted occurrence. First rename the bound $y$ to a fresh $z$, obtaining $\forall zS(x,z)$, and then substitute to get $\forall zS(y,z)$. The paper's condition that a term be free for a variable excludes such capture.

A subset is Cb-embedded if every bounded continuous real-valued function on it extends to a bounded continuous real-valued function on the ambient space. A bounded extension can be clipped to preserve the original bound. This is weaker than C-embeddedness: the natural numbers in their Stone-Čech compactification have the bounded extension property, but their unbounded identity function cannot extend to a compact space.

Start planar Brownian motion at $i$ and stop at its first hit of the real axis. The vertical maximum has the displayed tail by optional stopping theorem in a strip, so its $p$th moment is $1/(1-p)$ for $p<1$ and infinite for $p\ge 1$. Reflection of the horizontal coordinate at a first level hit gives $\mathbb{P}(\sup X>\lambda )=2{\pi }^{-1}{\int }_{\lambda }^{\infty }(1+x^2{)}^{-1}dx$. The absolute horizontal maximum has upper and lower bounds of this same inverse-level order, hence the same positive-moment threshold. Its small-value probability is exponentially small in the reciprocal level, so all negative moments also exist.

Raising a solvent's boiling point at fixed external pressure by a dissolved nonvolatile solute, under conditions where the solvent vapour pressure is reduced. The simple rule does not apply unchanged to every mixture of volatile components.

A common symmetric saddle-point system couples primal unknowns with constraint multipliers through the displayed block matrix, with symmetric $H,C$. At $C=0$, full row rank of $A$ and a nonsingular reduced Hessian are exactly the nonsingularity conditions. Such matrices arise from equality-constrained quadratic models and mixed finite element methods. A regularized block $C=\mu I$ also arises when an augmented linear system replaces a badly scaled quadratic-penalty Newton system.

If $X,Y$ are independent exponential random variables with one common rate $\lambda >0$, put $U=X+Y$. The change of variables for probability densities $(x,y)=(u-y,y)$ gives $f_{U,Y}(u,y)={\lambda }^2{e}^{-\lambda u}$ on $0<y<u$. Its marginal density is ${\lambda }^{2}u{e}^{-\lambda u}$, so the conditional probability density of $Y$ given $U=u>0$ is $1/u$ on $(0,u)$. This is the shape-$(1,1)$ case of beta-gamma independence. In particular $Y/U$ is uniform on $(0,1)$ and independent of $U$. Equality of the rates is essential: different rates leave an exponential tilt across the conditional interval.

Suppose $q$ is a sublinear functional on the bounded real sequences, dominated by the limit superior and nonpositive on every shift difference $x-Sx$. The Hahn-Banach theorem then yields a Banach limit. Indeed $0\le q(x)+q(-x)$ implies $q(x)\ge -q(-x)\ge \mathrm{liminf}{x}_n$, so $q$ agrees with the ordinary limit on convergent sequences. Extend this linear limit functional by Hahn-Banach to a linear $\psi \le q$. Domination on $x-Sx$ and on its negative forces $\psi (x)=\psi (Sx)$. The two-sided limit bounds give positivity, norm one and agreement with ordinary limits. In finite-shift averaging constructions, the needed bound on shift differences follows by telescoping consecutive averages to $(x_{n+1}-x_{n+k+1})/k$.

A catenoid has zero mean curvature, but need not minimize area for its fixed boundary rings. For the profile $y(x)=\cosh x$ on $[-2,2]$, take an endpoint-zero variation $\eta (x)=\cosh x-\cosh 2$. The second variation of the rotational area isTo derive the integral, differentiate $y\sqrt{1+y^{\prime 2}}$ twice, then integrate its mixed term by parts; the endpoint term vanishes. To evaluate it, substitute ${\eta }^{\prime 2}-{\eta }^2=-1-C^2+2C\cosh x$, using the antiderivatives of $\mathrm{sech}x$ and ${\mathrm{sech}}^{2}x$. The result is negative because $\arctan (\sinh 2)<\pi /2$ and $(C+C^{-1})\tanh 2>\pi$.

Small positive and negative perturbations remain positive and preserve the boundary values. The first variation vanishes, while the negative second variation gives nearby smaller areas. Thus being a minimal surface in the zero-mean-curvature sense is a stationarity condition, not a guarantee of area minimization for arbitrary boundary separations.

For $|w|<1$, the disk automorphism $f_w(z)=(z-w)/(1-\overline{w}z)$ maps the boundary circle to itself. If $g(\theta )$ is a continuous argument of $w-e^{i\theta }$, direct conjugation gives ${\varphi }_w(\theta )=-\theta +2g(\theta )$ modulo $2\pi$. Differentiating the argument givesand substitution yields the displayed positive derivative. Its integral over one circuit is $2\pi$, so the boundary map is orientation preserving of degree one. Transforming a uniform exit angle at the centre by its inverse gives the harmonic measure density $(2\pi {)}^{-1}{\varphi }_w^{\prime }(\theta )$ for a planar Brownian motion started at $w$. This is the Poisson kernel for the unit disk with its probability normalization.

For $-(p{u}^{\prime }{)}^{\prime }+qu=f$ with one homogeneous Neumann condition and one fixed Dirichlet value, the dual problem has error forcing and homogeneous corresponding boundary data. Galerkin orthogonality with its nodal interpolant yields an element-residual identity with no jump terms, because the interpolation error vanishes at every node. With $p_{\ast }=\min p>0$, $q_{\ast }=\min q>0$, $q^{\ast }=\max q$, one reliable constant isThe proof combines a dual $H^2$ estimate with two interval Poincaré inequalities. Constants are independent of the nonuniform mesh.

For an arithmetical provability predicate write $\square A={\mathrm{Pr}}_T(┌A┐)$. The conditions are: if $T⊢A$ then $T⊢\square A$; $T⊢\square (A\to B)\to (\square A\to \square B)$; and $T⊢\square A\to \square \square A$. The first is an external rule, while the latter two are internal theorems. They formalize proof verification, closure under modus ponens rule and positive introspection. None licenses reflection from a proved sentence $\square A$ to $A$.

Assume the Hilbert-Bernays-Löb derivability conditions and the diagonal lemma. Choose $D$ with $T⊢D\leftrightarrow (\square D\to A)$. Necessitating the forward implication and using distribution and positive introspection gives $T⊢\square D\to \square A$. If $T⊢\square A\to A$, then $T⊢\square D\to A$, so the reverse fixed-point implication gives $T⊢D$. Necessitation gives $T⊢\square D$, and the preceding implications give $T⊢A$. No consistency assumption is needed for this implication between provability assertions.

Assume the Hilbert-Bernays-Löb derivability conditions and the diagonal lemma. If $T+X$ proves ${\mathrm{Pr}}_T(┌Y┐)\to Y$ for every sentence $Y$, then $T⊢\neg X$. Take the single instance $Y=\neg X$ and discharge the assumption: $T⊢X\to (\square \neg X\to \neg X)$. This propositionally implies $T⊢\square \neg X\to \neg X$, and Löb's theorem gives $T⊢\neg X$. A diagonal proof is also possible using the Gödel sentence of the extension and formalized proof transfer, without appealing to Löb's theorem.

A Rosser provability predicate adds a bounded proof-order test to an arithmetical provability predicate: a proof of the sentence must occur before every proof of its negation. For a consistent theory it has the same standard extension as ordinary provability. Internally its behavior can differ: arithmetic proves $\neg R_T(┌\perp ┐)$ by splitting proof codes before and after a fixed proof of $\neg \perp$. This does not establish the usual consistency statement for ordinary provability.

A two-variable formula enumerates a set $A$ in a theory $S$ when membership supplies a standard numeral stage whose instance is provable, while nonmembership makes every standard-stage instance refutable. The notion contains these proof obligations, not merely a syntactic complexity restriction on the formula. With bounded completeness, a bounded formula whose existential closure defines a computably enumerable set provides such an enumerator.^[ref]

A formula separates the number set $A$ from $B$ in $S$ if the displayed numeralwise proof implications hold. No decision is required outside $A\cup B$. In a consistent theory the sets must be disjoint. A diagonal sentence asserting the negation of its membership in a separator of provable from refutable codes is undecidable by the two direct contradiction cases.

An arithmetical proof relation represents the effective relation that a natural number encodes a formal proof of the logical formula with a specified Gödel number. With the usual coding apparatus its proof-checking relation is bounded. Existential quantification over the formal proof code gives the ordinary arithmetical provability predicate.

A logical formula weakly defines a total numerical function in a first-order theory when, at every standard input tuple, it proves the graph instance with the correct standard output and refutes graph instances with every incorrect standard output. This is numeralwise representation of the graph; it does not yet assert uniqueness against nonstandard outputs inside a first-order model.

Let $K_x$ be the directed set of compact elements below $x$, with least upper bound $x$, and put $A_x=\{y:y\ll x\}$. A compact element $k\le x$ belongs to $A_x$: a directed set whose least upper bound is at least $x$ also has least upper bound at least $k$, so the definition of $k\ll k$ supplies an element above $k$. Hence $K_x\subseteq A_x$.

If $y_1,y_2\in A_x$, apply the way-below relation to $K_x$ to find $k_1,k_2\in K_x$ above them. Since $K_x$ is directed, it contains a common upper bound $k$ for $k_1,k_2$. This $k$ belongs to $A_x$, proving that $A_x$ is directed. Every member of $A_x$ is below $x$, while $K_x\subseteq A_x$ has least upper bound $x$. Therefore $x$ is the least upper bound of $A_x$, which is the defining property of a continuous poset.

Suppose the distinct required runway lengths are $0=s_0<s_1<\cdots <s_k$, with $n_i>0$ users of type $i$, constant cost $\lambda \ge 0$ per unit length, and suffix counts $N_i={\sum }_{\ell =i}^k{n}_{\ell }$. Then every type-$j$ user has the displayed Shapley value. For layer $i$, exactly $N_i$ users require it. The first of them in a uniformly random permutation contributes its entire cost $\lambda (s_i-s_{i-1})$. Each requiring user has probability $1/N_i$ of being first. Linearity of the Shapley value sums these expected marginal contributions across the layers that user needs.

The allocation lies in the cost core. Its payments sum to the full runway cost. For any coalition $S$, its total payment toward layer $i$ is $\lambda (s_i-s_{i-1})|S\cap R_i|/N_i$, where $R_i$ is the set of users requiring that layer. This is zero if $S$ needs no such layer, and at most the full layer cost otherwise. Summing gives ${\sum }_{j\in S}{\varphi }_j\le c(S)$. Suffix counts followed by prefix sums compute all distinct type payments in $O(k)$ arithmetic operations.