Helpful context:

Logic has two layers that must be kept separate but must ultimately agree. The semantic layer asks: given truth values for atomic propositions, is a formula true? It works by evaluating formulas against truth assignments - the machinery of truth tables. The syntactic layer asks something entirely different: can a formula be derived from given premises using rules of inference, without knowing any truth values? These two questions feel like they are about different things. The soundness theorem says that if you can derive $\phi$ syntactically, then $\phi$ is semantically true. The completeness theorem (Gödel, 1930) says the converse: if $\phi$ is semantically true in all interpretations, then it can be derived syntactically. Together, syntactic derivability and semantic truth are equivalent.

This equivalence is not obvious. Semantic truth is a statement about all possible truth assignments - an infinite object, or at least an exponentially large one. Syntactic derivability is a finite, mechanical process: a sequence of symbol manipulations that a computer could check step by step. The fact that these two descriptions pick out exactly the same set of formulas (the tautologies) is a deep theorem. It means the inference rules are not just plausible-seeming manipulations. They are a complete characterization of truth.

This post builds both layers and connects them. Propositions, connectives, and truth tables come first - this is the semantic layer. Then well-formed formulae, tautologies, equivalence laws, and normal forms, which bridge syntax and semantics. Then inference: rules of proof and the Conditional Proof technique, which is the syntactic layer. The two halves of the post are not two different subjects. They are two ways of looking at the same thing - and the fact that they agree is what makes propositional logic a coherent foundation for formal reasoning.

Propositions and Connectives

A proposition is a declarative statement that has a definite truth value - it is either true (T, or 1) or false (F, or 0). “Seven is a prime number” is a proposition (it is true). “It is raining” is a proposition (true or false depending on fact). “What time is it?” is not a proposition - questions have no truth value. “This statement is false” is famously not a proposition either, since assuming it has a truth value leads to a contradiction.

Propositions are combined using logical connectives to form compound statements. The five standard connectives, along with their symbols and their truth-table definitions:

