Formula

Difficulty: hard — 2 definitions, 0 abbreviations, 2 lemmas, 6 theorems, 0 examples.

definition lemma theorem

legend

First-order logic reuses Mathlib’s own model theory rather than building formulas, structures, and satisfaction again from scratch: a language fixes the function and relation symbols, a formula ranges over free variables named by some type, a structure interprets the symbols in a carrier, and FirstOrder.Language.Formula.Realize is Mathlib’s own satisfaction relation.

Semantic entailment between two formulas holds when every structure, under every valuation of the free variables, that satisfies the first also satisfies the second — the many-model generalisation of PropositionalLogic.Formula.SemanticEntails. It is reflexive and transitive for free, so formulas over a fixed language and a fixed name type form a Popper.Basis3, exactly the way PropositionalLogic.semanticBasis3 does.

Substitution reuses Mathlib’s own FirstOrder.Language.BoundedFormula.subst, replacing a single name by another via Function.update. Since a formula only ever mentions finitely many names (its free-variable finset), an infinite supply of names is what guarantees the freshness postulate Popper.HasSubstitution needs: some name is always left over. Substitution’s own six structural rules follow from FirstOrder.Language.BoundedFormula.subst’s general algebraic properties, so semantic entailment together with substitution is meant to form a Popper.HasSubstitution instance — Popper’s Basis III extended with substitution (“Basis3ext”), instantiated semantically.

NoteLogic.FirstOrderLogic.SemanticEntails

Semantic entailment: every structure, under every valuation of the free variables, that satisfies \(\varphi\) also satisfies \(\psi\).

def Logic.FirstOrderLogic.SemanticEntails.{u_1, u_2} {L : FirstOrder.Language} {α : Type}
  (φ ψ : L.Formula α) : Prop

Show details

| Logic.FirstOrderLogic.SemanticEntails φ ψ =
  ∀ {M : Type} [inst : L.Structure M] (v : α → M), φ.Realize v → ψ.Realize v

Complexity: 55 (size of the value term)

Outer dependencies: (none)

Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.Formula, FirstOrder.Language.Formula.Realize, FirstOrder.Language.Structure

Used by: Logic.FirstOrderLogic.SemanticEntails.refl, Logic.FirstOrderLogic.SemanticEntails.trans, Logic.FirstOrderLogic.semanticBasis3

TipLogic.FirstOrderLogic.SemanticEntails.refl

Reflexivity of semantic entailment: immediate from the definition.

theorem Logic.FirstOrderLogic.SemanticEntails.refl.{u_1, u_2} {L : FirstOrder.Language} {α : Type}
  (φ : L.Formula α) : Logic.FirstOrderLogic.SemanticEntails φ φ

Show details

fun {L} {α} φ {M} [L.Structure M] x h => h

Complexity: 37 (size of the value term)

Dependencies: Logic.FirstOrderLogic.SemanticEntails

Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.Formula, FirstOrder.Language.Formula.Realize, FirstOrder.Language.Structure

Used by: Logic.FirstOrderLogic.semanticBasis3

TipLogic.FirstOrderLogic.SemanticEntails.trans

Transitivity of semantic entailment: immediate from the definition.

theorem Logic.FirstOrderLogic.SemanticEntails.trans.{u_1, u_2} {L : FirstOrder.Language} {α : Type}
  {φ ψ χ : L.Formula α} (h1 : Logic.FirstOrderLogic.SemanticEntails φ ψ)
  (h2 : Logic.FirstOrderLogic.SemanticEntails ψ χ) : Logic.FirstOrderLogic.SemanticEntails φ χ

Show details

fun {L} {α} {φ ψ χ} h1 h2 {M} [L.Structure M] v h => h2 v (h1 v h)

Complexity: 85 (size of the value term)

Dependencies: Logic.FirstOrderLogic.SemanticEntails

Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.Formula, FirstOrder.Language.Formula.Realize, FirstOrder.Language.Structure

