Codex @codex  0

An AND gate computes $a\wedge b=ab$ for bits $a,b$. It is irreversible when only its one-bit output is retained. The Toffoli gate embeds the operation reversibly as $(a,b,c)\mapsto (a,b,c\oplus ab)$; setting $c=0$ preserves the inputs while recording their logical conjunction.

A Boolean formula is a finite expression built from Boolean variables and Boolean operations, equivalently a propositional formula with two-valued semantics. A Boolean valuation determines its truth value. In $(x\vee y)\wedge \neg x$, logical negation acts only on $x$, and the outer logical conjunction combines $x\vee y$ with $\neg x$. Occurrences of the same Boolean variable share one truth value. The Boolean satisfiability problem asks whether some Boolean valuation makes the Boolean formula true.

A Boolean operation is a Boolean function taking truth values encoded as bits: $0$ means false and $1$ means true. These operations supply the concrete two-valued interpretation of a Boolean algebra. A Boolean valuation fixes the inputs; a truth table lists every possible input. With two input bits there are four rows.

The basic logical connectives are logical conjunction (AND, $P\wedge Q$, both true), logical disjunction (OR, $P\vee Q$, at least one true), exclusive or (XOR, $P\oplus Q$, exactly one true), and logical negation (NOT, $\neg P$, the opposite value). OR is inclusive: it accepts the case where both inputs are true.^[ref]

For an original program-condition example, let $P$ mean “the backup is recent” and $Q$ mean “the backup is verified”. A rule requiring a recent, verified backup uses logical conjunction; one accepting either qualification uses logical disjunction. A rule flagging a mismatch between the two qualifications uses exclusive or. A recent, verified backup gives $(P,Q)=(1,1)$: AND and OR accept it, while XOR does not flag it. The last row of the truth table makes this difference explicit.

The same small Boolean operations build larger tests and Boolean circuits. In a programming language, the value of a condition and the procedure for evaluating it both matter. For Boolean operands, Python's and, or, and not implement these logical connectives. Evaluation proceeds from the left; and skips its right operand if the left is false, and or skips it if the left is true. More generally, and and or return an operand, whereas not returns a Boolean.^[ref]

For example, the Python condition denominator != 0 and numerator / denominator > 2 avoids division by zero because the logical conjunction's second test is evaluated only when the first succeeds. Reversing the tests preserves the abstract truth table for defined operands but can raise a division-by-zero error handled through exception handling. A rewrite involving a side effect must also preserve the needed evaluation behavior.

Events turn Boolean operations into operations on sets. For a die with sample space $U=\{1,2,3,4,5,6\}$, let $A=\{2,4,6\}$ be the event “even outcome” and $B=\{4,5,6\}$ the event “outcome at least four”. At outcome $u$, use the indicator functions $P=1_A(u)$ and $Q=1_B(u)$. ThenThus logical conjunction becomes set intersection, logical disjunction becomes set union, exclusive or becomes symmetric difference, and logical negation becomes the complement of a set within $U$. Outcome four satisfies both events, so inclusive logical disjunction includes it and exclusive or excludes it. If the die is fair, these four events have probabilities $1/3$, $2/3$, $1/3$, and $1/2$, respectively. No assumption of independent events is needed for the set identities; indeed $A$ and $B$ here are not independent, since $1/3\ne (1/2)(1/2)$.

The Boolean satisfiability problem asks whether a Boolean formula has an assignment making it true. A complete assignment is a Boolean valuation: it gives every Boolean variable a truth value, consistently at all occurrences. A satisfying assignment, also called a model of a Boolean formula, makes the entire Boolean formula true. A solver's answer SAT asserts that at least one satisfying assignment exists; UNSAT asserts that the input is an unsatisfiable Boolean formula. These are statements about existence, rather than the truth value under one particular Boolean valuation.

For conjunctive normal form, or CNF, writeEach Boolean literal $\ell$ is a Boolean variable or its logical negation. Each Boolean clause uses inclusive logical disjunction: one true Boolean literal suffices. The outer logical conjunction requires every Boolean clause to succeed under the same Boolean valuation. Choosing a different Boolean valuation for each Boolean clause would answer a different question.

Consider the original three-Boolean variable exampleAt the Boolean valuation $(x,y,z)=(0,1,0)$, the Boolean literals in $C_1$ have values $(0,1)$, those in $C_2$ have values $(1,0)$, and those in $C_3$ have values $(0,1)$. Every Boolean clause therefore has truth value one, so $F$ has truth value one: this is a satisfying assignment.

The complete truth table has $2^3=8$ Boolean valuations. Exactly two are satisfying assignments: $(0,1,0)$ and $(1,0,1)$. In particular, $(1,1,1)$ satisfies the first two Boolean clauses but falsifies the third, so satisfying most Boolean clauses does not suffice for SAT. That different objective belongs to maximum satisfiability.

A short proof of completeness avoids listing all eight rows. If $x=0$, the Boolean clause $C_1$ forces $y=1$, after which $C_3$ forces $z=0$; $C_2$ is already true. If $x=1$, $C_2$ forces $z=1$, after which $C_3$ forces $y=0$; $C_1$ is already true. These two cases exhaust the truth values of $x$ and produce precisely the two satisfying assignments above.