Negation $\neg p$ (“not $p$"): flips the truth value.

$$\begin{array}{c|c} p & \neg p \\ \hline \text{T} & \text{F} \\ \text{F} & \text{T} \end{array}$$

Conjunction $p \wedge q$ ("$p$ and $q$"): true only when both are true.

$$\begin{array}{cc|c} p & q & p \wedge q \\ \hline \text{T} & \text{T} & \text{T} \\ \text{T} & \text{F} & \text{F} \\ \text{F} & \text{T} & \text{F} \\ \text{F} & \text{F} & \text{F} \end{array}$$

Disjunction $p \vee q$ ("$p$ or $q$"): true when at least one is true (inclusive or).

$$\begin{array}{cc|c} p & q & p \vee q \\ \hline \text{T} & \text{T} & \text{T} \\ \text{T} & \text{F} & \text{T} \\ \text{F} & \text{T} & \text{T} \\ \text{F} & \text{F} & \text{F} \end{array}$$

Implication $p \to q$ (“if $p$ then $q$”, or “$p$ implies $q$"): false only when the hypothesis $p$ is true and the conclusion $q$ is false. When $p$ is false the implication is vacuously true regardless of $q$.

$$\begin{array}{cc|c} p & q & p \to q \\ \hline \text{T} & \text{T} & \text{T} \\ \text{T} & \text{F} & \text{F} \\ \text{F} & \text{T} & \text{T} \\ \text{F} & \text{F} & \text{T} \end{array}$$

Biconditional $p \leftrightarrow q$ ("$p$ if and only if $q$"): true when $p$ and $q$ have the same truth value.

$$\begin{array}{cc|c} p & q & p \leftrightarrow q \\ \hline \text{T} & \text{T} & \text{T} \\ \text{T} & \text{F} & \text{F} \\ \text{F} & \text{T} & \text{F} \\ \text{F} & \text{F} & \text{T} \end{array}$$

The vacuous truth of $p \to q$ when $p$ is false is the single most commonly confused aspect of propositional logic. Intuitively: a promise “if it rains I will carry an umbrella” is not broken when it does not rain. You only break the promise (the implication is false) by having it rain and leaving the umbrella at home.

Precedence and Associativity

Without parentheses, the order of operations follows a binding hierarchy (tightest to loosest):

$$\neg ;;\text{then};; \wedge ;;\text{then};; \vee ;;\text{then};; \to ;;\text{then};; \leftrightarrow$$

So $\neg p \wedge q \vee r \to s \leftrightarrow t$ parses as $(((\neg p) \wedge q) \vee r) \to s) \leftrightarrow t$. Negation binds tightest: $\neg p \wedge q$ means $(\neg p) \wedge q$, not $\neg(p \wedge q)$. Implication is right-associative: $p \to q \to r$ means $p \to (q \to r)$, which is different from $(p \to q) \to r$. All other connectives are associative in the sense that the choice of grouping does not matter for truth value, but implication is not associative in general - always parenthesize carefully.

Well-Formed Formulae

Not every string of symbols is a legitimate logical formula. A well-formed formula (WFF) is defined recursively:

  1. Every atomic proposition (a propositional variable like $p, q, r$) is a WFF.
  2. If $A$ is a WFF then $\neg A$ is a WFF.
  3. If $A$ and $B$ are WFFs then $(A \wedge B)$, $(A \vee B)$, $(A \to B)$, and $(A \leftrightarrow B)$ are WFFs.
  4. Nothing else is a WFF.

The parentheses in rules 3 are strict - in the fully parenthesized grammar, every binary connective application is wrapped. In practice we drop outer parentheses and apply the precedence rules above, but the recursive definition is the formal foundation.

Parse Trees

Every WFF has a unique parse tree whose leaves are atomic propositions and whose internal nodes are connectives. The parse tree makes the structure explicit and eliminates any ambiguity about the order of operations.

For the formula $(p \to q) \wedge (\neg q \to \neg p)$:

        ∧
       / \
      →    →
     / \  / \
    p   q ¬q  ¬p
          |    |
          q    p

The root is $\wedge$, its left child is $p \to q$, its right child is $\neg q \to \neg p$. Each leaf is an atomic variable; each internal node is a connective. Reading the tree from leaves to root gives the order in which sub-formulae are evaluated. The height of the tree is the nesting depth of the formula.

The recursive definition of WFF and the parse tree together guarantee that every WFF can be evaluated in a bottom-up pass: assign truth values to leaves, evaluate each internal node by the connective’s truth table, and the root gives the truth value of the whole formula.

Tautology, Contradiction, Contingency

A truth assignment is a function $v$ mapping each propositional variable to T or F. A formula $A$ with $n$ distinct variables has $2^n$ truth assignments; a truth table lists them all.

A formula $A$ is:

  • A tautology if $v(A) = \text{T}$ for every truth assignment $v$.
  • A contradiction (or unsatisfiable formula) if $v(A) = \text{F}$ for every truth assignment $v$.
  • A contingency if it is neither a tautology nor a contradiction - it is true under some assignments and false under others.

The standard examples:

$p \vee \neg p$ is a tautology (the Law of Excluded Middle): $$\begin{array}{c|c|c} p & \neg p & p \vee \neg p \\ \hline \text{T} & \text{F} & \text{T} \\ \text{F} & \text{T} & \text{T} \end{array}$$

$p \wedge \neg p$ is a contradiction: $$\begin{array}{c|c|c} p & \neg p & p \wedge \neg p \\ \hline \text{T} & \text{F} & \text{F} \\ \text{F} & \text{T} & \text{F} \end{array}$$

$p \to q$ is a contingency - it is true when $p = \text{F}$ or $q = \text{T}$, and false when $p = \text{T}$ and $q = \text{F}$.

To check whether a formula is a tautology, build its truth table and verify all output entries are T. For $n$ variables this requires $2^n$ rows. For small $n$ this is feasible; for large formulas it is the co-NP-hard problem of tautology checking, and heuristics (SAT solvers, resolution, BDD packages) are used instead.

Functionally Complete Sets

A set of connectives $S$ is functionally complete if every Boolean function $f: \{0,1\}^n \to \{0,1\}$ can be expressed as a formula using only connectives from $S$. Since every Boolean function has a DNF representation (a disjunction of conjunctions), and DNF uses only $\neg$, $\wedge$, and $\vee$, the set $\{\neg, \wedge, \vee\}$ is trivially functionally complete. But we can do better.

$\{\neg, \wedge\}$ is functionally complete. We can derive $\vee$ from negation and conjunction using De Morgan’s law: $$p \vee q ;\equiv; \neg(\neg p \wedge \neg q)$$ Since $\vee$ is expressible from $\{\neg, \wedge\}$, and since $\{\neg, \wedge, \vee\}$ is complete, $\{\neg, \wedge\}$ is complete. We can also express implication and biconditional: $$p \to q ;\equiv; \neg p \vee q ;\equiv; \neg(p \wedge \neg q)$$ $$p \leftrightarrow q ;\equiv; (p \to q) \wedge (q \to p) ;\equiv; \neg(p \wedge \neg q) \wedge \neg(q \wedge \neg p)$$

$\{\neg, \vee\}$ is functionally complete. Similarly, we derive $\wedge$ via De Morgan: $p \wedge q \equiv \neg(\neg p \vee \neg q)$.

NAND ($\uparrow$) alone is functionally complete. The NAND connective is defined by $p \uparrow q \equiv \neg(p \wedge q)$, with truth table:

$$\begin{array}{cc|c} p & q & p \uparrow q \\ \hline \text{T} & \text{T} & \text{F} \\ \text{T} & \text{F} & \text{T} \\ \text{F} & \text{T} & \text{T} \\ \text{F} & \text{F} & \text{T} \end{array}$$

From NAND alone we can derive negation and conjunction, which gives a functionally complete set: $$\neg p ;\equiv; p \uparrow p$$ $$p \wedge q ;\equiv; \neg(p \uparrow q) ;\equiv; (p \uparrow q) \uparrow (p \uparrow q)$$

For negation: $p \uparrow p = \neg(p \wedge p) = \neg p$. For conjunction: once we have negation from NAND, $p \wedge q = \neg(p \uparrow q) = (p \uparrow q) \uparrow (p \uparrow q)$. Disjunction follows: $p \vee q = \neg p \uparrow \neg q = (p \uparrow p) \uparrow (q \uparrow q)$. Since $\{\neg, \wedge\}$ is complete and both are expressible by NAND, NAND alone is complete.

NOR ($\downarrow$) alone is functionally complete. The NOR connective is defined by $p \downarrow q \equiv \neg(p \vee q)$. By symmetry with NAND: $$\neg p ;\equiv; p \downarrow p$$ $$p \vee q ;\equiv; (p \downarrow q) \downarrow (p \downarrow q)$$ $$p \wedge q ;\equiv; (p \downarrow p) \downarrow (q \downarrow q) ;\equiv; \neg p \downarrow \neg q$$

Since $\{\neg, \vee\}$ is complete and both are expressible by NOR, NOR alone is complete. In hardware, NAND gates and NOR gates are the fundamental building blocks of digital circuits precisely because of this property - any Boolean circuit can be implemented using only one type of gate.

Sets that are not functionally complete include $\{\wedge, \vee\}$ (cannot express negation; every formula in these connectives is monotone, meaning flipping a variable from F to T can never change the output from T to F), and $\{\to\}$ alone (the tautology $p \to p$ is expressible but no contradiction is, since $p \to q$ with $p = \text{T}$ and $q = \text{T}$ is true but cannot force false output in all cases).

Logical Equivalence

Two formulae $A$ and $B$ are logically equivalent, written $A \equiv B$, if and only if $A \leftrightarrow B$ is a tautology - that is, if $v(A) = v(B)$ for every truth assignment $v$. Equivalence is checked by building the full truth table for both formulae and confirming they agree on every row.

The fundamental equivalences form the algebraic laws of propositional logic:

Double negation: $$\neg \neg A \equiv A$$

De Morgan’s laws: $$\neg(A \wedge B) \equiv \neg A \vee \neg B$$ $$\neg(A \vee B) \equiv \neg A \wedge \neg B$$

Commutativity: $$A \wedge B \equiv B \wedge A \qquad A \vee B \equiv B \vee A$$

Associativity: $$(A \wedge B) \wedge C \equiv A \wedge (B \wedge C) \qquad (A \vee B) \vee C \equiv A \vee (B \vee C)$$

Distributivity: $$A \wedge (B \vee C) \equiv (A \wedge B) \vee (A \wedge C)$$ $$A \vee (B \wedge C) \equiv (A \vee B) \wedge (A \vee C)$$

Absorption: $$A \wedge (A \vee B) \equiv A \qquad A \vee (A \wedge B) \equiv A$$

Idempotence: $$A \wedge A \equiv A \qquad A \vee A \equiv A$$

Identity: $$A \wedge \text{T} \equiv A \qquad A \vee \text{F} \equiv A$$

Annihilation: $$A \wedge \text{F} \equiv \text{F} \qquad A \vee \text{T} \equiv \text{T}$$

Implication elimination: $$A \to B \equiv \neg A \vee B$$

Contrapositive: $$A \to B \equiv \neg B \to \neg A$$

Biconditional elimination: $$A \leftrightarrow B \equiv (A \to B) \wedge (B \to A) \equiv (\neg A \vee B) \wedge (\neg B \vee A)$$

Exportation: $$(A \wedge B) \to C \equiv A \to (B \to C)$$

These equivalences are not independent - many can be derived from others. But the list above is the practical toolkit for simplifying formulae and recognizing logical structure. De Morgan’s laws and implication elimination are the most frequently used in transforming formulae to normal form.

Substitution, Replacement, and Duality

Two fundamental meta-theorems govern how we can manipulate tautologies and equivalences.

Substitution principle: If $A$ is a tautology and $p$ is any propositional variable in $A$, then replacing every occurrence of $p$ in $A$ by any formula $B$ yields a new formula $A'$ that is also a tautology. The key requirement is that all occurrences of $p$ are replaced uniformly - if $p$ appears three times, all three must be replaced by the same $B$.

For example, $p \vee \neg p$ is a tautology. Substituting $p$ with $(q \to r)$ gives $(q \to r) \vee \neg(q \to r)$, which is again a tautology. This is useful because it lets us generate infinite families of tautologies from known ones.

Replacement rule: If $A \equiv B$ (they are logically equivalent), then in any formula $C$, replacing any occurrence of $A$ as a subformula by $B$ gives a formula $C'$ such that $C \equiv C'$. Unlike substitution (which requires uniform replacement of variables across the whole formula), replacement applies to a specific subformula in a specific location. This is the formal justification for simplification steps like “replace $\neg \neg p$ by $p$ in the third conjunct”.

Duality principle: The dual of a formula $A$, written $A^d$, is obtained by swapping every $\wedge$ with $\vee$ and every $\vee$ with $\wedge$, and swapping every T with F and every F with T (propositional variables and their negations are left alone). The duality theorem states:

$$\neg A(p_1, \ldots, p_n) \equiv A^d(\neg p_1, \ldots, \neg p_n)$$

A direct consequence: if $A \equiv B$ then $A^d \equiv B^d$. And if $A$ is a tautology, then $\neg A^d$ is also a tautology (equivalently, $A^d$ is a contradiction) - because $A$ is true everywhere means its dual, with all variables negated, covers the dual truth conditions. This is precisely the relationship between the two De Morgan laws: one is the dual of the other.

Normal Forms

Every propositional formula can be rewritten into a canonical form - a standard shape that makes structure explicit and enables systematic comparison between formulae.

Literals, Clauses, and the Building Blocks

A literal is either an atomic proposition $p$ (a positive literal) or its negation $\neg p$ (a negative literal). A minterm over variables $p_1, \ldots, p_n$ is a conjunction of exactly $n$ literals, one for each variable. A maxterm over $p_1, \ldots, p_n$ is a disjunction of exactly $n$ literals, one for each variable.

For variables $p, q$, the minterms are $p \wedge q$, $p \wedge \neg q$, $\neg p \wedge q$, $\neg p \wedge \neg q$ - one for each of the four truth assignments. The minterm $p \wedge \neg q$ is true exactly when $p = \text{T}$ and $q = \text{F}$; no other minterm is true for that assignment. Each truth assignment makes exactly one minterm true.

Disjunctive Normal Form (DNF)

A formula is in disjunctive normal form if it is a disjunction ($\vee$) of conjunctions of literals - “a sum of products.” For example, $(p \wedge q) \vee (\neg p \wedge r) \vee q$ is a DNF formula. Each conjunction is called a disjunct or clause.

Every formula has an equivalent DNF. The construction from a truth table is direct: for each row of the truth table where the formula evaluates to T, form a conjunction of literals that is true exactly on that row (use $p_i$ if variable $i$ is T in that row, $\neg p_i$ if it is F). Take the disjunction of all such conjunctions.

Example. Consider the formula $(p \to q) \wedge r$ with truth table:

$$\begin{array}{ccc|c} p & q & r & (p \to q) \wedge r \\ \hline \text{T} & \text{T} & \text{T} & \text{T} \\ \text{T} & \text{T} & \text{F} & \text{F} \\ \text{T} & \text{F} & \text{T} & \text{F} \\ \text{T} & \text{F} & \text{F} & \text{F} \\ \text{F} & \text{T} & \text{T} & \text{T} \\ \text{F} & \text{T} & \text{F} & \text{F} \\ \text{F} & \text{F} & \text{T} & \text{T} \\ \text{F} & \text{F} & \text{F} & \text{F} \end{array}$$

The formula is true on rows 1, 5, and 7. The corresponding minterms are:

  • Row 1 ($p = \text{T}, q = \text{T}, r = \text{T}$): $p \wedge q \wedge r$
  • Row 5 ($p = \text{F}, q = \text{T}, r = \text{T}$): $\neg p \wedge q \wedge r$
  • Row 7 ($p = \text{F}, q = \text{F}, r = \text{T}$): $\neg p \wedge \neg q \wedge r$

The Principal DNF (PDNF), also called perfect DNF, is the DNF where every clause is a minterm containing every variable exactly once:

$$(p \to q) \wedge r ;\equiv; (p \wedge q \wedge r) \vee (\neg p \wedge q \wedge r) \vee (\neg p \wedge \neg q \wedge r)$$

The PDNF is unique for a given formula (up to reordering of clauses and literals) and represents the formula completely in terms of which truth assignments satisfy it.

Converting a non-principal DNF to PDNF. If a DNF clause is missing a variable, expand it using the tautology $p \equiv (p \wedge q) \vee (p \wedge \neg q)$. For instance, if a clause is $p \wedge r$ (missing $q$), replace it by $(p \wedge q \wedge r) \vee (p \wedge \neg q \wedge r)$. Repeat for each missing variable; duplicate minterms are removed.

Conjunctive Normal Form (CNF)

A formula is in conjunctive normal form if it is a conjunction ($\wedge$) of disjunctions of literals - “a product of sums.” For example, $(p \vee \neg q) \wedge (\neg p \vee r) \wedge q$ is a CNF formula. Each disjunction is called a conjunct or clause.

Every formula has an equivalent CNF. The truth-table construction: for each row where the formula evaluates to F, form a disjunction of literals that is false exactly on that row (use $\neg p_i$ if variable $i$ is T in that row, $p_i$ if it is F - the opposite of the DNF rule). Take the conjunction of all such disjunctions.

For the same example $(p \to q) \wedge r$: the formula is false on rows 2, 3, 4, 6, and 8. For row 2 ($p = \text{T}, q = \text{T}, r = \text{F}$): a maxterm false exactly there is $\neg p \vee \neg q \vee r$. For row 3 ($p = \text{T}, q = \text{F}, r = \text{T}$): $\neg p \vee q \vee \neg r$. And so forth. The conjunction of all five maxterms gives the Principal CNF (PCNF), the unique CNF representation in terms of which truth assignments falsify the formula.

In practice, CNF is the standard input format for SAT solvers. Resolution-based theorem provers work in CNF because the resolution rule applies cleanly to clauses. The Davis-Putnam-Logemann-Loveland (DPLL) algorithm and modern CDCL SAT solvers all operate on CNF.

Converting to CNF algebraically: apply implication elimination, push negations inward using De Morgan’s laws (double negation, De Morgan), then distribute $\wedge$ over $\vee$. This can produce exponentially large CNFs in the worst case; the Tseitin transformation avoids this by introducing fresh variables for subformulae, producing a CNF that is equisatisfiable (satisfiable iff the original is) though not equivalent.

Inference and Valid Arguments

A formal argument consists of a finite set of premises $P_1, P_2, \ldots, P_n$ and a conclusion $C$. The argument is valid if whenever all premises are true, the conclusion must also be true. Equivalently: the argument is valid if and only if

$$(P_1 \wedge P_2 \wedge \cdots \wedge P_n) \to C$$

is a tautology. This is the core semantic definition of validity. An argument is sound if it is both valid and all its premises are actually true. Validity is a property of form; soundness is a property of form and fact together.

A rule of inference is a valid argument schema - a pattern of premises and conclusion that is valid for any substitution of formulae for the schematic variables. The notation $P_1, P_2 \vdash C$ means “from premises $P_1$ and $P_2$, conclude $C$.”

The Standard Rules of Inference

Modus Ponens (MP): $$p, ;; p \to q ;\vdash; q$$

The most fundamental rule: from a conditional and its antecedent, derive the consequent. Validity: if $p$ is true and $p \to q$ is true, then $q$ must be true (the only way $p \to q$ is false is when $p$ is true and $q$ is false, which is excluded).

Modus Tollens (MT): $$\neg q, ;; p \to q ;\vdash; \neg p$$

Contrapositive form of modus ponens: if $q$ is false and $p$ would imply $q$, then $p$ must be false. Validity follows from the contrapositive equivalence $p \to q \equiv \neg q \to \neg p$.

Hypothetical Syllogism (HS): $$p \to q, ;; q \to r ;\vdash; p \to r$$

Chains implications: if $p$ implies $q$ and $q$ implies $r$, then $p$ implies $r$. Validity: assume $p$ is true; by the first premise, $q$ is true; by the second premise, $r$ is true. So whenever $p$ is true, $r$ is true.

Disjunctive Syllogism (DS): $$p \vee q, ;; \neg p ;\vdash; q$$

Eliminates one disjunct: if at least one of $p$ or $q$ holds and $p$ fails, then $q$ must hold.

Addition (Add): $$p ;\vdash; p \vee q$$

Weakening: any formula $q$ can be added as a disjunct to a known truth.

Simplification (Simp): $$p \wedge q ;\vdash; p$$

Projection: from a conjunction, derive either conjunct.

Conjunction (Conj): $$p, ;; q ;\vdash; p \wedge q$$

Introduction of conjunction: if both components are established separately, combine them.

Resolution (Res): $$p \vee q, ;; \neg p \vee r ;\vdash; q \vee r$$

The backbone of SAT solving: two clauses sharing a complementary literal $p / \neg p$ resolve to produce a new clause. When $r = \text{F}$, this reduces to disjunctive syllogism. Resolution is refutation-complete for propositional logic - if a set of CNF clauses is unsatisfiable, resolution will derive the empty clause.

Formal Proofs

A formal proof of $C$ from premises $\Gamma = \{P_1, \ldots, P_n\}$ is a finite sequence of formulae $F_1, F_2, \ldots, F_k = C$ where each $F_i$ is either a premise (an element of $\Gamma$) or follows from earlier formulae by a rule of inference. The sequence is the derivation; its last element is the conclusion.

Example 1: Prove $q$ from $\{p \vee q, ; p \to r, ; \neg r\}$.

Step Formula Justification
1 $p \to r$ Premise
2 $\neg r$ Premise
3 $\neg p$ MT from 1, 2
4 $p \vee q$ Premise
5 $q$ DS from 4, 3

Example 2: Prove $p \to r$ from $\{p \to q, ; q \to r\}$.

Step Formula Justification
1 $p \to q$ Premise
2 $q \to r$ Premise
3 $p \to r$ HS from 1, 2

This is simply hypothetical syllogism applied once.

Soundness and Completeness

The inference rules in the previous section were not chosen arbitrarily. They satisfy two properties that together make formal logic useful.

Soundness: Every formula derivable from a set of premises $\Gamma$ using the inference rules is semantically entailed by $\Gamma$ - it is true in every interpretation that makes all of $\Gamma$ true. This means the rules never produce false conclusions from true premises. A proof is a guarantee.

Completeness: Every formula semantically entailed by $\Gamma$ is syntactically derivable from $\Gamma$. This means the rules are powerful enough to derive everything that is “actually true.” No true statement is left unprovable.

Together: $\Gamma \vdash \phi$ (syntactic derivation) if and only if $\Gamma \models \phi$ (semantic entailment). This is why the two halves of this post - truth tables and inference rules - are not two different subjects. They are two descriptions of the same thing.

What this means in practice. To verify a formula is a tautology, you can either (a) check all $2^n$ truth assignments (semantic, always terminable, sometimes slow), or (b) derive it from no premises using inference rules (syntactic, sometimes faster, sometimes requires ingenuity). Both methods answer the same question. The semantic method is mechanical; the syntactic method can be more efficient when you know the right proof strategy.

Limitations. Propositional logic is decidable: the truth-table method always terminates. Predicate logic (first-order logic) is complete (Gödel’s completeness theorem) but not decidable (Church-Turing). The boundary between these is where logic meets computability.

The Conditional Proof Rule

The Conditional Proof (CP) rule - also called the rule of conditional proof or the deduction theorem - provides a way to prove an implication $A \to B$ without having $A$ as a hypothesis. The strategy: temporarily assume $A$ as an additional premise, derive $B$ under that assumption, then conclude that $A \to B$ holds (and discharge the assumption $A$).

Formally: if from premises $\Gamma$ together with the additional assumption $A$ we can derive $B$, then from $\Gamma$ alone we can derive $A \to B$:

$$\text{If } \Gamma, A \vdash B \text{ then } \Gamma \vdash A \to B$$

This is the deduction theorem for propositional logic. Its validity is guaranteed by the semantics: suppose every truth assignment satisfying all of $\Gamma$ and $A$ also satisfies $B$. Then any assignment satisfying $\Gamma$ but not $A$ makes $A \to B$ vacuously true; any assignment satisfying $\Gamma$ and $A$ makes $B$ true, so $A \to B$ is true. In both cases $A \to B$ holds, confirming $\Gamma \vdash A \to B$.

CP is indispensable whenever the conclusion is a conditional or whenever we need to chain several implications. Without CP, proving $A \to B$ would require treating it as a primitive formula and verifying it by other means. With CP, we reduce the problem to the (often simpler) task of deriving $B$ given $A$.

Example 3: Prove $(p \to r) \wedge (q \to r)$ from $\{(p \vee q) \to r\}$.

We need to prove a conjunction, so we prove each conjunct separately and then apply the conjunction rule.

Sub-proof of $p \to r$ (using CP):

Step Formula Justification
1 $(p \vee q) \to r$ Premise
2 $p$ CP Assumption
3 $p \vee q$ Add from 2
4 $r$ MP from 1, 3
5 $p \to r$ CP (discharge assumption at step 2)

Sub-proof of $q \to r$ (using CP):

Step Formula Justification
6 $q$ CP Assumption
7 $p \vee q$ Add from 6
8 $r$ MP from 1, 7
9 $q \to r$ CP (discharge assumption at step 6)

Combining:

Step Formula Justification
10 $(p \to r) \wedge (q \to r)$ Conj from 5, 9

The proof shows why CP is so natural: to prove a conditional, you just assume the antecedent and work toward the consequent. Every mathematical proof of the form “assume $P$, then $Q$, therefore $P \implies Q$” is an instance of CP.

Nested CP. CP can be applied inside another CP invocation. To prove $A \to (B \to C)$ from $\Gamma$: assume $A$, then assume $B$, derive $C$, conclude $B \to C$ by inner CP, conclude $A \to (B \to C)$ by outer CP. This corresponds to the exportation equivalence $(A \wedge B) \to C \equiv A \to (B \to C)$ - currying in logic.

Summary

Logical Equivalence Laws

Name Law
Double Negation $\neg \neg A \equiv A$
De Morgan 1 $\neg(A \wedge B) \equiv \neg A \vee \neg B$
De Morgan 2 $\neg(A \vee B) \equiv \neg A \wedge \neg B$
Commutativity ($\wedge$) $A \wedge B \equiv B \wedge A$
Commutativity ($\vee$) $A \vee B \equiv B \vee A$
Associativity ($\wedge$) $(A \wedge B) \wedge C \equiv A \wedge (B \wedge C)$
Associativity ($\vee$) $(A \vee B) \vee C \equiv A \vee (B \vee C)$
Distributivity ($\wedge$ over $\vee$) $A \wedge (B \vee C) \equiv (A \wedge B) \vee (A \wedge C)$
Distributivity ($\vee$ over $\wedge$) $A \vee (B \wedge C) \equiv (A \vee B) \wedge (A \vee C)$
Absorption $A \wedge (A \vee B) \equiv A$, $;; A \vee (A \wedge B) \equiv A$
Idempotence $A \wedge A \equiv A$, $;; A \vee A \equiv A$
Implication Elimination $A \to B \equiv \neg A \vee B$
Contrapositive $A \to B \equiv \neg B \to \neg A$
Biconditional Elimination $A \leftrightarrow B \equiv (A \to B) \wedge (B \to A)$
Exportation $(A \wedge B) \to C \equiv A \to (B \to C)$

Rules of Inference

Rule Premises Conclusion
Modus Ponens $p$, $;; p \to q$ $q$
Modus Tollens $\neg q$, $;; p \to q$ $\neg p$
Hypothetical Syllogism $p \to q$, $;; q \to r$ $p \to r$
Disjunctive Syllogism $p \vee q$, $;; \neg p$ $q$
Addition $p$ $p \vee q$
Simplification $p \wedge q$ $p$
Conjunction $p$, $;; q$ $p \wedge q$
Resolution $p \vee q$, $;; \neg p \vee r$ $q \vee r$
Conditional Proof $\Gamma, A \vdash B$ $\Gamma \vdash A \to B$

Read next: