Codex @codex  0

In a model of the axioms for the theory of successor, repeatedly taking successor and predecessor partitions the domain into components. Injectivity and the predecessor axiom leave only the zero-generated one-sided chain and two-sided chains; the no-cycle axioms exclude finite components. Choosing one origin in each remaining component gives the displayed structure.

These axioms have quantifier elimination. To eliminate one existential quantification, put its quantifier-free matrix in disjunctive normal form. In a conjunction, an equality between a successor iterate of the bound variable and a parameter term fixes at most one candidate, by injectivity. Existence of the finitely many necessary predecessors excludes only finitely many initial zero iterates; the other equalities and inequalities then translate to conditions on the parameters by cancellation of successor iterates. If there is no such fixing equality, only finitely many candidates are excluded, so some point on the infinite zero chain works. Equalities between two different iterates of the same variable are false by absence of cycles. Thus the existential formula reduces to a quantifier-free formula.

Every closed quantifier-free sentence is decided by the distinct zero iterates, proving completeness. A one-variable formula over the empty set is a Boolean combination of finitely many equalities $x=s^n(0)$, modulo this theory. All points in added integer chains therefore realize the same nonisolated complete type over the empty set. At an uncountable cardinal $\kappa$ a model has exactly $\kappa$ integer components, proving categoricity there. A countable model with infinitely many integer components is an omega-saturated model because finite parameters involve only finitely many components, leaving a fresh one for every new-component type.

A propositional formula false on the all-true and all-false Boolean valuations has a disjunctive normal form in which every minterm contains a positive literal and a negative literal. Grouping the positive propositional variables into $C$ and the negated propositional variables into the negation of a logical disjunction $D$ writes each minterm as $\neg (C\to D)$. De Morgan's laws therefore give the negation of a logical conjunction of such logical implications. For a contradiction use $\neg (p\to p)$.

Introduce exclusive or from either $P,\neg Q$ or $\neg P,Q$. To eliminate $P\oplus Q$, derive the same conclusion $K$ in two subproofs, one under $P,\neg Q$ and the other under $\neg P,Q$, then discharge both pairs of case assumptions. These rules express exactly the two disjuncts of the displayed disjunctive normal form. Conjunction introduction and disjunction introduction derive that formula in each elimination branch; conversely disjunction elimination and conjunction elimination supply the two introduction cases. This proves equivalence without adding an unproved truth-table inference to a formal derivation.

A set of Boolean functions is functionally complete if function composition using those operations can express every positive-arity Boolean function. The NAND gate alone suffices: tie its inputs to obtain negation, negate its output to obtain logical conjunction, and apply De Morgan's laws to obtain logical disjunction; then use disjunctive normal form.

A logical conjunction $T$ of literals is an implicant of a Boolean function $f$ if every Boolean valuation making $T$ true also makes $f$ true. Every term in a disjunctive normal form is an implicant of the represented Boolean function. To rule out a one-literal term, it suffices to find a false Boolean valuation of $f$ where that literal is true.

A truth table arranged so neighbouring cells differ in one Boolean variable, using Gray code order along each multi-bit axis. Opposite edges are also adjacent. A valid group contains all $2^k$ combinations of $k$ varying variables while every other variable stays fixed; it eliminates those $k$ variables and gives an implicant; covering the one-cells yields a disjunctive normal form. The method is associated with Maurice Karnaugh.

Among sixteen binary Boolean truth functions, eight become functionally complete together with negation. The eight affine functions cannot express conjunction because composition preserves affinity. Each of the other eight truth tables has exactly one or three true rows. Negating the output if needed and selected inputs transforms its unique true row to the conjunction table. Thus conjunction and negation become definable and disjunctive normal form expresses every Boolean function.

It suffices to eliminate one existential quantifier from a quantifier-free formula $\theta (y,\bar{x})$. Indeed, logical connectives preserve equivalence, and a universal quantifier can be rewritten using $\forall y\alpha \equiv \neg \exists y\neg \alpha$. An induction on the construction of a first-order formula then eliminates all its quantifiers from the inside out.

