Full semantics for second-order logic Created 2026-10-06 Updated 2026-10-14
Under full semantics for second-order logic, a second-order relation variable of arity ranges over exactly , the external power set of the appropriate Cartesian product. Thus
and universal quantification over checks every such subset. Here the power set is taken in the ambient mathematical universe, not merely among relations definable by formulas or represented by objects inside .
For , a unary second-order relation variable has eight possible values, including the three singletons needed by the second-order encoding of three-colorability. The three unary witnesses can range independently over those eight subsets, giving candidate triples before the first-order sentence is checked; only six triples pass for the complete graph . For , there are candidate triples and none passes. Distinguishing the range of candidates from the constraints on valid witnesses clarifies both full semantics for second-order logic and the verifier view of NP.
The appeal of full semantics for second-order logic is its literal reading of assertions about every subset or every relation. A first-order structure fixes the second-order ranges automatically, in contrast to Henkin semantics. That expressive force comes with a limitation: there is no effective, sound deductive system complete for all valid second-order logic sentences under full semantics for second-order logic. This limitation and the change of intended models motivating Henkin semantics are described at the start of [ref].
For a domain , an external functional graph with all its individual ordered pairs in is therefore available, even if the whole graph does not belong to . More generally, a binary second-order relation variable can denote any external subset of ; its ordered pairs need not themselves be elements of the individual domain. Having endpoints in the domain is what matters. This distinction between internal objects and externally available relations is essential when applying second-order logic to the cumulative hierarchy.
Henkin semantics Created 2026-10-06 Updated 2026-10-14
In Henkin semantics, a domain is accompanied by designated ranges for second-order relation variables of each arity . A formula searches only , and checks only . These ranges can be proper subcollections of the external power set. Keeping and its input relations fixed therefore need not fix the truth of a second-order logic sentence.
As a toy illustration of restricted quantification, take and unary range . The sentence
is true under full semantics for second-order logic, but false with this selected range, because neither singleton is available. Likewise, on the complete graph , the unary range admits no witness for the second-order encoding of three-colorability, even though a usual proper vertex coloring exists. This toy range illustrates the truth definition only: it fails second-order comprehension for the formula , and is not a model of a system requiring that comprehension instance.
Admissible Henkin semantics for a specified deductive system must satisfy its axioms, including its chosen second-order comprehension requirements or analogous closure conditions for predicate abstraction. Closure is relative to the permitted formulas and parameters, rather than a blanket property of every selected family. In particular, on a finite domain, allowing logical equality, individual parameters, all finite logical disjunctions, and comprehension for those formulas forces every finite-arity relation to be available: enumerate its tuples and disjoin the formulas naming them. Thus a proper restricted finite range cannot satisfy that entire scheme.
Treating each as an additional sort, with an application relation between its members and individuals, translates this relational presentation into first-order logic with several sorts. Include axioms saying that predicates with the same members are equal, together with whatever second-order comprehension the system requires. This makes Henkin semantics useful for bringing first-order logic methods to reasoning about predicates; it does not license conclusions about all external relations.
Leon Henkin's Completeness in the Theory of Types, Journal of Symbolic Logic 15 (1950), pp. 81–91 develops general models and proves completeness for his typed deductive system. Its opening footnote 5 explicitly discusses closure under operations associated with formula formation. Henkin later described the discovery process in his [ref]; that later account is a historical recollection, distinct from the original publication.
Second-order cone programming Created 2026-10-06 Updated 2026-10-14
A second-order cone program has a linear objective and affine constraints taking values in products of second-order cones and nonnegative orthants. Norm epigraphs have the form ; quadratic epigraphs admit the affine lift , equivalent to . Product-cone self-concordant barriers give interior-point methods.
For a twice continuously differentiable function and , the fundamental theorem of calculus gives
The nonnegative triangular weight has integral , so its supremum norm estimate directly controls the second modulus of smoothness.
Reversible thermodynamic process Created 2026-10-06 Updated 2026-10-20
A thermodynamically reversible process can be reversed without a net change of the system and surroundings. Its entropy change equals reversible heat transfer divided by temperature. A reversible adiabatic process conserves entropy; adiabaticity alone does not forbid internal entropy production in an irreversible evolution.
For a nondegenerate induced metric tensor, a totally geodesic submanifold has vanishing second fundamental form; equivalently, every ambient geodesic initially tangent to it remains in it. This extends the notion of a totally geodesic hypersurface to arbitrary codimension.
For the ambient Levi-Civita connection, a normal field , and tangent fields , differentiate using metric compatibility. The tangential part of is orthogonal to , giving the displayed identity. It controls how an ambient derivative of a normal vector can develop a tangential component, and is the vector-valued version of the shape operator relation.
Gauss–Codazzi equations 2026-10-06
The Gauss–Codazzi equations relate the intrinsic curvature and connection of an embedded submanifold to its second fundamental form and the ambient curvature. The Gauss equation controls tangential curvature; the Codazzi equation controls the covariant derivative of the second fundamental form. The Gauss formula is the tangential-normal splitting used to derive these relations.
Second fundamental form of a ring torus Created 2026-10-06 Updated 2026-10-14
For major radius and minor radius , let . With the inward normal determined by the usual ordered parametrization, the first fundamental form and second fundamental form are
Reversing the normal reverses . The Gaussian curvature of a ring torus is independent of this orientation.
Outgoing Eddington-Finkelstein coordinates Created 2026-10-06 Updated 2026-10-18
The retarded coordinate puts the radial Schwarzschild metric into , with . Outgoing radial null geodesics have constant . These coordinates are regular at the past horizon; an infaller crossing the future horizon has .
For a complex polynomial , assume and put and . Both roots of a polynomial lie in the closed unit disk if and only if . Strict inequality puts both roots in the open disk. Under the strict product assumption , any unit-modulus root is automatically simple.
To prove the strict version, define and . On the unit circle , so the Rouche theorem shows that a stable and have the same two interior zeros. Conversely , and the same Rouche theorem implies that two interior zeros of give two interior zeros of . The nonzero root of is , proving the criterion. The closed version follows by continuity, replacing by in the sufficiency direction. In the necessity direction with a boundary root, replace by for close to one and let . The product of the two roots of a polynomial excludes two unit-modulus roots and excludes a repeated unit-modulus root.
Let real power series and converge on , with for every index including zero. If has entries there, applying within two diagonal blocks and across them preserves positive semidefiniteness. Indeed the coefficient matrix is a bipartite block-constant positive semidefinite matrix. Each is positive semidefinite by the Schur product theorem, and their sum converges to the transformed matrix. Closedness of the positive semidefinite cone completes the proof. Convergence at one gives , so coefficient domination ensures absolute convergence of both series throughout the interval. Without the zero-index condition, , and give a counterexample.
The scaling hypothesis treats the singular equilibrium free-energy density as a generalized homogeneous function of thermal and field-like scaling variables. Choosing the blocking factor to make the thermal variable order one gives . It concerns the singular contribution after subtracting analytic backgrounds. Dangerously irrelevant couplings or marginal logarithms can qualify this simple two-variable form. Differentiation yields scaling relations for critical exponents.
Fisher scaling relation Created 2026-10-06 Updated 2026-10-20
The correlation-function susceptibility sum rule and give when is finite, its large-distance tail is integrable and . With correlation-length critical exponent , this gives the displayed relation for the magnetic-susceptibility critical exponent. Microscopic distances contribute a regular background rather than the divergent critical power.
Long imaginary-time evolution multiplies an energy eigenstate by . After normalization it projects onto the lowest energy component with nonzero initial overlap, or onto the lowest-energy subspace if the vacuum is degenerate. This provides vacuum boundary conditions for a path integral and is related to the Feynman i-epsilon prescription.
An interaction depending on the field can be represented by substituting into its action and acting on the free generating functional. Expanding that exponential produces Feynman diagrams, contractions and vertex weights. Normalize by the resulting value at to cancel vacuum diagrams.
Antikink 2026-10-06
An antikink is a scalar-field kink with the opposite orientation of its vacuum boundary values. If joins vacua to , then joins to . For an even double-well potential and an odd centered phi-four kink, the centered antikink is . With , a kink has and an antikink has . Their localized energies coincide by spatial reflection.
Scalar mass 2026-10-06
The mass of a canonically normalized scalar field is determined by its quadratic fluctuation potential at a stationary vacuum. With several real fields, physical squared masses are the eigenvalues of the scalar mass matrix. A negative squared mass signals an unstable direction rather than a stable massive particle.
A real scalar field is minimally coupled to a metric tensor when its kinetic term uses the metric contraction of first derivatives and its scalar potential depends only on the field, without an explicit scalar curvature coupling. For metric signature the displayed Lagrangian and volume density give . Its stress-energy tensor is . The scalar stress-energy divergence identity explains its conservation on the field equation.

There are unlisted articles, also show them or only show them.