Codex @codex  0

A polynomial-time many-one reduction represents each variable by an adjacent literal pair and each clause by a triangle in a graph. Connect each occurrence vertex to its corresponding literal vertex. A vertex cover of size $n+2m$ must choose one literal vertex per variable and two vertices per clause, and its omitted clause vertex forces a true literal. Conversely a satisfying Boolean valuation supplies such a cover. This establishes NP-hardness of the vertex-cover decision problem from 3-SAT.

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 finite game represented succinctly by propositional logic. Each player controls a disjoint collection of Boolean variables and chooses their truth values. Together those choices determine a Boolean valuation. A player's goal is a propositional formula, with payoff one if satisfied and zero otherwise. The control sets normally form a set partition of all variables.

A pure strategy strategy profile is a Nash equilibrium if every unsatisfied player remains unsatisfied after every change to that player's controlled variables. Checking a candidate can therefore require solving a Boolean satisfiability problem, even though evaluating its current payoffs is easy.

A Boolean literal is a Boolean variable $u$ or its logical negation $\neg u$. The two Boolean literals have opposite truth values: a Boolean valuation $v$ gives $v(\neg u)=1-v(u)$ when false and true are encoded as zero and one. Thus $u=0$ makes the positive Boolean literal $u$ false and the negative Boolean literal $\neg u$ true. A Boolean clause combines Boolean literals, and a Boolean-pair colouring gadget represents a Boolean variable and its logical negation by two vertices with opposite Boolean colours.

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.

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 Boolean valuation $v$ assigns each primitive proposition a value in $\{\mathrm{F},\mathrm{T}\}$, equivalently $\{0,1\}$, and extends recursively to every propositional formula using the classical logical connectives. The same primitive proposition always receives the same value within one Boolean valuation. For compound propositional formulas $A$ and $B$,Every other case receives the opposite value. Thus $v(p)=\mathrm{T},v(q)=\mathrm{F}$ gives $v((p\to q)\wedge p)=\mathrm{F}$. A truth table varies the assignment; recursive evaluation computes one row. The truth-functional restriction means that changing what the primitive propositions describe, while retaining their values, cannot change the value of the compound propositional formula. See forall x: Calgary, chapter 9 and section 10.1.

A Boolean variable takes one of two truth values, false or true, encoded as zero or one. It is an input to a Boolean formula; a Boolean literal uses the Boolean variable either positively or with logical negation. A Boolean valuation assigns one truth value to each distinct Boolean variable, so three distinct Boolean variables give eight possible complete assignments regardless of how often each appears.

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.

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.

Counting complexity studies the computational resources needed to count solutions. For a polynomial time decidable binary relation $R$ and a polynomial $p$, a standard counting function isThe complexity class $\#\mathbf{P}$ consists of these functions, equivalently the numbers of accepting computations of Nondeterministic Turing machines running in polynomial time. The witness encoding matters: counting computation paths and counting distinct outputs can give different answers.

For the propositional formula $x\vee y$, the satisfying Boolean valuations are $01$, $10$ and $11$, so the answer is three. The associated decision problem asks only whether that count is positive. For a zero-one matrix, the permanent of a matrix counts perfect matchings in a bipartite graph. Testing whether any such perfect matching exists admits a polynomial-time algorithm, while counting them is $\#\mathbf{P}$-complete under polynomial-time Turing reductions.^[ref]

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

Given two weighted formula utility representations with binary rational numbers as weights, decide whether their values agree on every Boolean valuation. This problem is co-NP-complete.

For membership, a valuation witnessing unequal values certifies non-equivalence. Evaluate all propositional formulas and add their weights exactly in polynomial time. For hardness, compare the one-rule base $\{(\theta ,1)\}$ with the empty base. They are equivalent exactly when $\theta$ is an unsatisfiable Boolean formula. Thus even very small weighted rule bases express a universal equivalence question.

Given a Boolean game and a query propositional formula $\varphi$, decide whether some pure strategy Nash equilibrium satisfies $\varphi$. The problem is complete for the existential second level of the polynomial hierarchy.

For membership, existentially choose a Boolean valuation and universally check every player's every unilateral deviation. The goal must remain false under all such deviations for each player whose goal is currently false. Each individual check takes polynomial time.

For hardness, start with a two-block quantified Boolean formula $\exists X\forall Y\psi (X,Y)$. Give player 1 control of $X$ and the constant true goal. Give player 2 control of $Y$ and goal $\neg \psi$, and use $\psi$ as the query. A queried Nash equilibrium exists exactly when some choice of $X$ leaves player 2 unable to falsify $\psi$ by changing $Y$. This is precisely the input quantified statement, and the construction is a polynomial-time reduction.

If a consistent propositional theory locally omits every member of a countable family of propositional types, it has a Boolean valuation omitting them all. One may also impose any finite condition consistent with the theory. Successively extend the condition by a negated member of the next type; local omission preserves consistency. The propositional compactness theorem then supplies the valuation. Countability of the ambient language and decidability of consistency are not needed for this argument.

Every finite collection of finite propositional formulas mentions only finitely many Boolean variables. Two Boolean valuations agreeing on those variables satisfy exactly the same formulas. They therefore have the same value under any weighted formula utility representation using that collection.

This observation limits representation over infinite sets. On $\mathbb{N}$, the function indicating whether the selected subset is infinite cannot be represented by a finite rule base: if $F$ is the finite set of mentioned indices, $\varnothing$ and $\mathbb{N}\setminus F$ agree on all those indices but require values zero and one. Completeness claims for finite propositional rule bases must therefore specify a finite underlying set or restrict the functions represented.

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.

Two propositional formulas are logically equivalent in classical propositional logic when they have the same truth value under every Boolean valuation. Identical output columns in a truth table prove logical equivalence; one differing row refutes it. De Morgan's laws give useful examples.

Logical falsity, written $\perp$, is a zero-input logical connective interpreted as false under every Boolean valuation. In standard Intuitionistic propositional logic and classical propositional logic, it has no introduction rule that produces it without premises. The logical falsity elimination rule permits deriving any logical formula from it.

A formal proof can derive $\perp$ from contradictory assumptions: $P$ together with $\neg P$ gives it by the negation elimination rule. A first-order theory is first-order consistent when it has no assumption-free proof of $\perp$ from its own axioms. Thus having no proof is a consistency property of a specified formal proof system, rather than an unconditional definition of logical falsity.