Logical Equivalences, Validity, and Satisfiability

Logical Equivalence

Two sentences α and β are logically equivalent, written α ≡ β, iff they are true in exactly the same set of models: M(α) = M(β).

Equivalently: α ≡ β iff α ↔︎ β is a tautology.

Standard Equivalences

Name	Equivalence
Commutativity of ∧	`α ∧ β ≡ β ∧ α`
Commutativity of ∨	`α ∨ β ≡ β ∨ α`
Associativity of ∧	`(α ∧ β) ∧ γ ≡ α ∧ (β ∧ γ)`
Associativity of ∨	`(α ∨ β) ∨ γ ≡ α ∨ (β ∨ γ)`
Double negation	`¬¬α ≡ α`
Contrapositive	`α → β ≡ ¬β → ¬α`
Implication elimination	`α → β ≡ ¬α ∨ β`
Biconditional elimination	`α ↔︎ β ≡ (α → β) ∧ (β → α)`
De Morgan 1	`¬(α ∧ β) ≡ ¬α ∨ ¬β`
De Morgan 2	`¬(α ∨ β) ≡ ¬α ∧ ¬β`
Distributivity ∧ over ∨	`α ∧ (β ∨ γ) ≡ (α ∧ β) ∨ (α ∧ γ)`
Distributivity ∨ over ∧	`α ∨ (β ∧ γ) ≡ (α ∨ β) ∧ (α ∨ γ)`

These are used to convert any sentence to CNF (required by resolution). The conversion procedure applies them systematically (see file 6).

Validity (Tautology)

A sentence is valid if it is true in ALL models.

Examples: - P ∨ ¬P (law of excluded middle) - (P ∧ Q) → P - (P → Q) ↔︎ (¬Q → ¬P) (contrapositive)

Connection to entailment: KB ⊨ α iff (KB → α) is a tautology. Equivalently:

KB ⊨ α iff KB ∧ ¬α is unsatisfiable

This is the basis for proof by refutation.

Satisfiability

A sentence is satisfiable if it is true in SOME model.

P ∧ Q — satisfiable (model: P=T, Q=T)
P ∧ ¬P — NOT satisfiable (contradiction)

SAT problem: Is a given propositional sentence satisfiable? NP-complete in general.

Unsatisfiability (Contradiction)

A sentence is unsatisfiable if it is true in NO model.

P ∧ ¬P
(P → Q) ∧ P ∧ ¬Q

The refutation connection:

KB ⊨ α iff KB ∧ ¬α is unsatisfiable.

Proof: If KB ⊨ α, every model of KB satisfies α, so no model satisfies KB ∧ ¬α. Conversely, if KB ∧ ¬α is unsatisfiable, there is no model where KB is true and α is false.

The Trichotomy

Every sentence falls into exactly one of:

┌─────────────────────────────────────────────┐
│  SATISFIABLE                                │
│  ┌──────────────────────────────────────┐   │
│  │  CONTINGENT                          │   │
│  │  (true in some, false in others)     │   │
│  └──────────────────────────────────────┘   │
│  ┌───────────┐                              │
│  │ TAUTOLOGY │  (true in ALL models)        │
│  └───────────┘                              │
├─────────────────────────────────────────────┤
│  UNSATISFIABLE  (true in NO models)         │
└─────────────────────────────────────────────┘

Valid ↔︎ ¬α is unsatisfiable
Unsatisfiable ↔︎ ¬α is valid
Satisfiable but not valid ↔︎ contingent

Key Inference Rules

Rule	Form	Name
Modus Ponens	`α → β, α ⊢ β`	MP
Modus Tollens	`α → β, ¬β ⊢ ¬α`	MT
And-Elimination	`α ∧ β ⊢ α`	And-Elim
Double-Negation Elim.	`¬¬α ⊢ α`	DNE
Unit Resolution	`α ∨ β, ¬β ⊢ α`	Unit-Res
Resolution	`α ∨ β, ¬β ∨ γ ⊢ α ∨ γ`	Resolution

Each rule is sound: the conclusion is entailed by the premises.