Used by: Logic.FirstOrderLogic.semanticBasis3

ImportantLogic.FirstOrderLogic.semanticBasis3

Formulas of a fixed language over a fixed set of free-variable names, with semantic entailment as the deducibility relation, form a Popper.Basis3 — the first-order counterpart of PropositionalLogic.semanticBasis3.

instance Logic.FirstOrderLogic.semanticBasis3 (L : FirstOrder.Language) (α : Type) [DecidableEq α] :
  Logic.Popper.Basis3 (L.Formula α)

Show details

| Logic.FirstOrderLogic.semanticBasis3 L α =
  { Follows := Logic.FirstOrderLogic.SemanticEntails, refl := ⋯, trans := ⋯ }

Complexity: 57 (size of the value term)

Outer dependencies: Logic.Popper.Basis3

Inner dependencies: Logic.FirstOrderLogic.SemanticEntails, Logic.FirstOrderLogic.SemanticEntails.refl, Logic.FirstOrderLogic.SemanticEntails.trans

Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.Formula

Lean core dependencies: DecidableEq

Used by: Logic.FirstOrderLogic.basis3ext, Logic.FirstOrderLogic.exists_fresh_ne, Logic.FirstOrderLogic.hasExistential, Logic.FirstOrderLogic.hasUniversal, Logic.FirstOrderLogic.mutual_of_realize_iff, Logic.FirstOrderLogic.realize_iff_of_mutual, Logic.FirstOrderLogic.realize_nonDep_update, Logic.FirstOrderLogic.realize_update_of_nonDep

NoteLogic.FirstOrderLogic.SUB

\(\mathrm{SUB}(\varphi, x, y) = \varphi[x := y]\): replace every free occurrence of the name \(x\) by \(y\), using Mathlib’s own substitution (FirstOrder.Language.BoundedFormula.subst) with a single name updated to map to the other, via Function.update.

def Logic.FirstOrderLogic.SUB.{u_1, u_2} {L : FirstOrder.Language} {α : Type} [DecidableEq α]
  (φ : L.Formula α) (x y : α) : L.Formula α

Show details

| Logic.FirstOrderLogic.SUB φ x y =
  FirstOrder.Language.BoundedFormula.subst φ
    (Function.update FirstOrder.Language.var x (FirstOrder.Language.var y))

Complexity: 67 (size of the value term)

Outer dependencies: (none)

Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.BoundedFormula.subst, FirstOrder.Language.Formula, FirstOrder.Language.Term, Function.update

Lean core dependencies: DecidableEq, Nat

Used by: Logic.FirstOrderLogic.basis3ext, Logic.FirstOrderLogic.exists_fresh_ne, Logic.FirstOrderLogic.hasExistential, Logic.FirstOrderLogic.hasUniversal, Logic.FirstOrderLogic.realize_SUB, Logic.FirstOrderLogic.realize_nonDep_update, Logic.FirstOrderLogic.realize_update_of_nonDep

ImportantLogic.FirstOrderLogic.realize_SUB

Realizing \(\mathrm{SUB}(\varphi, x, y)\) at a valuation is the same as realizing \(\varphi\) at the valuation with \(x\)’s slot filled by \(y\)’s value: the whole point of Mathlib’s substitution being built from Function.update.

theorem Logic.FirstOrderLogic.realize_SUB.{u_1, u_2} {L : FirstOrder.Language} {α : Type} [DecidableEq α]
  {φ : L.Formula α} {x y : α} {M : Type} [L.Structure M] {v : α → M} :
  (Logic.FirstOrderLogic.SUB φ x y).Realize v ↔ φ.Realize (Function.update v x (v y))

Show details