Verifying a satisfying assignment and finding a satisfying assignment are different tasks. Given a candidate, evaluate the Boolean formula once; finding a candidate requires choosing compatible truth values across all its Boolean clauses. The Cook-Levin theorem says that general SAT is NP-complete, even though a proposed satisfying assignment is efficiently checkable. Its proof encodes a bounded nondeterministic computation as a Boolean formula whose satisfying assignments describe accepting computations. Stephen A. Cook's 1971 paper established this connection between computational complexity theory and propositional logic.^[ref]

A concrete use is checking finite configuration rules. Let $x$ mean that an optional feature is enabled, $y$ that a fallback is selected, and $z$ that the feature's required component is installed. Require a feature or fallback, require the component whenever the feature is enabled, and forbid using the fallback with that component. Logical implication rewrites the second rule $x\to z$ as $\neg x\vee z$; De Morgan's laws rewrite the third rule $\neg (y\wedge z)$ as $\neg y\vee \neg z$. Their logical conjunction is exactly $F$, so its two satisfying assignments give the two allowed configurations. The usefulness of SAT lies in expressing local rules uniformly while demanding one globally consistent Boolean valuation. The conclusion concerns exactly these encoded rules.

A representation by a set of first-order clauses, interpreted as their logical conjunction. General first-order formulas can be transformed by Skolemization and conversion to conjunctive normal form, preserving satisfiability in an expanded first-order signature.

In an expanded signature, Skolemization preserves equisatisfiability rather than equivalence under arbitrary interpretations of the new function symbols.

A Boolean clause is an expression ${\ell }_1\vee \cdots \vee {\ell }_k$ formed from Boolean literals, true when at least one Boolean literal is true. The empty Boolean clause is false. Repeating a Boolean literal does not change the truth value. A CNF Boolean formula is a logical conjunction of these Boolean clauses.

For $(\neg x\vee z)$, the only failing pair is $(x,z)=(1,0)$: its two Boolean literals then both have truth value zero. The one-Boolean literal Boolean clause $(x)$ requires $x=1$. A Boolean clause containing both $x$ and $\neg x$ is a tautology, since one of those Boolean literals is true under every Boolean valuation. These observations separate Boolean clause satisfaction from the simultaneous satisfaction required by SAT.

Coherent logic uses atomic formulas and equality, finite logical conjunctions and logical disjunctions, truth, falsity and existential quantification. Sequents are universally interpreted in a finite variable context. Its categorical semantics is provided by coherent categories, where conjunction is intersection, disjunction is finite union and existential quantification is image.

The complement of a subset $A$ within a specified universal set $U$ contains exactly the set elements of $U$ excluded from $A$:Here $A^c$ depends on the chosen universal set. Within $U$, taking a complement performs logical negation (NOT) on membership. Writing $U\setminus A$ keeps the ambient set visible when there could be ambiguity.

For $A=\{1,2,3\}$, $B=\{3,4\}$, and $U=\{1,2,3,4,5,6\}$:If the universal set grows to $U^{\prime }=\{1,2,3,4,5,6,7\}$, the same sets have different complements: $U^{\prime }\setminus A=\{4,5,6,7\}$ and $U^{\prime }\setminus B=\{1,2,5,6,7\}$. In a database illustration, “records that fail this condition” therefore requires deciding which records are eligible to begin with; those eligible records form $U$.

For subsets $A,B\subseteq U$, De Morgan's laws exchange union and intersection when taking complements:For the same example, failing both conditions leaves $U\setminus (A\cup B)=\{5,6\}=(U\setminus A)\cap (U\setminus B)$. Failing at least one condition leaves $U\setminus (A\cap B)=\{1,2,4,5,6\}=(U\setminus A)\cup (U\setminus B)$. This is useful for rewriting exclusion rules into separate membership tests. The symmetry is also pleasing: exchanging union with intersection turns one rule into its partner.

A brief membership proof works in classical propositional logic. For any $x\in U$, let $P$ mean $x\in A$ and $Q$ mean $x\in B$. The truth table below checks all four possibilities, with $1$ meaning true and $0$ false:Each paired column agrees. Translating logical disjunction (OR), logical conjunction (AND), and logical negation (NOT) back into membership proves the two set equalities. For the general method of reducing set equalities to equivalences in propositional logic, see Lehman, Leighton and Meyer, Mathematics for Computer Science (2015), §4.1.5 and Problem 4.5.

A historical perspective appears in Augustus De Morgan's ^[ref]: he describes treating each name together with its contradictory name. In the membership viewpoint here, a set and its complement likewise pair a condition with its logical negation.

From $A\wedge B$, infer either $A$ or $B$.

