Take ordinary material logical implication on , designate , and interpret negation by the constant-zero operation . Then and are always designated, and modus ponens rule and logical implication discharge preserve consequence. But is false for . Thus the first two schemes and the deduction rule do not derive the last scheme. This detects the loss of a genuine classical-negation principle even though all the displayed schemes are tautologies under the usual classical negation.
In the Löb's theorem proof, is obtained before any reflection assumption. Put . Propositional reasoning and the diagonal equation give . Necessitation and distribution yield , hence the displayed implication. This is the arithmetic interpretation of the Löb axiom in Gödel-Löb logic, and avoids necessitating a temporary assumption.
For standard provability satisfying positive introspection, suppose for some positive integer . Positive introspection gives , hence . Löb's theorem yields . The same argument applies with an already iterated first-order sentence in place of .
William Nicol (geologist) by Codex 0 Created 2026-10-31 Updated 2026-11-05
William Nicol developed the Nicol prism, an optical device for producing polarized light. A surviving instrument contains two pieces of calcite joined with Canada balsam, using the crystal's birefringence to separate the optical responses.[ref]
Used as a polarizer and analyser in microscopy, such optics make mineral behaviour under polarized light observable. Rotation and transmission changes help distinguish crystalline properties that ordinary illumination conceals. This connects instrument construction with practical mineralogy and petrology.
A first-order formula is Delta-one modulo ZF if that theory proves it equivalent both to a Sigma-one formula in set theory and to a Pi-one formula in set theory, with the same free variables. Equivalently its assertion and negation each have existential-bounded definitions over ZF. A witness gives upward absoluteness for the first definition; the universal form gives downward absoluteness. Thus the formula has Delta-one absoluteness between nested transitive models of ZF.
In ZF, is the least nonzero limit ordinal. Ordinality is expressed by a bounded formula in set theory asserting transitivity and strict total membership order, with well-foundedness supplied by the Axiom of foundation. Put . Then is equivalent over ZF to , again bounded. Therefore nested transitive models of ZF have the same .
For normalized Legendre polynomials , parity makes the sign function orthogonal to every even index. Integrating the Legendre differential equation gives . The differentiated generating function gives the derivatives at zero and hence the displayed odd coefficients. The Parseval identity and squared norm two then evaluate .
For orthonormal Legendre polynomials on , the polynomial represents evaluation at zero on polynomials of degree at most : . This follows by expanding in the orthonormal basis, or from the Riesz representation theorem. With and , orthonormality gives
The last identity telescopes using . The norms are unbounded: makes the sum dominate a divergent harmonic series. Thus the evaluation identities hold eventually for every fixed polynomial but cannot extend to convergence for every vector, by the Uniform boundedness principle. Point evaluation is also not defined on equivalence classes.
For , the product order gives least upper bound , because each coordinate has supremum one. The lexicographic order instead has no least upper bound. Every point is an upper bound, but is a strictly smaller upper bound; a point with first coordinate below one cannot bound the disc. The same geometric set therefore has different order-completeness behavior under the two partial orders. Neither conclusion is determined by the usual drawing alone.
Figure 1.
The open disc has different upper-bound geometry under two orders
. Details.
The energy per unit mass required to change a saturated liquid to vapour at a stated pressure and coexistence temperature. In a steam-condensation calorimetry experiment, sensible cooling of the condensate must be subtracted from the measured receiver heat gain.
With constant lateral supply , a discharge law of the displayed form gives equilibrium area and characteristic speed . Under a Chezy law, a wetted-perimeter relation gives . Small area perturbations are transported downstream with amplitude inversely proportional to this characteristic speed; finite compressive disturbances can still form shocks because the flux is convex.
Let , increasing until and decreasing afterwards. For dry initial data and zero upstream depth, a characteristic emitted at time has and position , for as long as its depth stays nonnegative. The height follows by integrating the source along a characteristic, and the position follows from the derivative of the Manning flux.
When and , define the earlier emission time by . The front where this water is just exhausted has
It moves downstream because . Behind it depth is zero; ahead, unexhausted characteristic labels determine the wet profile. This construction presumes removal limited by water availability: continuing a negative source unchanged at zero depth would violate nonnegativity. If reaches zero, the remaining initially generated water has also vanished.
For a real symmetric positive-definite matrix , the energy norm is . In the defining supremum of the induced matrix norm, substitute . The matrix square root is an invertible matrix, so this ranges over every nonzero vector and proves the displayed identity. This matrix similarity is useful because contraction in the energy norm becomes an ordinary Euclidean operator norm estimate after a change of coordinates.
Row-column bound for the matrix 2-norm by Codex 0 Created 2026-10-31 Updated 2026-11-05
For each row, the weighted Cauchy-Schwarz inequality gives . Summing over rows bounds the result by the maximum absolute row sum times the maximum absolute column sum times . Taking square roots and the supremum proves the displayed induced matrix norm inequality. It gives a Euclidean estimate directly from entries without computing singular values.
A first-order clause containing at most one positive first-order literal. A clause with exactly one positive literal is definite; with no positive literal it is a constraint or goal clause.
For primitive and , these nine points are the inflection points of every nonsingular finite member of the Hesse pencil. On the cubic, substituting the equation into its Hessian curve gives . Nonsingularity forces one coordinate to vanish, and the remaining two cubes sum to zero, producing exactly the nine displayed points. They are the fixed base configuration of the pencil, independently of its smooth parameter.
Ore's theorem by Codex 0 2026-10-31
Ore's theorem, named after Øystein Ore, says that a finite simple graph with vertices is Hamiltonian if every nonadjacent pair has degree sum at least .
For a proof, enlarge a hypothetical counterexample to an edge-maximal non-Hamiltonian graph. Adding a missing edge creates a Hamiltonian cycle, hence the original graph has a Hamiltonian path . If both and are edges, the path closes to a cycle by reversing its final segment. Thus the index sets of these two kinds of edges are disjoint in , giving , a contradiction. The degree condition is sufficient and need not follow from a lower bound of on every individual degree.
Let be a first-order consistent arithmetic first-order theory with the Hilbert-Bernays-Löb derivability conditions, and suppose . Provability of and provability of falsity are equivalent inside , because either refutable first-order sentence implies the other. Thus is equivalent inside to its formal consistency statement. The second incompleteness theorem gives .
For integers , the standard Rodrigues' formula has the endpoint value and squared norm displayed above. The lowest-power term after differentiations is , giving the endpoint value after division by . For the norm, integrate by parts times against the same polynomial; its leading coefficient is , so the final derivative is . All boundary terms vanish and the remaining Gamma function integral is . Normalizing the value at zero to one divides the polynomial by and its squared norm by the square of that factor. Only when or do these normalizations already coincide.
For a vector state on a C-star algebra, and . Thus is a well-defined linear isometry from the quotient pre-Hilbert space onto . It extends to an isometry from the completed GNS space onto : its range is complete and therefore closed, and contains the dense subspace . The space is invariant under both and its adjoints. On quotient vectors, , proving the displayed unitary equivalence after continuity. The cyclic vector maps to .
If , then , since the rank-one map sends to any chosen . In this case, for the rank-one orthogonal projection , is equivalent to , by evaluating at and using .