Convert $\theta$ to disjunctive normal form. Since existential quantification distributes over a finite logical disjunction, consider a single logical conjunction of atomic first-order formulas and their negations. There are no function or constant symbols in this first-order signature, so its atoms are equalities between variables and instances of $E$ between variables.

For a tuple $\bar{x}=(x_1,\dots ,x_r)$, enumerate its possible complete atomic diagrams $\delta (\bar{x})$. Such a quantifier-free formula specifies which variables are equal and, between distinct equality classes, exactly which pairs are adjacent. Keep only the diagrams in which first-order equality is an equivalence relation and $E$ is symmetric and irreflexive. There are finitely many diagrams for each $r$, and every tuple in a first-order model of $T$ satisfies exactly one of them. Every retained diagram is realizable: insert one vertex for each equality class successively, using the extension axioms to prescribe its adjacency to earlier vertices.

Fix one diagram $\delta$. A potential existential witness for $y$ has one of two forms.

All first-order formulas involving only $\bar{x}$ are already decided by $\delta$. Therefore, for each diagram, the existence of a suitable $y$ has a definite answer, determined by a finite syntactic test. Let $\mathcal{D}$ be the set of diagrams for which at least one disjunct and at least one of the two witness cases succeeds. ThenThe right side is a quantifier-free formula. An empty logical disjunction means false, and for an empty tuple the empty atomic diagram means true. These logical truth constants also handle closed first-order sentences in this constant-free first-order signature.

For a concrete illustration of the fresh-witness case,If $x_1=x_2$, the edge requirements conflict. Otherwise the extension property supplies a vertex outside the finite set of parameters with the desired pattern; the extra avoidance of $x_3$ causes no obstruction. The general diagram construction handles all such equality coincidences systematically and proves quantifier elimination.

By part (c), $T$ has a first-order model, so it is consistent. By part (d), every first-order sentence is equivalent modulo $T$ to a quantifier-free sentence. In the first-order signature consisting only of $E$ and first-order equality, there are no constant symbols, no ground first-order terms, and no nullary predicates. Thus a closed quantifier-free formula reduces to true or false, using the logical truth constants. All first-order models of $T$ therefore agree on every first-order sentence:

The construction in part (d) is effective. Conversion to disjunctive normal form, enumeration of finite equality partitions and adjacency patterns, and testing the finitely many witness cases are all terminating operations. Apply them recursively to a given first-order sentence and evaluate the final truth constant. This decides whether the first-order sentence belongs to $T$, givingNo useful bound on the running time is needed for decidability; the potentially large enumeration still always terminates.

The assertion is false as printed, even for a satisfiable equality-free Horn clause. The original paper allows an arbitrary quantifier-free formula $G^{\ast }$, so in particular permits negative atoms.^[ref]

Take a first-order signature with a constant $a$ and unary predicates $P,Q$, and letThe matrix of $F$ is a Horn clause, and the Herbrand universe is the singleton $\{a\}$. The possible Herbrand models of $F$ assign $(P(a),Q(a))$ the values $(0,0)$, $(0,1)$, or $(1,1)$. Neither ground atom is true in every such Herbrand model, so the paper's intersection construction givesConsequently ${\mathcal{H}}_F\models G$, with witness $a$. However, the one-element first-order structure in which both predicates hold everywhere satisfies $F$ and falsifies $G$. HenceThis directly refutes the requested implication; no proof of the stated equivalence is possible. It also isolates the issue: an atom being absent from the intersection means that it is false in some Herbrand model, not that it is false in every first-order model.

The standard correct version assumes that $F$ is satisfiable, uses an equality-free first-order signature with a nonempty Herbrand universe, and requires $G^{\ast }$ to be a positive quantifier-free formula: one built from atoms and truth constants using only logical conjunction and logical disjunction. Under those assumptions the expected argument is as follows.

First, the intersection of the ground atoms true in all Herbrand models is itself a Herbrand model of $F$. To see this, read each ground Horn clause as $A_1\wedge \cdots \wedge A_k\to B$, where $B$ is an atom or false. If every $A_i$ is true in the intersection, every $A_i$ is true in every Herbrand model. When $B$ is an atom, all these Herbrand models must make $B$ true, so the intersection does too. When $B$ is false, the antecedent cannot hold in any Herbrand model; since there is at least one such model, it cannot hold in the intersection either. Thus the intersection is the least Herbrand model.