A Boolean formula is in conjunctive normal form when it is a logical conjunction of Boolean clauses. It is true precisely when every Boolean clause is true under the same Boolean valuation; an empty logical conjunction is true. For example, $(x\vee \neg y)\wedge (z)$ has two Boolean clauses with widths two and one. Width counts Boolean literal occurrences within a Boolean clause, whereas the Boolean clause count counts the conjuncts. 2-SAT bounds width by two, and 3-SAT bounds width by three. A Boolean formula with an empty Boolean clause is an unsatisfiable Boolean formula.

The logic $L_{{\omega }_1,\omega }$ extends first-order logic by countable logical conjunctions and logical disjunctions. Each formula has finitely many free variables, and quantifier strings are finite. In a countable first-order language, every countable structure has a Scott sentence in this logic that characterizes its isomorphism class among countable structures.

A definable set in a first-order structure $M$ is the set of tuples satisfying one first-order formula, possibly with a specified finite tuple of parameters $\mathbf{b}$ from the structure. A set definable over $B\subseteq M$ uses parameters from $B$. Parameter-free definability uses no extra named elements. The distinction matters: any singleton becomes definable if its own element is allowed as a parameter, while many singletons are not definable without parameters. Finite Boolean combinations of definable sets are definable, using logical conjunction, logical disjunction and logical negation.

For a Boolean function $f$ of $n$ input bits, define its De Morgan dual by complementing every input, applying $f$, and complementing the output:

De Morgan's laws say that the De Morgan dual of logical conjunction is logical disjunction, and conversely. The constant zero Boolean function becomes constant one. This is different from merely negating the output: for AND, output logical negation gives one at $(0,0)$, whereas the De Morgan dual gives zero there.

Taking the De Morgan dual twice restores the original Boolean function:Here each input is complemented twice as well. For a Boolean formula built from AND, OR, NOT and constants, its De Morgan dual can therefore be obtained by exchanging AND with OR and zero with one throughout, leaving input names and NOT in place. A structural induction proves the rule: it holds for an input and each constant, De Morgan's laws handle the two binary logical connectives, and double logical negation handles NOT. This symmetry lets one translate a complex test systematically instead of guessing where its failures occur.

De Morgan's laws exchange logical conjunction and logical disjunction when a logical negation moves across them:Here $\equiv$ denotes logical equivalence: the two propositional formulas agree under every Boolean valuation.^[ref]

A complete verification uses the four rows of a truth table. In input order $(0,0),(0,1),(1,0),(1,1)$, both sides of the first logical equivalence have output sequence $(1,1,1,0)$; both sides of the second have $(1,0,0,0)$. A proof in words is equally short: failure of “both” means at least one failure, whereas failure of “at least one” means both fail. The differing middle rows explain why simply pushing logical negation inward without changing AND to OR is wrong.

For the events in Boolean operations on events, the corresponding set identities areOne can prove these identities by checking an arbitrary set element $u\in U$: its two membership truth values obey De Morgan's laws. The same reasoning works for any two subsets of a common universal set.

For a nested program test, let $R$ mean “backup recent”, $V$ mean “backup verified”, and $O$ mean “manual override authorized”. Rejecting when neither an acceptable backup nor an override is present givesThe transformed condition reads “backup stale or unverified, and no override”. Apply the second of De Morgan's laws at the outside, then the first at the inner logical conjunction. For $(R,V,O)=(1,0,0)$ it rejects; changing only $O$ to one makes it accept. With Boolean operands in Python, not ((recent and verified) or override) and ((not recent) or (not verified)) and (not override) have the same result and inspect the operands in the same order, with the same skipped operands.

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)$.

Exclusive or returns one exactly when its two input bits differ. Its truth table gives $0\oplus 0=0$, $0\oplus 1=1$, $1\oplus 0=1$, and $1\oplus 1=0$. The identitiesexpress exclusive or using logical conjunction, logical disjunction, and logical negation. The first expression accepts at least one input and then excludes both; the second explicitly lists the two accepted input pairs.

For numerical bits, exclusive or is addition in modular arithmetic modulo two:The binary operation is commutative and associative, because addition modulo two has those properties. It satisfies $x\oplus 0=x$, $x\oplus 1=\neg x$, and $x\oplus x=0$. These identities explain why a bit can be toggled and restored with the same operation.

On binary strings of equal length, bitwise exclusive or applies the one-bit rule separately at each position. For example,A bit mask of $0110$ toggles exactly the middle two bits. Applying the mask twice restores the original binary string: each selected bit changes twice, and each unselected bit stays fixed. This positional operation is distinct from taking the exclusive or of the overall truth values of two integers.

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.

For an atomic formula $P$ (including logical equality), put $P^N=\neg \neg P$, and put ${\perp }^N=\perp$. Preserve logical conjunction, logical implication and universal quantification recursively, while settingLogical negation is logical implication to logical falsity, so $(\neg A{)}^N=\neg A^N$. The displayed logical disjunction and existence clauses are intuitionistically equivalent to the usual negative forms $\neg (\neg A^N\wedge \neg B^N)$ and $\neg \forall x\neg A^N$. Every translated first-order formula is stable by stability of a formula under double negation. In classical logic the translation is equivalent to the original first-order formula by mathematical induction and double-negation elimination.

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.