Pinned article: Introduction to the OurBigBook Project

Welcome to the OurBigBook Project! Our goal is to create the perfect publishing platform for STEM subjects, and get university-level students to write the best free STEM tutorials ever.
Everyone is welcome to create an account and play with the site: ourbigbook.com/go/register. We belive that students themselves can write amazing tutorials, but teachers are welcome too. You can write about anything you want, it doesn't have to be STEM or even educational. Silly test content is very welcome and you won't be penalized in any way. Just keep it legal!
We have two killer features:
  1. topics: topics group articles by different users with the same title, e.g. here is the topic for the "Fundamental Theorem of Calculus" ourbigbook.com/go/topic/fundamental-theorem-of-calculus
    Articles of different users are sorted by upvote within each article page. This feature is a bit like:
    • a Wikipedia where each user can have their own version of each article
    • a Q&A website like Stack Overflow, where multiple people can give their views on a given topic, and the best ones are sorted by upvote. Except you don't need to wait for someone to ask first, and any topic goes, no matter how narrow or broad
    This feature makes it possible for readers to find better explanations of any topic created by other writers. And it allows writers to create an explanation in a place that readers might actually find it.
    Figure 1.
    Screenshot of the "Derivative" topic page
    . View it live at: ourbigbook.com/go/topic/derivative
  2. local editing: you can store all your personal knowledge base content locally in a plaintext markup format that can be edited locally and published either:
    This way you can be sure that even if OurBigBook.com were to go down one day (which we have no plans to do as it is quite cheap to host!), your content will still be perfectly readable as a static site.
    Figure 5. . You can also edit articles on the Web editor without installing anything locally.
    Video 3.
    Edit locally and publish demo
    . Source. This shows editing OurBigBook Markup and publishing it using the Visual Studio Code extension.
  3. https://raw.githubusercontent.com/ourbigbook/ourbigbook-media/master/feature/x/hilbert-space-arrow.png
  4. Infinitely deep tables of contents:
    Figure 6.
    Dynamic article tree with infinitely deep table of contents
    .
    Descendant pages can also show up as toplevel e.g.: ourbigbook.com/cirosantilli/chordate-subclade
All our software is open source and hosted at: github.com/ourbigbook/ourbigbook
Further documentation can be found at: docs.ourbigbook.com
Feel free to reach our to us for any help or suggestions: docs.ourbigbook.com/#contact