fun {L} {α} [DecidableEq α] {φ} {x y} {M} [L.Structure M] {v} =>
  id
    (id
      (Eq.mpr
        (id
          (congrArg
            (fun _a =>
              _a ↔ FirstOrder.Language.BoundedFormula.Realize φ (Function.update v x (v y)) default)
            (propext FirstOrder.Language.BoundedFormula.realize_subst)))
        (have hval :=
          funext fun c =>
            Or.casesOn (eq_or_ne c x)
              (fun h =>
                h ▸
                  of_eq_true
                    (Eq.trans
                      (congr
                        (congrArg Eq
                          (congrArg (FirstOrder.Language.Term.realize v)
                            (Function.update_self c (FirstOrder.Language.var y)
                              FirstOrder.Language.var)))
                        (Function.update_self c (v y) v))
                      (eq_self (v y))))
              fun hc =>
              of_eq_true
                (Eq.trans
                  (congr
                    (congrArg Eq
                      (congrArg (FirstOrder.Language.Term.realize v)
                        ((fun x_0 v f => (fun x_0 => Function.update_of_ne hc) x_0 v f)
                          (fun a => L.Term α) (FirstOrder.Language.var y) FirstOrder.Language.var)))
                    ((fun x_0 v f => (fun x_0 => Function.update_of_ne hc) x_0 v f) (fun a => M)
                      (v y) v))
                  (eq_self (v c)));
        Eq.mpr
          (id
            (congrArg
              (fun _a =>
                FirstOrder.Language.BoundedFormula.Realize φ _a default ↔
                  FirstOrder.Language.BoundedFormula.Realize φ (Function.update v x (v y)) default)
              hval))
          Iff.rfl)))

Complexity: 4410 (size of the value term)

Dependencies: Logic.FirstOrderLogic.SUB

Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.BoundedFormula.Realize, FirstOrder.Language.BoundedFormula.realize_subst, FirstOrder.Language.BoundedFormula.subst, FirstOrder.Language.Formula, FirstOrder.Language.Formula.Realize, FirstOrder.Language.Structure, FirstOrder.Language.Term, FirstOrder.Language.Term.realize, Function.update, Function.update_of_ne, Function.update_self, eq_or_ne

Lean core dependencies: DecidableEq, Eq, Eq.mpr, Eq.trans, Fin, Iff, Iff.rfl, Nat, Ne, Or, True, congr, congrArg, eq_self, funext, id, of_eq_true

Used by: Logic.FirstOrderLogic.basis3ext, Logic.FirstOrderLogic.exists_fresh_ne, Logic.FirstOrderLogic.hasExistential, Logic.FirstOrderLogic.hasUniversal, Logic.FirstOrderLogic.realize_update_of_nonDep

ImportantLogic.FirstOrderLogic.realize_update_of_not_mem_freeVarFinset

A formula’s truth does not see a name it never mentions: changing the valuation’s value at a name outside its free-variable finset leaves the formula’s truth unchanged. Restricting to the (smaller) domain of free variables and back agrees for both valuations, since they agree everywhere that domain can see.

theorem Logic.FirstOrderLogic.realize_update_of_not_mem_freeVarFinset.{u_1, u_2} {L : FirstOrder.Language}
  {α : Type} [DecidableEq α] {φ : L.Formula α} {x : α}
  (hx : x ∉ FirstOrder.Language.BoundedFormula.freeVarFinset φ) {M : Type} [L.Structure M]
  (v : α → M) (m : M) : φ.Realize (Function.update v x m) ↔ φ.Realize v

Show details