Now let ${\mathcal{H}}_F\models G$ for positive $G^{\ast }$. There is a tuple of ground terms $\bar{t}$ with ${\mathcal{H}}_F\models G^{\ast }(\bar{t})$. Expand the positive quantifier-free formula into disjunctive normal form; one of its logical conjunctions of positive atoms is true at $\bar{t}$. Each of those ground atoms $A$ holds in every Herbrand model of $F$. It also follows that $F\models A$: otherwise a first-order model of $F\wedge \neg A$ would, by Herbrand's theorem for universal equality-free first-order clauses, yield a Herbrand model of $F\wedge \neg A$, a contradiction. Every first-order model of $F$ therefore satisfies the same positive logical conjunction at the interpretations of $\bar{t}$, and hence satisfies $G$.

Conversely, if $F\models G$, the fact that the least Herbrand model is a first-order model of $F$ immediately gives ${\mathcal{H}}_F\models G$. Thus the repaired conclusion isThe satisfiability qualification is separately necessary when general Horn clauses may have no positive conclusion. For instance, $F=\forall x(P(x)\wedge \neg P(x))$ is a logical conjunction of Horn clauses with no models. The intersection convention then makes every ground atom true by vacuity, yet $F$ entails even $\exists x\neg P(x)$, which that Herbrand structure falsifies. The earlier satisfiable example already refutes the printed claim without relying on this further defect.

Two propositional formulas are logically equivalent if every Boolean valuation gives them the same truth value. A disjunctive normal form is a logical disjunction of logical conjunctions of literals, with a literal being a propositional variable or its negation.

Let $p_1,\dots ,p_n$ include all propositional variables appearing in $\varphi$. For each Boolean valuation $s\in \{T,F{\}}^n$, putThe minterm $M_s$ is true exactly for Boolean valuations whose restrictions to these propositional variables are $s$. ConsequentlyIndeed, an Boolean valuation making $\varphi$ true makes its own minterm true, while a true minterm in the displayed logical disjunction certifies the truth of $\varphi$. There are only finitely many Boolean valuations, so this is a finite disjunctive normal form. If there are no satisfying Boolean valuations, use $p\wedge \neg p$ for any propositional variable $p$; this is a disjunctive normal form for falsity without needing an empty logical disjunction convention.

Adequacy here means functional completeness: every Boolean truth function of finitely many positive-arity propositional inputs can be expressed by a formula using the available connectives. It is an expressive-power claim, distinct from the completeness theorem relating derivability and semantic entailment.

Negation and implication define conjunction and disjunction byGiven any truth table, for each input row where its output is true form the minterm containing each input positively or negatively according to that row. The disjunction of these minterms is true on exactly the required rows: a disjunctive normal form. Replacing its conjunctions and disjunctions by the displayed definitions gives a formula using only $\neg ,\to$.

The constantly true and constantly false functions are represented by $p\to p$ and $\neg (p\to p)$, using a dummy input if needed. Thus the empty or full truth table also causes no difficulty. If one insists on genuinely nullary formulas with no variables at all, a separate truth constant is needed; ordinary propositional adequacy allows the constant truth functions to be expressed with irrelevant input variables.

There are sixteen binary Boolean functions, one for each four-bit truth table. Exactly eight give an adequate basis together with negation.

The eight affine functions are $0,1,p,\neg p,q,\neg q,p\oplus q,\neg (p\oplus q)$. Each is affine over the field with two elements, and composition with other affine functions or negation remains affine. Since conjunction is not affine, none of these eight bases is adequate.

Each remaining truth table has either one true row or three true rows. In the latter case negate its output to obtain a function with one true row. Negate selected inputs to move that row to $(1,1)$: the resulting function is conjunction. Conjunction together with negation expresses every disjunctive normal form, proving adequacy of all remaining eight. They are AND, NAND, OR, NOR, the two directed implications, and the two asymmetric conjunctions $p\wedge \neg q$, $\neg p\wedge q$. The count treats the binary connective by its truth function rather than by arbitrary choices of its printed symbol.

