Formula

Difficulty: easy — 3 definitions, 1 abbreviations, 0 lemmas, 0 theorems, 0 examples.

definition abbreviation

legend

The syntax and semantics of classical propositional logic: formulas built from atomic propositions and the four connectives negation, conjunction, disjunction, and implication, and the truth table each formula computes.

Logic.PropositionalLogic.Formula

A propositional formula over a type \(\alpha\) of atomic propositions. Built from an atom, or from a smaller formula (or two) by one of the four connectives: negation, conjunction, disjunction, and implication.

inductive Logic.PropositionalLogic.Formula (α : Type) : Type

atom : α → Logic.PropositionalLogic.Formula α

neg : Logic.PropositionalLogic.Formula α → Logic.PropositionalLogic.Formula α

and : Logic.PropositionalLogic.Formula α →
Logic.PropositionalLogic.Formula α → Logic.PropositionalLogic.Formula α

or : Logic.PropositionalLogic.Formula α →
Logic.PropositionalLogic.Formula α → Logic.PropositionalLogic.Formula α

imp : Logic.PropositionalLogic.Formula α →
Logic.PropositionalLogic.Formula α → Logic.PropositionalLogic.Formula α

Show details

Outer dependencies: (none)

Lean core dependencies: Eq, HEq, Nat, Nat.ble, Nat.decEq, Not, PProd, PULift, PUnit, SizeOf, cond, dite, eq_of_heq

Logic.PropositionalLogic.Valuation

An assignment of a truth value to every atom.

abbrev Logic.PropositionalLogic.Valuation (α : Type) : Type

Show details

| Logic.PropositionalLogic.Valuation α = (α → Bool)

Complexity: 5 (size of the value term)

Outer dependencies: (none)

Lean core dependencies: Bool

Logic.PropositionalLogic.Formula.val

The truth value of a formula under a valuation: the truth table, computed structurally. Each connective’s clause is definitionally its usual truth-table rule, so it needs no separate lemma to unfold — plain simp already knows it.

def Logic.PropositionalLogic.Formula.val {α : Type} (v : Logic.PropositionalLogic.Valuation α) :
  Logic.PropositionalLogic.Formula α → Bool

Show details

| Logic.PropositionalLogic.Formula.val v (Logic.PropositionalLogic.Formula.atom a) = v a
| Logic.PropositionalLogic.Formula.val v φ.neg = !Logic.PropositionalLogic.Formula.val v φ
| Logic.PropositionalLogic.Formula.val v (φ.and ψ) =
  (Logic.PropositionalLogic.Formula.val v φ && Logic.PropositionalLogic.Formula.val v ψ)
| Logic.PropositionalLogic.Formula.val v (φ.or ψ) =
  (Logic.PropositionalLogic.Formula.val v φ || Logic.PropositionalLogic.Formula.val v ψ)
| Logic.PropositionalLogic.Formula.val v (φ.imp ψ) =
  (!Logic.PropositionalLogic.Formula.val v φ || Logic.PropositionalLogic.Formula.val v ψ)

Complexity: 27 (size of the value term)

Outer dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Valuation

Lean core dependencies: Bool, Bool.and, Bool.not, Bool.or, Eq, Eq.mpr, Eq.symm, PProd, PUnit, congrArg, id

Logic.PropositionalLogic.Formula.Tautology

A tautology: true under every valuation.

def Logic.PropositionalLogic.Formula.Tautology {α : Type} (φ : Logic.PropositionalLogic.Formula α) :
  Prop

Show details

| φ.Tautology =
  ∀ (v : Logic.PropositionalLogic.Valuation α), Logic.PropositionalLogic.Formula.val v φ = true

Complexity: 23 (size of the value term)

Outer dependencies: Logic.PropositionalLogic.Formula

Inner dependencies: Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.Valuation

Lean core dependencies: Bool, Eq

Used by: Logic.PropositionalLogic.Formula.completeness, Logic.PropositionalLogic.Formula.soundness

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitionabbreviationdeclared elsewheredependencyproof dependency

legend