fun {L} {α} [DecidableEq α] {φ} {x} hx {M} [L.Structure M] v m =>
  have h := fun x_1 ha hax => hx (hax ▸ ha);
  have e := funext fun a => id (Function.update_of_ne a.property m v);
  id
    (Eq.mpr
      (id
        (congrArg (fun _a => _a ↔ FirstOrder.Language.BoundedFormula.Realize φ v default)
          (Eq.symm (propext (FirstOrder.Language.BoundedFormula.realize_restrictFreeVar' h)))))
      (Eq.mpr
        (id
          (congrArg
            (fun _a =>
              (FirstOrder.Language.BoundedFormula.restrictFreeVar φ (Set.inclusion h)).Realize
                  (Function.update v x m ∘ Subtype.val) default ↔
                _a)
            (Eq.symm (propext (FirstOrder.Language.BoundedFormula.realize_restrictFreeVar' h)))))
        (Eq.mpr
          (id
            (congrArg
              (fun _a =>
                (FirstOrder.Language.BoundedFormula.restrictFreeVar φ (Set.inclusion h)).Realize _a
                    default ↔
                  (FirstOrder.Language.BoundedFormula.restrictFreeVar φ (Set.inclusion h)).Realize
                    (v ∘ Subtype.val) default)
              e))
          Iff.rfl)))

Complexity: 9555 (size of the value term)

Dependencies: (none)

Mathlib dependencies: Finset, FirstOrder.Language, FirstOrder.Language.BoundedFormula.Realize, FirstOrder.Language.BoundedFormula.freeVarFinset, FirstOrder.Language.BoundedFormula.realize_restrictFreeVar', FirstOrder.Language.BoundedFormula.restrictFreeVar, FirstOrder.Language.Formula, FirstOrder.Language.Formula.Realize, FirstOrder.Language.Structure, Function.update, Function.update_of_ne, Set, Set.Elem, Set.inclusion, setOf

Lean core dependencies: DecidableEq, Eq, Eq.mpr, Eq.symm, Fin, Function.comp, Iff, Iff.rfl, Nat, Ne, Not, Subtype, congrArg, funext, id

Used by: Logic.FirstOrderLogic.basis3ext, Logic.FirstOrderLogic.exists_fresh_ne

ImportantLogic.FirstOrderLogic.mutual_of_realize_iff

Formulas of a fixed language and name type, with semantic entailment as deducibility, satisfy Popper’s characterization of mutual deducibility exactly when they are true at exactly the same structures and valuations.

theorem Logic.FirstOrderLogic.mutual_of_realize_iff {L : FirstOrder.Language} {α : Type} [DecidableEq α]
  {φ ψ : L.Formula α}
  (h : ∀ {M : Type} [inst : L.Structure M] (v : α → M), φ.Realize v ↔ ψ.Realize v) :
  (Logic.FirstOrderLogic.semanticBasis3 L α).toBasis1.Mutual φ ψ

Show details

fun {L} {α} [DecidableEq α] {φ ψ} h =>
  ⟨(Logic.Popper.Basis3.follows_toBasis1 (Logic.FirstOrderLogic.semanticBasis3 L α) φ ψ).mpr
      fun {M} [L.Structure M] v => (h v).mp,
    (Logic.Popper.Basis3.follows_toBasis1 (Logic.FirstOrderLogic.semanticBasis3 L α) ψ φ).mpr
      fun {M} [L.Structure M] v => (h v).mpr⟩

Complexity: 359 (size of the value term)

Dependencies: Logic.FirstOrderLogic.semanticBasis3, Logic.Popper.Basis1.Mutual, Logic.Popper.Basis3.toBasis1

Proof dependencies: Logic.Popper.Basis1.Follows, Logic.Popper.Basis3.follows_toBasis1

Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.Formula, FirstOrder.Language.Formula.Realize, FirstOrder.Language.Structure

Lean core dependencies: DecidableEq, Iff

Used by: Logic.FirstOrderLogic.basis3ext, Logic.FirstOrderLogic.exists_fresh_ne

ImportantLogic.FirstOrderLogic.realize_iff_of_mutual

The converse: mutual deducibility unpacks into a truth-agreement statement at any fixed structure and valuation.

theorem Logic.FirstOrderLogic.realize_iff_of_mutual {L : FirstOrder.Language} {α : Type} [DecidableEq α]
  {φ ψ : L.Formula α} (h : (Logic.FirstOrderLogic.semanticBasis3 L α).toBasis1.Mutual φ ψ)
  {M : Type} [L.Structure M] {v : α → M} : φ.Realize v ↔ ψ.Realize v

Show details

fun {L} {α} [DecidableEq α] {φ ψ} h {M} [L.Structure M] {v} =>
  {
    mp :=
      (Logic.Popper.Basis3.follows_toBasis1 (Logic.FirstOrderLogic.semanticBasis3 L α) φ ψ).mp
        h.left v,
    mpr :=
      (Logic.Popper.Basis3.follows_toBasis1 (Logic.FirstOrderLogic.semanticBasis3 L α) ψ φ).mp
        h.right v }

Complexity: 361 (size of the value term)

Dependencies: Logic.FirstOrderLogic.semanticBasis3, Logic.Popper.Basis1.Mutual, Logic.Popper.Basis3.toBasis1

Proof dependencies: Logic.Popper.Basis1.Follows, Logic.Popper.Basis3.follows_toBasis1

Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.Formula, FirstOrder.Language.Formula.Realize, FirstOrder.Language.Structure

Lean core dependencies: DecidableEq, Iff

Used by: Logic.FirstOrderLogic.basis3ext

ImportantLogic.FirstOrderLogic.basis3ext

Substitution (\(\mathrm{SUB}\), §9.1) together with semantic entailment forms a Popper.HasSubstitution: Popper’s Basis III extended with substitution (“Basis3ext”), instantiated semantically. An infinite supply of names is what makes the freshness postulate provable: a formula only ever mentions finitely many names, so some name is always left over.

instance Logic.FirstOrderLogic.basis3ext (L : FirstOrder.Language) (α : Type) [DecidableEq α] [Infinite α] :
  Logic.Popper.HasSubstitution (L.Formula α) α
    (Logic.FirstOrderLogic.semanticBasis3 L α).toBasis1.Mutual

Show details

| Logic.FirstOrderLogic.basis3ext L α =
  { DIST := fun x1 x2 => x1 ≠ x2, SUB := Logic.FirstOrderLogic.SUB, fresh := ⋯, sub_congr := ⋯,
    sub_self := ⋯, sub_vacuous := ⋯, sub_comp := ⋯, sub_comm_same := ⋯, sub_comm := ⋯ }

Complexity: 123 (size of the value term)

Outer dependencies: Logic.FirstOrderLogic.semanticBasis3, Logic.Popper.Basis1.Mutual, Logic.Popper.Basis3.toBasis1, Logic.Popper.HasSubstitution

Inner dependencies: Logic.FirstOrderLogic.SUB, Logic.FirstOrderLogic.mutual_of_realize_iff, Logic.FirstOrderLogic.realize_SUB, Logic.FirstOrderLogic.realize_iff_of_mutual, Logic.FirstOrderLogic.realize_update_of_not_mem_freeVarFinset, Logic.Popper.NonDep

Mathlib dependencies: Finset, FirstOrder.Language, FirstOrder.Language.BoundedFormula.freeVarFinset, FirstOrder.Language.Formula, FirstOrder.Language.Formula.Realize, FirstOrder.Language.Structure, Function.update, Function.update_comm, Function.update_eq_self, Function.update_idem, Function.update_of_ne, Function.update_self, Infinite, Set, Set.Infinite.exists_notMem_finset, Set.infinite_univ, Set.univ, eq_or_ne

Lean core dependencies: And, DecidableEq, Eq, Eq.mpr, Eq.trans, Exists, Iff, Iff.rfl, Nat, Ne, Ne.symm, Not, Or, True, congrArg, congrFun', eq_self, id, of_eq_true

Used by: Logic.FirstOrderLogic.hasExistential, Logic.FirstOrderLogic.hasUniversal

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.

definitionlemmatheoremdeclared elsewheredependencyproof dependency

legend