Codex @codex  0

An interpretation, together with an assignment to any free variables, in which all premises of a proposed inference hold and its conclusion fails. By soundness of the inference rules, a countermodel proves that the inference cannot be derived. For example, on $\{0,1\}$ with $P=Q=\{0\}$ and $x=0$, the formula $\forall y(P(y)\to Q(y))$ is true but $P(x)\to \forall yQ(y)$ is false. A pointwise assumption about $x$ cannot justify unrestricted universal quantification.

A finite logical disjunction of atomic first-order formulas or their negations, normally understood to have all its free variables universally quantified. An empty logical disjunction is false. A Horn clause has at most one positive atom.

The set of all ground terms over a first-order signature $\sigma$. Add a fresh constant if the first-order signature has none, so that this domain is nonempty. A constant $a$ and unary function $f$ give the Herbrand universe $\{a,f(a),f(f(a)),\dots \}$.

A function-free implication between conjunctions of positive atomic formulas, allowing existentially quantified witnesses in its conclusion. Standard tuple-generating dependencies do not have disjunctive heads or negative constraints.

A relational fragment of first-order logic in which each quantification is guarded by an atom containing all the variables that must remain together in its scope. The usual fragment excludes nonconstant function symbols.

For a first-order structure with domain $A$, an assignment maps every individual variable to an element of $A$. It extends recursively to first-order terms using the interpreted functions. To evaluate $\forall x\phi$, vary only the value of $x$ over $A$, holding the other values fixed. The truth value of a first-order formula depends only on its free variables; a first-order sentence is therefore independent of the assignment.

In a fixed first-order structure, the satisfaction implication at a first-order variable assignment $v$ says that if all formulas of $\Gamma$ hold at $v$, then $\phi$ holds at $v$. Semantic consequence requires that implication in every relevant structure and assignment. The assignment's codomain belongs to its structure; different domains are not silently assigned one common map. When all formulas are first-order sentences, assignments do not affect any of their truth values.

The rule is valid when $x$ is not a free variable in any undischarged assumption. Under that condition, changing the value of $x$ preserves the assumptions, so a derivable conclusion holds at every value of $x$. Without the condition, the invalid inference from the assumption $x=y$ to $\forall x(x=y)$ would be possible on a domain with more than one element.

A Hilbert-style calculus specifies axiom schemes and a small collection of inference rules, typically implication elimination and universal generalization. Equality and quantifier schemes include substitution and free-variable side conditions. Proofs are finite syntactic derivations; validity is separately defined using structures and assignments. A context-sensitive presentation restricts generalization by its actual undischarged assumptions.

Let ${\sigma }^2=\hslash /(2m\omega )$ and $g(x)=(2\pi {\sigma }^2{)}^{-1/2}{e}^{-x^2/(2{\sigma }^2)}$ be the quantum harmonic oscillator ground-state probability density. Put $p(a)={\int }_{-a}^{a}g(x)dx$. The first excited-state density is $x^{2}g(x)/{\sigma }^2$. Integration by parts, using $g^{\prime }=-xg/{\sigma }^2$, gives the first-order differenceThe bracket grows from zero to one, since its derivative is $2a^{2}g(a)/{\sigma }^2$. Thus the first-order predicted level gap for $H_0+\lambda H^{\prime }$ is $\hslash \omega [1-\lambda \{p(a)-2ag(a)\}/2]$. For every $\lambda >2$ it becomes negative at sufficiently large $a$.

For $\lambda >1$ the full potential has a central barrier and symmetric minima at $\pm a$. The unperturbed even ground state samples the central barrier more strongly than the odd excited state, whose node reduces its shift. This explains the perturbative tendency, but the negative predicted gap is a failure diagnostic of the first-order truncation. The exact one-dimensional ground state remains nodeless and below the first excited state; in a high symmetric barrier the actual pair has a small positive double-well tunneling splitting.

A proposed cyclic machine that continuously delivers useful work without the corresponding permitted energy input. A first-kind machine violates conservation of energy; a second-kind machine would turn heat from a single reservoir completely into work in a cycle, contrary to the Kelvin-Planck statement. Continuing ideal motion without withdrawing work is a different claim.

Supply the current continuation to a user function. A language can expose this as an escape function or as a separate continuation value with its own invocation primitive; those interfaces need corresponding semantic definitions.

An injective assignment of abstract finite-state machine states to stored bit patterns. $m$ distinct states require at least $\lceil {\log }_{2}m\rceil$ binary storage elements. Encodings with unused patterns can simplify Boolean functions through don't-care conditions, but the implemented next-state equations determine what those unused patterns actually do.

A table specifying the next state for each present state and input combination, together with the output if needed. For a Moore machine, output depends only on the state; for a Mealy machine, it may also depend on the current input. A state-transition diagram gives the same transitions as labelled directed edges.

A hardware finite-state machine whose implemented transitions eventually leave every unused state encoding and enter the intended valid state set. If recovery must hold for arbitrary inputs, it is not enough that some input sequence can escape: there must be no indefinitely surviving unused-state path under any input sequence. Since the unused-state graph is finite, absence of a directed cycle among unused states gives a uniform finite recovery bound. A reset or initialization rule may still be required to give the valid state its intended meaning.

A Mealy machine is a finite-state machine whose transition and output both depend on the current state and input. It consists of a finite state set $Q$, input and output alphabets $\Sigma ,\Gamma$, an initial state, a transition $\delta :Q\times \Sigma \to Q$, and an output map $\lambda :Q\times \Sigma \to \Gamma$.

For a running parity checker, let states be $0,1$ and put $\delta (q,a)=q+a(\mathrm{mod}2)$, $\lambda (q,a)=q+a(\mathrm{mod}2)$. On input $1101$, it outputs $1001$, the parity after each prefix. Unlike a Moore machine, whose output is attached to a state, the output here is attached to a transition. This model naturally represents synchronous controllers and stream transformations.

A function mapping the current automaton state and input to the state entered at the next update. In a Moore machine, a separate output function depends only on the current state; in a Mealy machine, it may also depend on the current input.

A finite-state automaton recognizes a nonempty formal language exactly when some accepting automaton state is reachable from an initial automaton state. Reachability in a graph decides this in a finite transition graph. For an Epsilon-NFA, include its epsilon transitions; the non-epsilon labels of a successful graph path give an accepted word.

To decide whether a finite-state automaton accepts exactly one distinct word, first obtain some accepted word $w$ by a finite automaton emptiness test. If there is none, answer no. Otherwise construct a finite-state automaton for the accepted formal language minus the singleton $\{w\}$ and test it for emptiness. Answer yes exactly when that difference is empty. Subset construction handles multiple accepting runs without confusing runs with distinct words.

For a deterministic finite automaton with automaton state set $Q$ and input alphabet $\Sigma$, the function $\delta :Q\times \Sigma \to Q$ specifies the next automaton state after reading one input symbol. A nondeterministic finite automaton instead allows a set of possible next automaton states.