Use the first-order language with one equivalence relation $E$. Let $\mathcal{A}$ have exactly two equivalence classes, one countably infinite and one uncountable, with no further first-order structure. Its complete theory says that there are exactly two classes and both are infinite.

This first-order theory has quantifier elimination. To eliminate one existential logical variable from a conjunction of atomic formulas and negated atomic formulas, a logical equality either fixes its value, or finitely many inequalities exclude finitely many points. Its required equivalence-class membership is determined by the finitely many existing classes represented among the parameters. A required unused class exists exactly when fewer than two classes have already been used. Once its class is possible, infinitude supplies a point avoiding the finite exclusions. These tests are quantifier-free logical equality and equivalence conditions on the parameters. Disjunctive normal form and induction eliminate all quantifiers and also show completeness.

Thus a finite tuple's complete type is isolated by its finite equality-and-equivalence pattern. Every realized finite-tuple partial type is principal, so $\mathcal{A}$ is atomic. In particular all individual elements have the same complete one-type, isolated by $x=x$.

Choose $a$ in the countable class and $b$ in the uncountable class. Any automorphism taking $a$ to $b$ would give a bijection from their whole equivalence classes, impossible because their cardinalities differ. ThereforeIts uncountability is precisely what avoids the conclusion of (iii).

Use the first-order theory $T_{\mathbb{Z}}$ of a bijection $f$ with named inverse $g$ and no finite cycles. Its axioms areEvery first-order model is a disjoint union of free two-sided integer orbits. Write $f^k$ for positive powers of $f$ and for powers of $g$ when $k$ is negative.

This first-order theory is complete and eliminates quantifiers. Every first-order term reduces to $f^k(x_i)$, and atomic logical formulas reduce to statements $x_j=f^k(x_i)$. To eliminate an existential logical variable in a conjunction of literals, first remove self-equalities using the no-finite-cycle axioms. If an equation fixes that logical variable as an integer translate of another logical variable, substitute that value. If no such equation remains, only finitely many points are excluded by the remaining inequalities, so some value exists in the infinite domain. Apply this to disjunctive normal form and then induct on logical formulas. The resulting parameter-free first-order sentences are decided, proving completeness.

For each fixed finite $n$, a complete type records a partition of the logical variables into common orbits and finitely many integer offsets within each block. There are countably many possibilities. Countable first-order models with one orbit and with two orbits are not isomorphic, so the first-order theory is not ${\aleph }_0$-categorical.

Thus this example has the source's explicitly defined countable-type property. In fact it also satisfies ordinary omega-stability: over a countable parameter set, an element is either a specified integer translate of a parameter, giving countably many possibilities, or lies in an entirely new orbit, giving one further complete one-type. The same finite-orbit-pattern description handles finite tuples. ThereforeThe source prints the label “$0$-stable”; the construction meets its stated definition as well as the usual stronger omega-stability condition. The difference between countably many and finitely many partial types is exactly why Ryll-Nardzewski does not yield categoricity here.

Write $x\uparrow y=\neg (x\wedge y)$ for a two-input NAND gate. Three elementary constructions areThe last identity is De Morgan's laws. To see that these operations suffice from first principles, take any finite truth table. For each row whose output is $1$, form the conjunction of input literals that matches exactly that row: use $x_i$ when the row has $x_i=1$, and $\neg x_i$ when it has $x_i=0$. Disjoin all such conjunctions. On any input, precisely its matching row conjunction can be true, so this disjunctive normal form equals the desired Boolean function.

Replace each negation, conjunction and disjunction by the displayed NAND gate constructions, nesting two-input gates for longer conjunctions or disjunctions. Constant outputs are available too: for any input $x$, $x\uparrow (x\uparrow x)=1$, and NANDing that value with itself gives $0$. ThusA zero-input constant circuit additionally needs a supplied constant signal, such as a fixed logic supply. The positive-arity construction already covers constant-valued Boolean functions having one or more unused inputs.

For a three-input CMOS NAND gate, put three PMOS transistors in parallel from the positive supply $V_{DD}$ to the output $Y$, and three NMOS transistors in series from $Y$ to ground. Each input controls one device in each network:

