📐 Propositional Logic Proofs Using Lean 4: A Practical Guide 🔗

This post provides a technical walkthrough of fundamental propositional logic concepts and their formal implementation using the Lean 4 programming language and theorem prover.

Whether you are a mathematician looking to formalize proofs or a programmer diving into type theory, this guide reconstructs logic from first principles. We will start with basic logical constants and explore how Lean 4 elegantly models logical constructs using the Curry-Howard Isomorphism—the principle that propositions are types and proofs are programs.

📑 Table of Contents 🔗

⚙️ The Preamble: Setting the Stage 🔗

Before defining our logical connectives, we need to set up a foundational environment. In Lean 4, this is typically done using two specific commands to control scope and computational behavior.

namespace Basic

noncomputable section

• namespace Basic: This command groups our definitions, preventing naming conflicts with Lean’s built-in library (the Prelude). It allows us to redefine fundamental structures like True, False, and And from scratch for educational purposes.
• noncomputable section: Lean 4 is both a theorem prover and a functional programming language. By default, it tries to generate executable bytecode for every definition. Marking a section as noncomputable tells the compiler to skip this step, which is common in formal logic where we care about mathematical properties rather than runtime execution.

🧩 Core Logical Connectives 🔗

In this section, we will define the foundational elements of logic, mapping standard mathematical notation to Lean 4 code.

✅ 1. True (⊤) 🔗

The simplest proposition is one that is universally logically valid. In programming terms, $\top$ behaves like a Unit type—it has exactly one state and carries no additional data.

Definition:

inductive True : Prop where
  | intro : True

Because it is defined with a single constructor (intro), the only way to “prove” True is to provide this exact constructor.

Examples:

-- Proving True unconditionally
example : True := True.intro

-- Any proposition 'a' trivially implies True
example {a : Prop} : a → True := fun _ => True.intro

❌ 2. False (⊥) 🔗

While True is defined by the trivial existence of a proof, False is defined by the total absence of one. It is an Empty type (or Void type).

Definition:

inductive False : Prop

Because False has no constructors, you can never instantiate it out of thin air. It represents a logical contradiction.

The Principle of Explosion (Ex Falso Quodlibet): If you ever find yourself holding a proof of False, logic breaks down, and you can prove anything. Lean handles this using the recursor False.elim.

-- From a falsehood, any proposition 'a' follows (⊥ → a)
def False.elim {a : Prop} (false_proof : False) : a := 
  false_proof.rec

🔄 3. Negation (¬) 🔗

In Lean 4, negation is not a primitive, built-in concept. Instead, it is defined functionally using implication and False. To prove that proposition $a$ is false (denoted $\neg a$), you must demonstrate a function where assuming $a$ leads directly to a contradiction ($\bot$).

Definition:

def Not (a : Prop) : Prop := a → False

Key Theorems:

-- Proving Negation: If assuming 'a' proves False, then Not 'a' is true.
theorem Not.intro {a : Prop} (h : a → False) : Not a := 
  fun ha => h ha

-- Double Negation Introduction (a → ¬¬a)
theorem not_not_intro {a : Prop} (ha : a) : Not (Not a) := 
  fun na => na ha  -- 'na' has type (a → False), so passing 'ha' yields False.

-- Modus Tollens: If (a → b) and (¬b), then (¬a)
theorem Not.imp {a b : Prop} (nb : Not b) (ab : a → b) : Not a := 
  fun ha => 
    have hb : b := ab ha
    nb hb

➡️ 4. Implication (→) 🔗

Because Lean relies on type theory, logical implication ($a \to b$) is treated literally as a function. To prove that $a$ implies $b$, you must write a function that takes an arbitrary proof of $a$ and returns a proof of $b$.

Chained Implication Example: If you can turn $c$ into $a$, and turn $b$ into $d$, you can transform a function from $a \to b$ into one from $c \to d$.

theorem imp_imp_imp {a b c d : Prop} 
  (ca : c → a) (bd : b → d) : (a → b) → (c → d) := 
  fun ab => fun hc => 
    have ha : a := ca hc
    have hb : b := ab ha
    bd hb

🔗 5. Conjunction (∧) 🔗

Logical conjunction, requiring both $a$ and $b$ to be true, is modeled as a structure. In programming terms, this is a Product type (a struct or tuple) that holds two separate pieces of evidence.

Definition:

structure And (a b : Prop) : Prop where
  intro ::
  left : a
  right : b

Key Proof Patterns:

-- Introduction: Creating an And
example {a b : Prop} (ha : a) (hb : b) : And a b := 
  And.intro ha hb

-- Symmetry: a ∧ b → b ∧ a
theorem And.symm {a b : Prop} (h : And a b) : And b a := 
  And.intro h.right h.left

🔀 6. Disjunction (∨) 🔗

Logical disjunction requires at least one of the propositions to be true. Unlike And, Or is an inductive Sum type (a tagged union), because there are two distinct, alternative ways to construct a proof.

Definition:

inductive Or (a b : Prop) : Prop where
  | inl (h : a) : Or a b
  | inr (h : b) : Or a b

To prove $a \lor b$, you wrap a proof of $a$ in the inl (inject-left) constructor, or a proof of $b$ in the inr (inject-right) constructor.

Example:

-- Symmetry: a ∨ b → b ∨ a
theorem Or.symm {a b : Prop} (h : Or a b) : Or b a :=
  match h with
  | Or.inl ha => Or.inr ha
  | Or.inr hb => Or.inl hb

↔️ 7. Logical Equivalence (↔) 🔗

Bi-implication, or “if and only if” (Iff), represents that two propositions are logically equivalent. It is defined as a structure holding implications in both directions.

Definition:

structure Iff (a b : Prop) : Prop where
  intro ::
  mp : a → b
  mpr : b → a

Reflexivity Example:

-- Every proposition is equivalent to itself (a ↔ a)
theorem Iff.refl {a : Prop} : Iff a a :=
  Iff.intro (fun ha => ha) (fun ha => ha)

🎯 Conclusion and Key Takeaways 🔗

By rebuilding propositional logic from scratch in Lean 4, we reveal the mechanical beauty of formal systems:

1. Constructive by Default: We define what it means to hold evidence of a truth, rather than merely stating something is true.
2. Propositions as Types: Through the Curry-Howard mapping, logical connectives directly correspond to standard programming structures: Implication is a function, And is a struct, Or is an enum, True is a unit, and False is void.
3. Proofs as Programs: Writing a mathematical proof in Lean is identical to writing a type-safe function that satisfies a specific signature.

Mastering these foundational building blocks provides the crucial stepping stones necessary to tackle more complex mathematical theorems, predicate logic, and the verification of complex software systems.

Kaue's Way of Life

Get It Free