Topics (384k) Articles (398k) Users (410) Discussions (242) Comments (383) Files (13k) New article
In propositional logic with the usual two truth values, negating a proposition twice preserves its truth value. Thus the complement of a set taken twice, in one fixed universal set, is the original set.
A propositional formula semantically entails when every Boolean valuation satisfying satisfies . Equivalently, is an unsatisfiable Boolean formula. Deciding semantic entailment is co-NP-complete: a counterexample Boolean valuation certifies failure in polynomial time, while reduces unsatisfiability to semantic entailment.
An indivisible statement treated as either true or false. In a labelled transition system, an atomic proposition holds at state exactly when .
From Boolean clauses containing complementary Boolean literals, derive the Boolean clause formed by removing that complementary pair and taking the remaining Boolean literals. For example, resolving with gives . Backward proof search with a positive-headed Horn clause and an all-negative query is a restricted use of this rule.
A propositional variable is an atomic symbol assigned a truth value by a Boolean valuation. A propositional formula is built from these symbols by logical connectives. The variables carry no quantifiers over individuals; their values may be chosen independently.
An inference rule deriving a clause from two clauses containing complementary literals. In propositional logic the displayed rule eliminates the atom . For first-order clauses, complementary atoms can first be made identical by a suitable first-order substitution.
A Hilbert proof system specifies axiom schemes and inference rules, commonly including modus ponens. A formal proof is a finite sequence of axiom instances, permitted assumptions and conclusions obtained from preceding lines by those rules. Soundness and completeness compare this syntactic derivability with semantic validity or semantic entailment. These properties concern the particular chosen axioms and rules.
A procedure passed as an argument to another procedure. For a nested procedure under lexical scope, the argument must preserve both its code and its defining environment, for example as a programming closure.
Here and are real functions of time. Differentiation in position gives . The standard probability current is thereforeFor a coherent state moving in a quadratic Hamiltonian, the centre follows the classical equation , so the current is the normalized Gaussian probability density transported at its centre velocity. The factor is essential: omitting it changes the current by a dimensional constant and violates the continuity equation for the normalized density. A spatially constant phase does not affect the current.
Let two first-order models satisfy a complete theory and suppose every element of the first is the value of a closed term. Send each such value to the value of the same first-order term in the second first-order model. Completeness decides all logical equality first-order sentences, making this map well-defined and injective. It also decides every logical formula with closed terms substituted, making the map elementary. Thus the first first-order model is prime.
The prime ideals of with are the zero ideal and the principal ideals generated by nonconstant primitive polynomials that are irreducible in .
To prove the description, invert the nonzero integers to obtain the localization . The extension of an ideal consists of the polynomials with and . Its contraction is : if and , the defining condition puts , so primeness gives . The prime ideal correspondence for localization makes this extension a proper prime ideal of .
If , its extension has a nonzero generator because is a principal ideal domain. Dividing this generator by its rational polynomial content gives an integer-coefficient primitive polynomial generating the same extended ideal. Divisibility descent by Gauss lemma for polynomials then gives in . The proper prime ideal in makes irreducible there. Conversely, any such polynomial generates a prime ideal in whose contraction is and whose intersection with is zero.
The intersection condition is essential: is a maximal ideal of , since its quotient ring is , but it is not principal. A common divisor of and must be a unit, which would generate the whole ring.
Along a boundary-layer streamline directed by increasing , an adverse pressure gradient is a rise in pressure in the direction of flow. The associated pressure gradient force opposes the velocity. In a steady inviscid outer stream the Euler equation gives , so a positive gradient decelerates a positive outer velocity. Within a viscous boundary layer the slower fluid near the wall has less streamwise momentum and can reverse while the outer stream still moves forward. The onset of flow separation is therefore associated with vanishing and then reversed wall shear stress. A pressure rise does not by itself locate separation: the full boundary-layer solution and upstream history also matter.
A pressure increment applied to a confined fluid in equilibrium is transmitted throughout it. The pressure increment is a scalar, not a force vector copied in one direction. Comparing different heights also requires the hydrostatic pressure difference. Finite-speed pressure wave propagation precedes the new equilibrium.
A pressure difference compares the pressures at two stated locations or against two reference states. With , a positive value means location one has higher pressure. A membrane or piston with equal effective face areas experiences a net pressure force of magnitude , even if both absolute pressures are large.
For example, pressures and across give a net pressure force of . A liquid-column manometer converts a pressure difference to a vertical level difference through hydrostatic pressure, while a differential pressure transducer senses it directly. Comparing ports at different heights requires accounting for the fluid between them. During flow, the relation between pressure difference and volumetric flow rate also depends on geometry, viscosity and other contributions to the energy balance.
For the Hermite differential equation with real , the wavefunction is square integrable on the real line only if is a polynomial. To prove this without assuming that even and odd tails cannot cancel, project a square-integrable solution onto its even and odd parts first. Each projection remains square integrable and satisfies the same equation.
In either nonterminating parity sequence, obeysThe tail has constant complex phase. For any fixed , comparison with bounds its coefficient magnitudes below by for sufficiently large . Thus on the positive real axis the tail dominates a positive multiple of after subtraction of finitely many terms. The Gaussian function factor leaves exponential growth , contradicting the square-integrable condition. Hence each nonzero parity sequence terminates. Its top coefficient forces , giving Hermite oscillator quantization and a Hermite polynomial of degree .
At a stationary point of the power penalty, define the displayed multiplier estimates. Its stationarity equation becomes . If and these multipliers are bounded, then each . Along any convergent primal subsequence, a further multiplier subsequence converges and yields equality-constrained first-order KKT conditions at the limit. This is a statement about finite cluster points: bounded multipliers alone do not prove convergence or boundedness of the primal iterates.
In uniform gravity a body's gravitational potential energy is its mass times gravitational acceleration times the Cartesian height of its centre of mass. If that height is represented by an axis distance and tilt angle , it is and the energy becomes . Treating simultaneously as a Cartesian height would introduce an extra, unjustified cosine.
Historical pharmaceutical preparation; its composition and clinical use must be identified by edition. [ref]
The Essentials of Materia Medica and Therapeutics by Alfred Baring Garrod (1865). corresponding monograph and British preparation
Near an equilibrium, a positive-definite scalar function has value zero at that point and is strictly positive at every other nearby point. This scalar notion differs from positive definiteness of a kernel.
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!
Intro to OurBigBook
. Source. We have two killer features:
- 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-calculusArticles 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/derivativeVideo 2. OurBigBook Web topics demo. Source. - 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.
- to OurBigBook.com to get awesome multi-user features like topics and likes
- as HTML files to a static website, which you can host yourself for free on many external providers like GitHub Pages, and remain in full control
Figure 2. You can publish local OurBigBook lightweight markup files to either OurBigBook.com or as a static website.Figure 3. Visual Studio Code extension installation.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. - Infinitely deep tables of contents:
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