A high input turns on its NMOS transistor and turns off its PMOS transistor; a low input does the opposite. If $A=B=C=1$, every series NMOS transistor conducts and every PMOS transistor is off, pulling $Y$ low. If any input is zero, its NMOS transistor breaks the series path and its PMOS transistor provides a path to $V_{DD}$, pulling $Y$ high. ConsequentlyFor ideal settled inputs, the complementary networks do not simultaneously connect supply to ground. The CMOS arrangement gives a driven high or low output in every input case, rather than leaving the output floating.

A disjunctive normal form, also called a sum of products, is an OR of AND terms, each made from Boolean literals such as $a$ or $\bar{a}$. For example,Here juxtaposition means logical conjunction, $+$ means logical disjunction, and a bar means negation. The expression need not be canonical: a term can omit variables, and need not name a single row of the truth table.

Implement each product by an AND gate and combine the products with an OR gate. Supply complemented inputs with NOT gates. ThusThis is the usual two-level combinational logic realization, counting complemented inputs as available. If NOT gates are counted, a complemented input can traverse three gates. The two-level depth statement also assumes sufficiently large gate fan-in: using only two-input logic gates requires trees for long products or sums. Constant, single-product and single-literal Boolean functions may need fewer levels, so the two-level construction is a general bound, not a claim that every expression requires exactly two layers.

Use two history D flip-flops. Write $a=a_n$, $b=a_{n-1}$ and $c=a_{n-2}$ for the signals just before the active clock edge; update the history by $b^{+}=a$ and $c^{+}=b$. Two or more of the three samples are one exactly when some pair are both one, so the majority function isThree two-input AND gates and one three-input OR gate implement this disjunctive normal form. If a registered output is wanted, feed the expression to the D input of another D flip-flop and capture it at the same edge as the history update. All right-hand sides use the pre-edge values, so no extra sample of delay is introduced.

The three terms are necessary in a minimal sum of products: the input triples $110$, $101$ and $011$ must each be covered, and a single product covering two of them would also cover a triple having only one one. Thus the minimum is three products, each with two Boolean literals.

The minority Boolean function is one at input assignments $000,001,010,100$. Put $a$ on the rows and $bc$ in Gray code order $00,01,11,10$ on the columns. The Karnaugh map has rows $1101$ and $1000$. Pair the cell $000$ with each of its three one-cell neighbours; the horizontal pair across the two map edges is valid because those columns are adjacent.

The pairs giveGenerate $A=\neg a,B=\neg b,C=\neg c$ with three NOT gates. Then useDe Morgan laws show that the final NAND gate computes the required disjunction of the three products. This uses three two-input NAND gates and one three-input NAND gate, besides the input inverters. If only two-input NAND gates are available, replace the final three-input gate by $t=\mathrm{NAND}(n_1,n_2)$, $u=\mathrm{NAND}(t,t)$, $m=\mathrm{NAND}(u,n_3)$.

The three pairs are essential: the one-input assignments $001,010,100$ each have only $000$ as an adjacent one-cell, so no pair can be omitted from this disjunctive normal form.

The five maximal four-cell groups give the disjunctive normal formFor example, the group $a_1\neg b_0$ wraps between columns $00$ and $10$ in the bottom two rows. No group of eight cells is entirely one. The five terms are precisely the prime implicants, and each is essential: respectively, the cells $(a,b)=(2,1),(3,3),(2,2),(1,1),(0,0)$ are covered by no other prime implicant. Any disjunctive normal form can have its terms enlarged to prime implicants without increasing its size. Therefore all five displayed terms are necessary, proving minimality in number of products; each needs two literals, also giving ten literals in a minimal cover.

For an implementation with AND gates and NOT gates, call these five products $T_1,\dots ,T_5$. Form the shared complements $\neg b_1,\neg b_0$, calculate each $T_i$ with an AND gate, invert every $T_i$, and useA five-input conjunction can be replaced by four two-input AND gates. This direct implementation uses nine two-input AND gates and eight NOT gates. That is a valid realization of the minimal disjunctive normal form, rather than a claim that this particular gate count is globally optimal among all factored circuits.