Herbrand model 2026-10-31
Witness constant 2026-10-31
A witness constant is a fresh constant symbol added to a first-order language so that an existential assertion has a named witness. In a Henkin construction one adds , with absent from the previous language. Freshness preserves consistency. Repeating the construction for the successively enlarged languages supplies the witness property used in a term model.
Henkin theory 2026-10-31
A Henkin theory has named witnesses for its provable existential sentences. In a Henkin construction, fresh constants and the corresponding Henkin witness axioms give this witness property. Completeness or maximal consistency can be imposed in an additional extension step.
Heat kernel with constant absorption 2026-10-31
The displayed fundamental solution solves on the real line with a Dirac delta at the initial time. It is the ordinary heat kernel multiplied by , because that factor removes the constant reaction term. Its integral is and it converges to the Dirac delta as . Convolution with initial data gives the corresponding solution. For the total mass decays by absorption; for it grows instead.
Static-one logic hazard 2026-10-31
A logic hazard in which an output intended to remain one briefly falls to zero. In a sum of products, cover every adjacent pair of one-cells in a Karnaugh map with a common product implicant. That term omits the changing input and remains one throughout the transition, holding the OR output high regardless of the other path delays. This argument assumes one input changes at a time and the circuit starts settled.
For a concrete circuit, let , , , and . Give every gate, including each inverter, propagation delay 10 ns. Starting from , lower at time zero. Signal falls at 10 ns, while rises only at 20 ns. Their gap passes through the two OR gates, making fall during 30–40 ns even though its steady-state value remains one.
A static-one logic hazard from unequal inversion and product paths
. Details. Adding the two consensus theorem products and preserves the Boolean function and holds the output high across every potentially hazardous single-input transition. The resulting five-term expression factors as . When a change of could leave the output steadily one, and keep the second product steadily one. In the zero-to-zero case with changing , and keep both output products zero. Changes of use only one polarity each and therefore have no opposite-polarity race. This factored implementation uses three OR gates, two AND gates and two NOT gates, with a 40 ns maximum input-to-output path at the stated delays.
A shared-factor implementation of the consensus theorem correction
. Details. For linear antiplane elasticity with body forces and Dirichlet data proportional to time, uniqueness gives at any fixed crack length . The minimized elastic-plus-load potential and its energy release rate scale quadratically. The local Griffith fracture criterion laws are , and , with positive toughness .
If is finite and continuous near the initial length, it is bounded there by . Continuity of the crack path keeps it in that neighborhood for a positive interval. Choose the interval short enough that ; complementarity then forces zero growth throughout it. This proves a positive initial waiting time without assuming the crack is stationary in advance.
Least element 2026-10-31
An element of a partially ordered set is a least element if for every . A least element is unique: two such elements are below each other, so antisymmetry makes them equal.
Leftmost derivation 2026-10-31
A grammar derivation that always expands the leftmost remaining nonterminal symbol. In a context-free grammar, each parse tree specifies exactly one leftmost derivation. Two distinct leftmost derivations of the same word therefore prove that the context-free grammar is an ambiguous grammar.
Arithmetical soundness of GL 2026-10-31
Map propositional letters to arithmetic sentences, map falsity to a refutable sentence, commute with implication and interpret by an arithmetical provability predicate. Propositional axioms remain theorems. The K axiom uses the second of the derivability conditions, and the Löb axiom uses the Internal form of Löb's theorem. Modus ponens rule is preserved directly, and the necessitation rule uses the first derivability condition. Induction on a GL proof therefore proves the displayed soundness implication for Peano arithmetic with the stipulated provability predicate.
GL fixed point for a provability implication 2026-10-31
The Löb axiom gives . The tautology , necessitated and distributed, gives . Thus , and replacing the antecedent in gives exactly . Setting produces a negative-provability fixed point, provably equivalent to .
In Gödel-Löb logic, the one-variable identity solves a boxed equation with a formula omitting its unknown letter. A finite simultaneous system can be solved by elimination. First solve its last equation with the other unknowns treated as parameters, substitute that formula into the preceding equations, and apply induction. Substituting the resulting solutions back into the last formula completes the system. This construction introduces no new parameter letters.
Modalized fixed-point theorem for GL 2026-10-31
If every occurrence of in lies under a box, Gödel-Löb logic has a formula without , using only the other letters of , satisfying the displayed equivalence. Write using the outermost boxes that contain , so has no . Solve by simultaneous boxed fixed-point elimination in GL. If the solutions are , then works by replacement of provably equivalent formulas.
Fixed point of boxed negated provability 2026-10-31
A formula provably equivalent to a boxed formula satisfies in GL. The displayed fixed point then gives both and under , hence . Boxed explosion proves the reverse implication. Under arithmetic realization this is a formal inconsistency statement; Sigma-1 soundness excludes its provability, while second incompleteness excludes provability of its negation.
Löb axiom implies positive introspection 2026-10-31
The Löb axiom over normal modal logic already implies . Put . Distribution gives , hence . Necessitation and distribution give ; the Löb axiom gives , which implies .
König bound for the Gimel function 2026-10-31
Choose cofinal ordinals , indexed by , and set . Then and . The König theorem for cardinal numbers gives . The estimate holds for every infinite cardinal number, regular or singular, under the usual axiom of choice convention for cardinal arithmetic.
Geometric minimum law Created 2026-10-31 Updated 2026-11-05
For independent positive-support geometric random variables with success probabilities , all must exceed for their minimum to exceed . The resulting survival function is . This is the positive-support geometric distribution with the displayed success probability. independence is needed for multiplying the survival probabilities.
Multiply two copies of the generating function of the physicists' Hermite polynomials and integrate against . Completing the square givesComparing coefficients gives the displayed orthogonality and normalization. Equivalently differentiation in at zero justifies coefficient extraction by the Gaussian integrable bound on compact parameter ranges. Hence the unnormalized Hermite functions have norm . This proves their mutual orthogonality; completeness of that family is an additional assertion.
There are unlisted articles, also show them or only show them.

