Formal system with propositions, connectives. Satisfiability.
Deep-dive lesson - accessible entry point but dense material. Use worked examples and spaced repetition.
Propositional logic is the smallest “formal language” where you can clearly separate two worlds: (1) syntax—what strings of symbols are well-formed—and (2) semantics—what those strings mean under a truth assignment. That split is the foundation of formal verification, SAT solving, and (eventually) NP-completeness and predicate logic.
Propositional logic builds formulas from atomic propositions (p, q, r) using connectives (¬, ∧, ∨, →, ↔). A valuation v assigns each atom T/F; semantics evaluates a formula to T/F under v. Key tasks: evaluate a formula under v, decide satisfiable/unsatisfiable, check validity, and reduce entailment Γ ⊨ φ to an unsatisfiability check of Γ ∧ ¬φ.
In everyday reasoning you mix language (“If it rains, the ground is wet”) with meaning (is it true today?). Propositional logic exists to make that separation precise:
This separation lets you do three powerful things:
You already know Boolean operators and truth tables. Propositional logic adds:
Atomic propositions (aka propositional variables): symbols like p, q, r. Each represents an indivisible statement with a truth value (T/F). Propositional logic does not look inside p to see structure like “rains(today)”. That is what predicate logic will do later.
Connectives (common set):
| Name | Symbol(s) | Reads as | Intuition |
|---|---|---|---|
| Negation | ¬φ | not φ | flips truth |
| Conjunction | φ ∧ ψ | φ and ψ | both true |
| Disjunction | φ ∨ ψ | φ or ψ | at least one true |
| Implication | φ → ψ | if φ then ψ | false only when φ true and ψ false |
| Biconditional | φ ↔ ψ | φ iff ψ | same truth value |
Well-formed formula (WFF): a string built by rules, e.g.
Parentheses (or operator precedence) remove ambiguity.
A valuation (truth assignment) v maps atoms to {T, F}. For example:
Then each connective is defined truth-functionally. For implication:
Everything else is defined similarly. The important meta-point: meaning is computed structurally from syntax.
Given a formula φ:
These are different questions. For example, p ∨ ¬p is valid. p ∧ ¬p is unsatisfiable. p → q is satisfiable but not valid.
A valuation v is like a point in a space of possible worlds. With two atoms p and q there are 4 valuations:
q=T q=F
+--------+ +--------+
p=T | (T,T) | | (T,F) |
+--------+ +--------+
p=F | (F,T) | | (F,F) |
+--------+ +--------+A formula φ corresponds to a set of valuations (its models):
Thinking this way makes satisfiable/valid/unsatisfiable feel like set properties:
If you want computation or proof, you need to know what the input language is. “p → q → r” is ambiguous unless you specify parsing rules. Syntax gives you:
Let PropVar be a set of atoms: p, q, r, …
Define formulas recursively:
This is a typical inductive definition: it both defines the set of formulas and enables proofs by structural induction.
Many texts adopt precedence like:
And often take → as right-associative: φ → ψ → χ means φ → (ψ → χ).
When in doubt, parenthesize.
Consider the formula:
Its parse tree (abstract syntax tree) makes the structure explicit:
(→)
/ \
(¬) r
|
(∧)
/ \
p qRead it bottom-up: p and q combine with ∧, then negated, then implies r.
This matters because evaluation follows the tree. Also, transformations (like pushing negations inward) are tree rewrites.
In an interactive canvas, a good “syntax mode” task is:
You may see:
The logic is the same; syntax is a surface layer. What matters is the connective’s truth function.
A common learner mistake is to treat formulas as if they are “just” Boolean expressions without appreciating the meta-questions: which valuations make it true? That is the semantics lens.
A valuation v assigns each atom a truth value:
Given v, extend it to all formulas by recursion on structure:
Notice implication’s definition:
This equivalence is extremely useful for transformations.
Because φ → ψ is defined as ¬φ ∨ ψ:
This matches the idea: “the only way to violate a promise ‘if φ then ψ’ is to have φ happen but ψ fail.”
A valuation v is a model of φ if ⟦φ⟧ᵥ = T, written v ⊨ φ.
The set of all models:
This is where the Venn-style picture becomes concrete.
Let the universe U be all valuations over {p, q}. Define:
Then:
A tiny “set” sketch (not to scale) helps:
Universe U (all valuations over p,q)
+---------------------------+
| ________ |
| / \ |
| / A=p \ |
| | ______ | |
| | / B \ | |
| | \_____/ | |
| \ / |
| \________/ |
+---------------------------+
A ∩ B corresponds to p ∧ q
U \ A corresponds to ¬pEven if the drawing is abstract, the mapping “connectives ↔ set operations” is real and is a powerful intuition pump.
Truth tables enumerate all valuations. Structural evaluation computes ⟦φ⟧ᵥ for one v.
In an interactive canvas, you want both workflows:
1) Satisfiable: ∃v, v ⊨ φ
2) Valid: ∀v, v ⊨ φ
3) Entailment: Γ ⊨ φ means every valuation that satisfies all formulas in Γ also satisfies φ.
Formally, for a finite set Γ = {γ₁, …, γₖ}:
Model-set view:
That single subset statement is often the cleanest way to think.
Many reasoning questions can be converted into SAT/UNSAT checks. This is a big deal because:
So you want a mental toolkit of reductions.
A formula φ is valid exactly when ¬φ is unsatisfiable:
Show the work (both directions):
(⇒) If φ is valid, then for all v, ⟦φ⟧ᵥ=T. So for all v, ⟦¬φ⟧ᵥ=F. Hence ¬φ has no model, so it’s UNSAT.
(⇐) If ¬φ is UNSAT, then there is no v with ⟦¬φ⟧ᵥ=T. So for all v, ⟦¬φ⟧ᵥ=F, hence ⟦φ⟧ᵥ=T. So φ is valid.
This “prove validity by showing UNSAT of the negation” is a standard solver workflow.
For a set of premises Γ (think: assumptions) and conclusion φ:
Where “Γ ∧ ¬φ” means conjoining all premises with ¬φ:
Derivation (step-by-step):
Start from definition:
Replace implication with a forbidden counterexample:
But “v ⊨ Γ and not(v ⊨ φ)” is exactly “v ⊨ (Γ ∧ ¬φ)”. So:
And “there does not exist a satisfying valuation” is precisely UNSAT.
If Γ ⊭ φ, then Γ ∧ ¬φ is satisfiable, and any satisfying valuation is a countermodel:
In an interactive canvas, “show counterexample for non-validity” should literally output a valuation v (e.g., p=T, q=F, r=F) and highlight which subformulas evaluate to what.
| Reasoning goal | Convert to | What solver returns |
|---|---|---|
| Is φ satisfiable? | SAT(φ) | a model v if yes |
| Is φ valid? | UNSAT(¬φ) | UNSAT proof or no model |
| Does Γ entail φ? | UNSAT(Γ ∧ ¬φ) | UNSAT or countermodel |
| Are φ and ψ equivalent? | UNSAT((φ ∧ ¬ψ) ∨ (¬φ ∧ ψ)) or UNSAT(¬(φ ↔ ψ)) | UNSAT or countermodel |
This is the “reduction mindset” you’ll reuse in complexity and formal methods.
Propositional logic looks small, but it is the substrate for:
Every formula corresponds to a Boolean circuit:
Evaluation under v is circuit evaluation. Satisfiability is “is there an input making the output 1?” Validity is “does the circuit output 1 for all inputs?”
This is why SAT solvers are so effective: they are optimized engines for exploring huge input spaces using pruning and learned clauses.
A standard solver interface expects CNF (conjunctive normal form):
where each literal ℓ is either p or ¬p.
You do not need full CNF conversion details yet, but conceptually:
Suppose a system must satisfy a safety property Safe under assumptions A.
You want: A ⊨ Safe.
Reduce to UNSAT:
If SAT, the model is a counterexample scenario (a bug trace in richer logics).
SAT is central because:
So the satisfiability question you learned here becomes the landmark problem behind P vs NP discussions.
Predicate logic keeps the same pattern:
But satisfiability becomes much harder (even undecidable in full first-order logic). Propositional logic is the “controlled environment” where the key ideas are clean.
A good interactive environment for this node should support three concrete learner actions:
These tasks force the syntax/semantics split and make “models” tangible rather than abstract.
Let φ = ¬(p ∧ q) → r. Use valuation v with v(p)=T, v(q)=F, v(r)=F. Compute ⟦φ⟧ᵥ step-by-step following the parse tree.
Start with the innermost connective: (p ∧ q).
We have ⟦p⟧ᵥ = T and ⟦q⟧ᵥ = F.
So ⟦p ∧ q⟧ᵥ = T ∧ F = F.
Negate that subformula:
⟦¬(p ∧ q)⟧ᵥ = ¬F = T.
Evaluate the implication:
φ = ¬(p ∧ q) → r.
We have left side = T and ⟦r⟧ᵥ = F.
So ⟦φ⟧ᵥ = T → F = F (this is the one falsifying case for implication).
Insight: Evaluation is structural: compute leaves (atoms), combine upward using connective definitions. The parse tree is an evaluation plan. Implication is only false when antecedent is true and consequent is false.
Consider ψ = (p → q) → (¬q → ¬p). Decide whether ψ is valid. If not, give a counterexample valuation; if yes, argue via UNSAT of its negation or direct reasoning.
Recognize the pattern: (p → q) → (¬q → ¬p) is the law of contraposition, which should be valid in propositional logic (material implication).
Confirm by reasoning with truth-functional equivalences.
First rewrite implications:
(p → q) ≡ (¬p ∨ q)
(¬q → ¬p) ≡ (q ∨ ¬p)
So ψ becomes:
(¬p ∨ q) → (q ∨ ¬p).
But the antecedent and consequent are syntactically the same up to commutativity of ∨:
(¬p ∨ q) and (q ∨ ¬p) are equivalent.
So we have a form: A → A, which is always true.
Therefore ψ is valid: for all valuations v, ⟦ψ⟧ᵥ = T.
Equivalently, ¬ψ is UNSAT, so no counterexample valuation exists.
Insight: A practical way to test validity is to (1) rewrite → as ¬· ∨ ·, then (2) simplify. Validity means there is no valuation that makes the formula false; solver-style, that’s UNSAT(¬ψ).
Let Γ = { p → q, q → r } and let conclusion be φ = p → r. Decide whether Γ ⊨ φ by reducing to UNSAT of (Γ ∧ ¬φ).
Write the entailment-to-UNSAT reduction:
Γ ⊨ φ iff ( (p → q) ∧ (q → r) ∧ ¬(p → r) ) is UNSAT.
Rewrite implications using (a → b) ≡ (¬a ∨ b):
(p → q) ≡ (¬p ∨ q)
(q → r) ≡ (¬q ∨ r)
(p → r) ≡ (¬p ∨ r)
So the conjunction becomes:
(¬p ∨ q) ∧ (¬q ∨ r) ∧ ¬(¬p ∨ r).
Simplify the negation:
¬(¬p ∨ r) ≡ (p ∧ ¬r) by De Morgan’s law.
Now we have:
(¬p ∨ q) ∧ (¬q ∨ r) ∧ (p ∧ ¬r).
Use (p ∧ ¬r) as strong constraints.
From p=true, the clause (¬p ∨ q) forces q=true.
From ¬r (so r=false), the clause (¬q ∨ r) becomes (¬q ∨ false) which forces ¬q=true, i.e., q=false.
We derived q=true and q=false, a contradiction.
Therefore the conjunction is UNSAT, hence Γ ⊨ (p → r).
Insight: Entailment checks become satisfiability checks. If the reduced formula were SAT, the satisfying valuation would be a concrete counterexample where all premises hold but the conclusion fails.
Propositional logic separates syntax (well-formed formulas) from semantics (truth under a valuation v).
A valuation v assigns each atomic proposition a truth value; semantics extends v to all formulas by structural recursion.
A model of φ is a valuation v with v ⊨ φ; the model set Mod(φ) is the set of all such valuations.
Satisfiable means Mod(φ) ≠ ∅; valid means Mod(φ) is all valuations; unsatisfiable means Mod(φ)=∅.
Material implication satisfies (φ → ψ) ≡ (¬φ ∨ ψ) and is false only when φ is true and ψ is false.
Validity reduces to UNSAT: φ is valid iff ¬φ is unsatisfiable.
Entailment reduces to UNSAT: Γ ⊨ φ iff (Γ ∧ ¬φ) is unsatisfiable; otherwise a satisfying valuation is a countermodel.
Parse trees make formula structure explicit and guide evaluation and rewriting.
Treating implication as causal implication rather than material implication; forgetting that if the antecedent is false, φ → ψ evaluates to true.
Confusing satisfiable with valid: a formula can be satisfiable (true in some valuations) but not valid (not true in all).
Mixing syntax and semantics: thinking “φ contains p” implies anything about its truth, without specifying a valuation.
Checking entailment by testing random valuations, instead of constructing (Γ ∧ ¬φ) and searching for a countermodel systematically.
Let φ = (p ∨ q) ∧ ¬p. (a) Find one valuation v that satisfies φ. (b) Is φ satisfiable, valid, or unsatisfiable?
Hint: To satisfy a conjunction, satisfy both parts. ¬p forces p=F; then make (p ∨ q) true by choosing q.
(a) Choose v(p)=F, v(q)=T. Then (p ∨ q)=T and ¬p=T, so φ=T.
(b) φ is satisfiable (we found a model). It is not valid because if p=T and q=F then (p ∨ q)=T but ¬p=F so φ=F. Therefore it is satisfiable but not valid.
Decide whether the formula ψ = (p → q) ∧ p ∧ ¬q is satisfiable. If it is unsatisfiable, explain why in a few steps.
Hint: Use the definition of implication: (p → q) is false only when p=T and q=F. Compare with p and ¬q constraints.
From p ∧ ¬q we get p=T and q=F. But then (p → q) evaluates to T → F = F. So the conjunction (p → q) ∧ p ∧ ¬q is false under any valuation satisfying p ∧ ¬q, and there is no other way to satisfy the conjunction. Hence ψ is UNSAT.
Entailment practice: Let Γ = { p ∨ q, ¬p } and conclusion be φ = q. Determine whether Γ ⊨ φ by reducing to UNSAT of (Γ ∧ ¬φ).
Hint: Build (p ∨ q) ∧ ¬p ∧ ¬q and see if any valuation satisfies it.
Reduce:
Γ ⊨ q iff ( (p ∨ q) ∧ ¬p ∧ ¬q ) is UNSAT.
But ¬p ∧ ¬q forces p=F and q=F, which makes (p ∨ q)=F. So the conjunction cannot be satisfied by any valuation. Therefore it is UNSAT and Γ ⊨ q.
Next nodes:
Related reinforcement: