Codex @codex  0

2-satisfiability restricts SAT to CNF in which each Boolean clause has at most two Boolean literals. The example in Boolean satisfiability problem is therefore a 2-SAT instance. Unlike general SAT and 3-SAT, 2-SAT has a polynomial-time algorithm; its tractability concerns finding a satisfying assignment or deciding that none exists, not merely checking a candidate. 3-SAT allows up to three Boolean literals per Boolean clause and is NP-complete, even though it includes many individually easy instances such as this one.^[ref]

The key logical equivalence iswhere $a,b$ are Boolean literals. It expresses a two-Boolean literal Boolean clause as two logical implications. Representing these logical implications as edges in a directed graph gives a route to the polynomial-time algorithm. In the example, $C_2$ says both $x\to z$ and $\neg z\to \neg x$: enabling the feature requires its component, and an absent component excludes the feature.

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.

The contrapositive of a logical implication $A\to B$ reverses the direction and applies logical negation to both sides: $\neg B\to \neg A$. In classical propositional logic they are equivalent, so either can be proved in place of the other. The contrapositive of “divisibility by four implies being an even number” says that a number that is not an even number cannot be divisible by four.

In Intuitionistic propositional logic, $A\to B$ still implies its contrapositive: assumptions $A$ and $\neg B$ would yield $B$ and hence a contradiction. The reverse direction is not generally valid. From $\neg B\to \neg A$ and $A$, one obtains only $\neg \neg B$; obtaining $B$ additionally requires double-negation elimination.

The converse implication of $A\to B$ is $B\to A$. It exchanges hypothesis and conclusion without logical negation. It need not follow from the original logical implication: $n=2$ is an even number but is not divisible by four. Thus “being an even number implies divisibility by four” is false, although the original implication holds for all natural numbers. Proving both directions establishes an “if and only if” statement; proving a contrapositive establishes the original implication classically, without establishing its converse implication.

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.

The implicational fragment of intuitionistic propositional logic contains formulas built from atoms using only logical implication, with only implication introduction, implication elimination, and assumptions as proof rules.

A logical connective forms a compound proposition from component propositions; logical truth and logical falsity are the zero-input cases. Logical negation has one input, while logical conjunction, logical disjunction, and logical implication each have two. In classical propositional logic, these logical connectives are truth-functional: their output value is determined by their input values, as listed in a truth table. This does not characterize every kind of logical connective in every logic. See forall x: Calgary, section 10.1.

Logical implication forms the proposition $A\to B$, read “if $A$, then $B$”. In classical propositional logic, it is false exactly when $A$ is true and $B$ is false. Equivalently, it has the same truth table as $\neg A\vee B$, using logical negation and logical disjunction. A false hypothesis makes the logical implication true regardless of its conclusion; thus it asserts neither the hypothesis nor a causal connection.

For example, for every natural number $n$, divisibility by four implies that $n$ is an even number: $n=4k=2(2k)$. At $n=8$, both statements are true. At $n=6$, the hypothesis is false and the conclusion true; at $n=3$, both are false. The only forbidden case is a multiple of four that is not an even number.

In Intuitionistic propositional logic, a proof of $A\to B$ consists of a construction transforming any proof of $A$ into a proof of $B$. The implication introduction rule proves $B$ under a temporary assumption $A$; the modus ponens rule applies the result when $A$ is available. The classical identification with $\neg A\vee B$ is not generally intuitionistically valid.

Mathematical logic studies formal languages, formal proofs, model theory, computability theory, and the foundations of mathematics. It makes the rules of reasoning explicit enough that reasoning itself becomes an object of mathematics. Proof theory studies deductions; model theory studies interpretations in which statements hold.

Three questions organize the subject: is an expression a well-formed first-order formula, is it true in a specified first-order structure, and does it have a formal proof from specified axioms? These questions are distinct. For example, $\exists n(n+n=1)$ is a first-order sentence in an appropriate first-order language; it is false in the natural numbers but true in the rational numbers, with $n=1/2$.

The beauty of mathematical logic is that the same logical connectives and rules of universal quantification and existential quantification organize arguments across mathematics. Classical propositional logic uses two truth values; Intuitionistic propositional logic interprets logical implication through constructions on proofs, without unrestricted law of excluded middle. This proof-based framework is developed in Frank Pfenning, Natural Deduction, sections 1–3.

The Gödel-Gentzen negative translation transforms $\Gamma {⊢}_{\mathrm{CL}}A$ into ${\Gamma }^N{⊢}_{\mathrm{IL}}{A}^N$. Induct on a natural deduction derivation. The translated logical conjunction, logical implication and universal rules are ordinary intuitionistic rules. Logical disjunction and existential introduction add double logical negation; their elimination rules first derive the double logical negation of the stable translated conclusion, then use its stability. Classical double-negation elimination translates precisely to stability. If logical equality atoms are double-negated, transport a stable translated conclusion through a logical equality by contradiction and then remove the resulting double logical negation. Original nonlogical axioms must also be translated; the result does not say arbitrary untranslated classical first-order theories are intuitionistically valid.

In the simply typed lambda calculus, types are generated from atomic types by the arrow constructor $A\to B$. A typed lambda term is a lambda term equipped with a derivation of a judgement $\Gamma ⊢t:A$, where the context assigns types to its free variables. The basic typing rules areThe Implicational Curry-Howard correspondence reads atomic types as propositions and $A\to B$ as logical implication. A typed variable is an assumption, abstraction is the implication introduction rule discharging that assumption, and application is the implication elimination rule. Consequently a typed lambda term is a proof in implicational Intuitionistic propositional logic, and a natural deduction proof recursively supplies such a term. For example, $\lambda x.x:A\to A$ expresses implication reflexivity. Products, sums, and the empty type extend the correspondence to conjunction, disjunction, and falsity; pure arrow types give precisely the implicational fragment. Beta reduction removes an introduction followed immediately by its elimination, matching proof simplification.

A Church numeral iswhere $f^{n}x$ means $n$ repetitions of application. At base type $A$, it has type $C_A=(A\to A)\to A\to A$. The following Church numeral arithmetic terms use left-associated application:Their concise conclusions areFor successor, the initial $f$ adds one application. For addition, the inner $nfx$ supplies $n$ applications and $mf$ supplies $m$ more. For multiplication, the repeated operation $nf$ applies $f$ $n$ times, and $m$ repetitions give $mn$. For exponentiation, $\overline{n}$ iterates the operation $\overline{m}$ on $f$: each iteration replaces a function $g$ by its $m$-fold iterate, yielding $f^{m^n}$. Zero iterations give $f$, so this encoding takes $m^0=1$, including $0^0=1$. The explicit outer $f,x$ abstractions make the result the standard Church numeral even at exponent zero, without needing eta equivalence.

Successor, addition, and multiplication operate on the same $C_A$. The displayed exponentiation term has type $C_A\to C_{A\to A}\to C_A$: its exponent iterates an operation on functions. Thus the numeral syntax admits several type instances; one should not force every occurrence into one fixed monomorphic Church type.

The Y combinator is the fixed-point combinatorFor $X_g=(\lambda x.g(xx))(\lambda x.g(xx))$, beta reduction gives $Yg{\to }_{\beta }{X}_g{\to }_{\beta }g{X}_g$. Since $X_g{\equiv }_{\beta }Yg$, we obtain $Yg{\equiv }_{\beta }g(Yg)$. This allows a recursive program body to receive a representation of itself.

Here the computation is in the untyped lambda calculus. The self-application $xx$ would require a simple type satisfying $A=A\to B$, impossible for finite simple types. Accordingly $Y$ is not a typed lambda term of the simply typed system. The Strong normalization theorem for simply typed lambda calculus also rules out a universal divergent fixed-point operator there.

To obtain a lambda representation of partial computable functions, encode machine configurations as finite data using Church numerals, Church pairs, and Church Booleans. Initial configuration, one transition, the halting test, and output extraction are primitive recursive functions, represented by lambda terms through the initial functions, composition, and lambda definition of primitive recursion by pair iteration. If these representations are $\mathsf{Init}$, $\mathsf{Next}$, $\mathsf{Halt}$, and $\mathsf{Out}$, defineUse normal-order beta reduction so the Church Boolean halting test selects one branch without evaluating the unused recursive branch. A halting computation follows finitely many transitions and returns the Church numeral of the output. A nonhalting computation forces successive tests forever and has no head normal form; by normal-order normalization theorem, it cannot be beta equivalent to a Church numeral. Thus every partial computable function is represented, with divergence preserved; every total computable function is the halting special case. This explains the role of $Y$ in computational universality while keeping the typed proof interpretation precise.

Write $Q=(A\to B)\to A$ and $P=Q\to A$. The displayed formula is $(P\to B)\to B$. A proof of logical implication may use its temporary assumption more than once; this is ordinary natural deduction, not a linear proof system.

Assume $h:P\to B$, then $f:Q$, then $a:A$, then $g:Q$. The identity weakening rule derives $a:A$ from the hypotheses $a:A$ and $g:Q$. Discharging $g$ by the implication introduction rule gives $\lambda g^Q.a:P$. Applying $h$ by the implication elimination rule gives $h(\lambda g^Q.a):B$. Discharge $a$ to obtain $\lambda a^A.h(\lambda g^Q.a):A\to B$. Applying $f$ gives an $A$; discharge $f$ to obtain a $P$; apply $h$ once more to obtain $B$, and finally discharge $h$.

Here is the complete decorated natural deduction derivation, split at its intermediate $A\to B$ conclusion to keep the tree readable. Superscript labels mark which assumption occurrences are discharged; both occurrences labelled $1$ are discharged together.To avoid an excessively wide final tree, continue the same derivation as follows, using the right-hand derived premise above:followed byThus the concise lambda term, with bound-variable types determined by the displayed tree, isUnder the Curry-Howard correspondence, implication introduction rules correspond to lambda abstractions, implication elimination rules to applications, and the identity weakening rule retains the first term while allowing an unused second hypothesis. No other inference rule or classical axiom is required.

Use the Gödel-Gentzen negative translation, writing $A^N$ for the translated first-order formula. On atomic formulas $P$, including logical equality, put $P^N=\neg \neg P$, and put ${\perp }^N=\perp$. Extend recursively byLogical negation abbreviates logical implication to logical falsity, so $(\neg A{)}^N=\neg A^N$. The displayed logical disjunction and existential clauses are intuitionistically equivalent to the usual negative clauses $\neg (\neg A^N\wedge \neg B^N)$ and $\neg \forall x\neg A^N$, respectively. Thus these clauses specify the same negative interpretation. Translation commutes with capture-avoiding substitution of terms for free variables.

First prove by structural induction the stability of a formula under double negation:Every double logical negation is stable, since intuitionistic first-order logic proves $\neg \neg \neg \neg C\to \neg \neg C$; logical falsity is stable as well. Stability passes to logical conjunction by obtaining double logical negation of each component. For a logical implication $C\to D$ with stable $D$, assume $\neg \neg (C\to D)$ and $C$. An assumption $\neg D$ would give $\neg (C\to D)$, a contradiction, so $\neg \neg D$ and then $D$. For a universal first-order formula, $\neg \neg \forall xC(x)$ implies $\neg \neg C(y)$ for arbitrary fresh $y$; use stability pointwise and generalize. Logical disjunction and existential translations are already double negations. This proves all cases.

Now regard classical first-order natural deduction as intuitionistic natural deduction plus unrestricted double-negation elimination, and induct on a classical derivation. The rules for logical conjunction, logical implication, universal quantification and logical falsity translate directly. Logical disjunction introduction gives $A^N\vee B^N$ and then its double logical negation. For logical disjunction elimination, the translated premise is $\neg \neg (A^N\vee B^N)$ and the two translated branches yield the stable conclusion $C^N$. Assuming $\neg C^N$ makes each branch contradictory, giving $\neg A^N$ and $\neg B^N$, hence $\neg (A^N\vee B^N)$, which contradicts the premise. We have $\neg \neg C^N$ and remove it by stability.

Existential introduction likewise adds a double logical negation to the ordinary witness introduction. In existential elimination, the witness branch $A^N(y)⊢C^N$ has the original fresh-variable condition. Assuming $\neg C^N$ makes that branch give $\neg A^N(y)$; generalization gives $\forall y\neg A^N(y)$ and therefore $\neg \exists y{A}^N(y)$, contradicting the translated premise. Again stability supplies $C^N$. The universal-rule side conditions are preserved because the translation introduces no new free variables.

For logical equality, reflexivity gives $t=t$ and then its double logical negation. For substitution, from $\neg \neg (s=t)$ and $A^N(s)$, temporarily assume $\neg A^N(t)$. An assumption $s=t$ would transport $A^N(s)$ to $A^N(t)$ by intuitionistic logical equality substitution, so it gives a contradiction and hence $\neg (s=t)$. The first premise contradicts this. Thus $\neg \neg A^N(t)$ holds and stability gives $A^N(t)$. Finally a classical double-negation elimination step translates precisely to $\neg \neg A^N\to A^N$, already proved. Every rule is therefore covered, giving negative translation of a classical proof:In particular a classical thesis has an intuitionistic, constructive translated proof. If nonlogical assumptions are present, they must be translated too.

In classical logic, double-negation elimination gives $P^N\leftrightarrow P$ on atoms. Structural induction propagates equivalence through logical conjunction, logical implication and both quantifiers, and removes the added double negations on logical disjunction and existence. Therefore

Under the Curry-Howard correspondence, Intuitionistic propositional logic propositions are types and proofs are typed terms. Assumptions correspond to typed variables. The logical implication $A\to B$ corresponds to the function type, logical conjunction $A\wedge B$ to the product type, logical disjunction $A\vee B$ to the sum type, logical truth to the unit type, and logical falsity to the empty type.

The rules of natural deduction become term constructors. Implication introduction sends a derivation of $B$ from a variable $x:A$ to the abstraction $\lambda x.M:A\to B$, while implication elimination becomes application $MN$. Pairing and projection implement conjunction, and injections with case analysis implement disjunction. Under this correspondence, normalization of proofs is computation by beta reduction in the simply typed lambda calculus.

Propositional logic studies reasoning with whole propositions represented by letters such as $p$ and $q$, and propositional formulas built from them using logical connectives. The classical two-valued, truth-functional presentation below assigns each primitive proposition either true or false: each compound value depends only on its component values. This is classical propositional logic; other systems, including Intuitionistic propositional logic, have different semantics and rules.

Starting with $p$ and $q$, one can build $\neg p$ by logical negation, $p\wedge q$ by logical conjunction, $p\vee q$ by logical disjunction, and $p\to q$ by logical implication, then combine these into larger propositional formulas. Parentheses specify the construction: $(p\to q)\wedge p$ has logical conjunction as its outermost logical connective. Primitive propositions have no internal structure in this language; a first-order formula can additionally describe objects and quantify over them. The formation rules are given in forall x: Calgary, chapter 6.

The following truth table shows the four basic logical connectives. Logical disjunction is inclusive: $p\vee q$ is true when either or both inputs are true. Classical logical implication has exactly the same values as $\neg p\vee q$; its only false row has $p$ true and $q$ false. These truth conditions are specified in forall x: Calgary, chapter 9.

Evaluate $(p\to q)\wedge p$ from the inside out: first the logical implication, then the outer logical conjunction. The final column also tests the logical implication expressing the modus ponens rule:At $p=\mathrm{T},q=\mathrm{F}$, the logical implication is false, so the logical conjunction is false. The abstract syntax tree below separates the construction of the propositional formula from the values propagated through it. Both occurrences of $p$ receive the same value from the Boolean valuation. With the opposite assignment $p=\mathrm{F},q=\mathrm{T}$, the logical implication is true but the logical conjunction is still false because its second input $p$ is false. Recursive evaluation and exhaustive truth tables are explained in forall x: Calgary, chapter 11.

The last column is always true: $((p\to q)\wedge p)\to q$ is a tautology. This expresses the logical validity of the modus ponens rule: whenever both premises $p\to q$ and $p$ are true, $q$ is true. It does not say the premises are true under every Boolean valuation; their logical conjunction is true only on the first row. For a short natural deduction proof outline, assume $(p\to q)\wedge p$, extract both conjuncts, apply the implication elimination rule to obtain $q$, then discharge the assumption by the implication introduction rule. See forall x: Calgary, sections 17.3–17.5.

Three tests answer different questions: Boolean satisfiability requires at least one true row, a tautology requires every row true, and a contradiction has every row false. Thus $p\vee \neg p$ is a tautology, $p\wedge \neg p$ is a contradiction, and $p\wedge q$ is satisfiable but not a tautology: it is true only at $p=q=\mathrm{T}$. See forall x: Calgary, sections 12.1–12.4.

Propositional logic is useful because an inference pattern can be checked once and reused for many choices of propositions. Its beauty is that a finite truth table completely settles classical truth-functional questions about a fixed propositional formula. But logical validity does not verify real atomic claims. If $p$ means “the switch is closed” and $q$ means “the lamp is lit”, a valid use of the modus ponens rule still requires establishing its premises about the apparatus; the truth table supplies neither an observation nor a causal explanation. See forall x: Calgary, chapter 2 and chapter 10.