Quantifiers
Difficulty: hard — 2 definitions, 0 abbreviations, 3 lemmas, 4 theorems, 0 examples.
The universal and existential quantifiers for first-order logic, defined via Mathlib’s own FirstOrder.Language.Formula.iAlls/FirstOrder.Language.Formula.iExs (quantifying away one name at a time, relabelled into the extra slot they expect), and shown to satisfy Popper’s characterizing properties (Popper.Basis1.IsUniversal, Popper.Basis1.IsExistential) against FirstOrderLogic.semanticBasis3.
The interesting direction in both cases needs a name \(y\) that is fresh for both the formula being quantified and the context formula \(c\): freshness for \(c\) (via Popper.NonDep) lets a fact about \(c\) and one specific valuation transfer to every valuation agreeing with it off \(y\), not just those reachable by renaming \(y\) to another name — the same Function.update_idem/Function.update_comm algebra FirstOrderLogic.basis3ext’s own substitution laws already rely on.
Logic.FirstOrderLogic.all
\(\mathrm{all}(x, \varphi) = \forall x. \varphi\): quantify \(\varphi\) over \(x\), by relabelling \(x\)’s occurrences into the extra slot FirstOrder.Language.Formula.iAlls expects and quantifying that slot away.
def Logic.FirstOrderLogic.all.{u_1, u_2} {L : FirstOrder.Language} {α : Type} [DecidableEq α] (x : α) (φ : L.Formula α) : L.Formula α
Show details
| Logic.FirstOrderLogic.all x φ = FirstOrder.Language.Formula.iAlls PUnit.{1} (FirstOrder.Language.Formula.relabel (fun a => if a = x then Sum.inr () else Sum.inl a) φ)
Complexity: 83 (size of the value term)
Outer dependencies: (none)
Logic.FirstOrderLogic.ex
\(\mathrm{ex}(x, \varphi) = \exists x. \varphi\): the existential counterpart of FirstOrderLogic.all.
def Logic.FirstOrderLogic.ex.{u_1, u_2} {L : FirstOrder.Language} {α : Type} [DecidableEq α] (x : α) (φ : L.Formula α) : L.Formula α
Show details
| Logic.FirstOrderLogic.ex x φ = FirstOrder.Language.Formula.iExs PUnit.{1} (FirstOrder.Language.Formula.relabel (fun a => if a = x then Sum.inr () else Sum.inl a) φ)
Complexity: 83 (size of the value term)
Outer dependencies: (none)
Logic.FirstOrderLogic.realize_all
Realizing \(\forall x.\varphi\) at a valuation is realizing \(\varphi\) at every valuation that agrees with it off \(x\): the whole point of relabelling \(x\) into FirstOrder.Language.Formula.iAlls’s own slot.
theorem Logic.FirstOrderLogic.realize_all.{u_1, u_2} {L : FirstOrder.Language} {α : Type} [DecidableEq α] {x : α} {φ : L.Formula α} {M : Type} [L.Structure M] {v : α → M} : (Logic.FirstOrderLogic.all x φ).Realize v ↔ ∀ (m : M), φ.Realize (Function.update v x m)
Show details
fun {L} {α} [inst : DecidableEq α] {x} {φ} {M} [inst_1 : L.Structure M] {v} => id (Eq.mpr (id (congrArg (fun _a => _a ↔ ∀ (m : M), φ.Realize (Function.update v x m)) (propext FirstOrder.Language.Formula.realize_iAlls))) { mp := fun h m => have this := h fun x => m; Eq.mpr (eq_of_heq ((fun L M inst α φ v v' e'_6 => Eq.casesOn (motive := fun a x => v' = a → e'_6 ≍ x → φ.Realize v ≍ φ.Realize v') e'_6 (fun h => Eq.ndrec (motive := fun v' => ∀ (e_6 : v = v'), e_6 ≍ Eq.refl v → φ.Realize v ≍ φ.Realize v') (fun e_6 h => HEq.refl (φ.Realize v)) (Eq.symm h) e'_6) (Eq.refl v') (HEq.refl e'_6)) L M inst_1 α φ (Function.update v x m) ((fun a => Sum.elim v (fun x => m) a) ∘ fun a => if a = x then Sum.inr () else Sum.inl a) (funext fun a => if ha : a = x then of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (dite_cond_eq_true (Eq.trans (congrFun' (congrArg Eq ha) x) (eq_self x))) (eq_rec_constant m (Eq.symm (of_eq_true (Eq.trans (congrFun' (congrArg Eq ha) x) (eq_self x))))))) (Eq.trans (congrArg ((fun a => Sum.elim v (fun x => m) a) ∘ fun a => if a = x then Sum.inr () else Sum.inl a) ha) (congrArg (Sum.elim v fun x => m) (ite_cond_eq_true (Sum.inr ()) (Sum.inl x) (eq_self x))))) (eq_self m)) else of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_false (eq_false ha))) (congrArg (Sum.elim v fun x => m) (ite_cond_eq_false (Sum.inr ()) (Sum.inl a) (eq_false ha)))) (eq_self (v a)))))) (Eq.mp (congrArg (fun _a => _a) (propext FirstOrder.Language.Formula.realize_relabel)) this), mpr := fun h i => Eq.mpr (id (congrArg (fun _a => _a) (propext FirstOrder.Language.Formula.realize_relabel))) (have this := h (i ()); Eq.mpr (eq_of_heq ((fun L M inst α φ v v' e'_6 => Eq.casesOn (motive := fun a x => v' = a → e'_6 ≍ x → φ.Realize v ≍ φ.Realize v') e'_6 (fun h => Eq.ndrec (motive := fun v' => ∀ (e_6 : v = v'), e_6 ≍ Eq.refl v → φ.Realize v ≍ φ.Realize v') (fun e_6 h => HEq.refl (φ.Realize v)) (Eq.symm h) e'_6) (Eq.refl v') (HEq.refl e'_6)) L M inst_1 α φ ((fun a => Sum.elim v i a) ∘ fun a => if a = x then Sum.inr () else Sum.inl a) (Function.update v x (i ())) (funext fun a => if ha : a = x then of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (congrArg ((fun a => Sum.elim v i a) ∘ fun a => if a = x then Sum.inr () else Sum.inl a) ha) (congrArg (Sum.elim v i) (ite_cond_eq_true (Sum.inr ()) (Sum.inl x) (eq_self x))))) (Eq.trans (dite_cond_eq_true (Eq.trans (congrFun' (congrArg Eq ha) x) (eq_self x))) (eq_rec_constant (i ()) (Eq.symm (of_eq_true (Eq.trans (congrFun' (congrArg Eq ha) x) (eq_self x))))))) (eq_self (i ()))) else of_eq_true (Eq.trans (congr (congrArg Eq (congrArg (Sum.elim v i) (ite_cond_eq_false (Sum.inr ()) (Sum.inl a) (eq_false ha)))) (dite_cond_eq_false (eq_false ha))) (eq_self (v a)))))) this) })
Complexity: 8173 (size of the value term)
Dependencies: Logic.FirstOrderLogic.all
Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.Formula, FirstOrder.Language.Formula.Realize, FirstOrder.Language.Formula.iAlls, FirstOrder.Language.Formula.realize_iAlls, FirstOrder.Language.Formula.realize_relabel, FirstOrder.Language.Formula.relabel, FirstOrder.Language.Structure, Function.update
Lean core dependencies: DecidableEq, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, Function.comp, HEq, Iff, Not, PUnit, Sum, Sum.elim, True, Unit, Unit.unit, congr, congrArg, congrFun', dite, dite_cond_eq_false, dite_cond_eq_true, eq_false, eq_of_heq, eq_self, funext, id, ite, ite_cond_eq_false, ite_cond_eq_true, of_eq_true
Used by: Logic.FirstOrderLogic.hasUniversal
Logic.FirstOrderLogic.realize_ex
Realizing \(\exists x.\varphi\) at a valuation is realizing \(\varphi\) at some valuation that agrees with it off \(x\): the existential counterpart of FirstOrderLogic.realize_all.
theorem Logic.FirstOrderLogic.realize_ex.{u_1, u_2} {L : FirstOrder.Language} {α : Type} [DecidableEq α] {x : α} {φ : L.Formula α} {M : Type} [L.Structure M] {v : α → M} : (Logic.FirstOrderLogic.ex x φ).Realize v ↔ ∃ m, φ.Realize (Function.update v x m)
Show details
fun {L} {α} [inst : DecidableEq α] {x} {φ} {M} [inst_1 : L.Structure M] {v} => id (Eq.mpr (id (congrArg (fun _a => _a ↔ ∃ m, φ.Realize (Function.update v x m)) (propext FirstOrder.Language.Formula.realize_iExs))) { mp := fun a => Exists.casesOn a fun i hi => Exists.intro (i ()) (Eq.mpr (eq_of_heq ((fun L M inst α φ v v' e'_6 => Eq.casesOn (motive := fun a x => v' = a → e'_6 ≍ x → φ.Realize v ≍ φ.Realize v') e'_6 (fun h => Eq.ndrec (motive := fun v' => ∀ (e_6 : v = v'), e_6 ≍ Eq.refl v → φ.Realize v ≍ φ.Realize v') (fun e_6 h => HEq.refl (φ.Realize v)) (Eq.symm h) e'_6) (Eq.refl v') (HEq.refl e'_6)) L M inst_1 α φ (Function.update v x (i ())) (Sum.elim v i ∘ fun a => if a = x then Sum.inr () else Sum.inl a) (funext fun a => if ha : a = x then of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (dite_cond_eq_true (Eq.trans (congrFun' (congrArg Eq ha) x) (eq_self x))) (eq_rec_constant (i ()) (Eq.symm (of_eq_true (Eq.trans (congrFun' (congrArg Eq ha) x) (eq_self x))))))) (Eq.trans (congrArg (Sum.elim v i ∘ fun a => if a = x then Sum.inr () else Sum.inl a) ha) (congrArg (Sum.elim v i) (ite_cond_eq_true (Sum.inr ()) (Sum.inl x) (eq_self x))))) (eq_self (i ()))) else of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_false (eq_false ha))) (congrArg (Sum.elim v i) (ite_cond_eq_false (Sum.inr ()) (Sum.inl a) (eq_false ha)))) (eq_self (v a)))))) (Eq.mp (congrArg (fun _a => _a) (propext FirstOrder.Language.Formula.realize_relabel)) hi)), mpr := fun a => Exists.casesOn a fun m hm => Exists.intro (fun x => m) (Eq.mpr (id (congrArg (fun _a => _a) (propext FirstOrder.Language.Formula.realize_relabel))) (Eq.mpr (eq_of_heq ((fun L M inst α φ v v' e'_6 => Eq.casesOn (motive := fun a x => v' = a → e'_6 ≍ x → φ.Realize v ≍ φ.Realize v') e'_6 (fun h => Eq.ndrec (motive := fun v' => ∀ (e_6 : v = v'), e_6 ≍ Eq.refl v → φ.Realize v ≍ φ.Realize v') (fun e_6 h => HEq.refl (φ.Realize v)) (Eq.symm h) e'_6) (Eq.refl v') (HEq.refl e'_6)) L M inst_1 α φ ((Sum.elim v fun x => m) ∘ fun a => if a = x then Sum.inr () else Sum.inl a) (Function.update v x m) (funext fun a => if ha : a = x then of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (congrArg ((Sum.elim v fun x => m) ∘ fun a => if a = x then Sum.inr () else Sum.inl a) ha) (congrArg (Sum.elim v fun x => m) (ite_cond_eq_true (Sum.inr ()) (Sum.inl x) (eq_self x))))) (Eq.trans (dite_cond_eq_true (Eq.trans (congrFun' (congrArg Eq ha) x) (eq_self x))) (eq_rec_constant m (Eq.symm (of_eq_true (Eq.trans (congrFun' (congrArg Eq ha) x) (eq_self x))))))) (eq_self m)) else of_eq_true (Eq.trans (congr (congrArg Eq (congrArg (Sum.elim v fun x => m) (ite_cond_eq_false (Sum.inr ()) (Sum.inl a) (eq_false ha)))) (dite_cond_eq_false (eq_false ha))) (eq_self (v a)))))) hm)) })
Complexity: 8323 (size of the value term)
Dependencies: Logic.FirstOrderLogic.ex
Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.Formula, FirstOrder.Language.Formula.Realize, FirstOrder.Language.Formula.iExs, FirstOrder.Language.Formula.realize_iExs, FirstOrder.Language.Formula.realize_relabel, FirstOrder.Language.Formula.relabel, FirstOrder.Language.Structure, Function.update
Lean core dependencies: DecidableEq, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, Exists, Function.comp, HEq, Iff, Not, PUnit, Sum, Sum.elim, True, Unit, Unit.unit, congr, congrArg, congrFun', dite, dite_cond_eq_false, dite_cond_eq_true, eq_false, eq_of_heq, eq_self, funext, id, ite, ite_cond_eq_false, ite_cond_eq_true, of_eq_true
Used by: Logic.FirstOrderLogic.hasExistential
Logic.FirstOrderLogic.realize_update_of_nonDep
If \(c\) does not depend on \(y\) (via a witness name \(z \neq y\)) and \(c\) holds at \(v\), \(c\) also holds at \(v\) with \(y\)’s slot set to any semantic value \(m\), not only one reachable by updating \(y\) to another name’s value. Composing the update at \(y\) with a detour through \(z\) and collapsing the two updates at \(y\) (Function.update_idem) is what lifts non-dependence on names to invariance under arbitrary semantic values.
theorem Logic.FirstOrderLogic.realize_update_of_nonDep✝ {L : FirstOrder.Language} {α : Type} [DecidableEq α] {y : α} {c : L.Formula α} (hc : Logic.Popper.NonDep (Logic.FirstOrderLogic.semanticBasis3 L α).toBasis1.Mutual Logic.FirstOrderLogic.SUB c y) {M : Type} [L.Structure M] {v : α → M} (m : M) (z : α) (hz : z ≠ y) (hv : c.Realize v) : c.Realize (Function.update v y m)
Show details
fun {L} {α} [DecidableEq α] {y} {c} hc {M} [L.Structure M] {v} m z hz hv => have hstep := (Logic.Popper.Basis3.follows_toBasis1 (Logic.FirstOrderLogic.semanticBasis3 L α) c (Logic.FirstOrderLogic.SUB c y z)).mp (hc z).right v hv; have hstep2 := Eq.mpr (id (congrArg (fun _a => _a) (propext Logic.FirstOrderLogic.realize_SUB))) (have hz' := Function.update_of_ne hz m v; Eq.mpr (id (congrArg (fun _a => c.Realize (Function.update (Function.update v y m) y _a)) hz')) (Eq.mpr (id (congrArg (fun _a => c.Realize _a) (Function.update_idem m (v z) v))) (Eq.mp (congrArg (fun _a => _a) (propext Logic.FirstOrderLogic.realize_SUB)) hstep))); (Logic.Popper.Basis3.follows_toBasis1 (Logic.FirstOrderLogic.semanticBasis3 L α) (Logic.FirstOrderLogic.SUB c y z) c).mp (hc z).left (Function.update v y m) hstep2
Complexity: 1810 (size of the value term)
Dependencies: Logic.FirstOrderLogic.SUB, Logic.FirstOrderLogic.semanticBasis3, Logic.Popper.Basis1.Mutual, Logic.Popper.Basis3.toBasis1, Logic.Popper.NonDep
Proof dependencies: Logic.FirstOrderLogic.realize_SUB, Logic.Popper.Basis1.Follows, Logic.Popper.Basis3.follows_toBasis1
Logic.FirstOrderLogic.realize_nonDep_update
The two-sided form of FirstOrderLogic.realize_update_of_nonDep: if \(c\) does not depend on \(y\), updating \(y\)’s slot to any semantic value never changes whether \(c\) holds.
theorem Logic.FirstOrderLogic.realize_nonDep_update✝ {L : FirstOrder.Language} {α : Type} [DecidableEq α] [Infinite α] {y : α} {c : L.Formula α} (hc : Logic.Popper.NonDep (Logic.FirstOrderLogic.semanticBasis3 L α).toBasis1.Mutual Logic.FirstOrderLogic.SUB c y) {M : Type} [L.Structure M] {v : α → M} (m : M) : c.Realize (Function.update v y m) ↔ c.Realize v
Show details
fun {L} {α} [DecidableEq α] [Infinite α] {y} {c} hc {M} [L.Structure M] {v} m => Exists.casesOn (exists_ne y) fun z hz => { mp := fun hv0 => have this := Logic.FirstOrderLogic.realize_update_of_nonDep✝ hc (v y) z hz hv0; Eq.mp (congrArg (fun _a => c.Realize _a) (Function.update_eq_self y v)) (Eq.mp (congrArg (fun _a => c.Realize _a) (Function.update_idem m (v y) v)) this), mpr := fun hv => Logic.FirstOrderLogic.realize_update_of_nonDep✝ hc m z hz hv }
Complexity: 2464 (size of the value term)
Dependencies: Logic.FirstOrderLogic.SUB, Logic.FirstOrderLogic.semanticBasis3, Logic.Popper.Basis1.Mutual, Logic.Popper.Basis3.toBasis1, Logic.Popper.NonDep
Proof dependencies: Logic.FirstOrderLogic.realize_update_of_nonDep
Logic.FirstOrderLogic.exists_fresh_ne
A name outside both \(x\) and \(b\)’s own free variables — the shared witness both FirstOrderLogic.hasUniversal and FirstOrderLogic.hasExistential quantify over.
theorem Logic.FirstOrderLogic.exists_fresh_ne✝ {L : FirstOrder.Language} {α : Type} [DecidableEq α] [Infinite α] (x : α) (b : L.Formula α) : ∃ y, x ≠ y ∧ Logic.Popper.NonDep (Logic.FirstOrderLogic.semanticBasis3 L α).toBasis1.Mutual Logic.FirstOrderLogic.SUB b y
Show details
fun {L} {α} [DecidableEq α] [Infinite α] x b => Exists.casesOn (Set.Infinite.exists_notMem_finset Set.infinite_univ (insert x (FirstOrder.Language.BoundedFormula.freeVarFinset b))) fun y h => And.casesOn h fun left hy => Exists.intro y ⟨fun h => hy (h ▸ Finset.mem_insert_self x (FirstOrder.Language.BoundedFormula.freeVarFinset b)), fun w => Logic.FirstOrderLogic.mutual_of_realize_iff fun {M} [L.Structure M] v => Eq.mpr (id (congrArg (fun _a => _a ↔ b.Realize v) (propext Logic.FirstOrderLogic.realize_SUB))) (Logic.FirstOrderLogic.realize_update_of_not_mem_freeVarFinset (fun h => hy (Finset.mem_insert_of_mem h)) v (v w))⟩
Complexity: 1403 (size of the value term)
Dependencies: Logic.FirstOrderLogic.SUB, Logic.FirstOrderLogic.semanticBasis3, Logic.Popper.Basis1.Mutual, Logic.Popper.Basis3.toBasis1, Logic.Popper.NonDep
Proof dependencies: Logic.FirstOrderLogic.mutual_of_realize_iff, Logic.FirstOrderLogic.realize_SUB, Logic.FirstOrderLogic.realize_update_of_not_mem_freeVarFinset
Mathlib dependencies: Finset, Finset.mem_insert_of_mem, Finset.mem_insert_self, FirstOrder.Language, FirstOrder.Language.BoundedFormula.freeVarFinset, FirstOrder.Language.Formula, FirstOrder.Language.Formula.Realize, FirstOrder.Language.Structure, Function.update, Infinite, Set, Set.Infinite.exists_notMem_finset, Set.infinite_univ, Set.univ
Logic.FirstOrderLogic.hasUniversal
Formulas of a fixed language and name type, with semantic entailment as deducibility and FirstOrderLogic.SUB as substitution, satisfy Popper’s characterization of universal quantification: FirstOrderLogic.all witnesses Popper.Basis1.IsUniversal for every name and every formula.
instance Logic.FirstOrderLogic.hasUniversal (L : FirstOrder.Language) (α : Type) [DecidableEq α] [Infinite α] : Logic.Popper.Basis1.HasUniversal (L.Formula α) α (Logic.FirstOrderLogic.semanticBasis3 L α).toBasis1 (Logic.FirstOrderLogic.basis3ext L α)
Show details
| Logic.FirstOrderLogic.hasUniversal L α = { all := Logic.FirstOrderLogic.all, all_isUniversal := ⋯ }
Complexity: 3932 (size of the value term)
Outer dependencies: Logic.FirstOrderLogic.basis3ext, Logic.FirstOrderLogic.semanticBasis3, Logic.Popper.Basis1.HasUniversal, Logic.Popper.Basis3.toBasis1
Inner dependencies: Logic.FirstOrderLogic.SUB, Logic.FirstOrderLogic.all, Logic.FirstOrderLogic.exists_fresh_ne, Logic.FirstOrderLogic.realize_SUB, Logic.FirstOrderLogic.realize_all, Logic.FirstOrderLogic.realize_nonDep_update, Logic.Popper.Basis1.Follows, Logic.Popper.Basis1.IsUniversal, Logic.Popper.Basis1.Mutual, Logic.Popper.Basis3.follows_toBasis1, Logic.Popper.NonDep
Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.Formula, FirstOrder.Language.Formula.Realize, FirstOrder.Language.Structure, Function.update, Function.update_comm, Function.update_self, Infinite
Used by: (none)
Logic.FirstOrderLogic.hasExistential
Formulas of a fixed language and name type, with semantic entailment as deducibility and FirstOrderLogic.SUB as substitution, satisfy Popper’s characterization of existential quantification: FirstOrderLogic.ex witnesses Popper.Basis1.IsExistential for every name and every formula.
instance Logic.FirstOrderLogic.hasExistential (L : FirstOrder.Language) (α : Type) [DecidableEq α] [Infinite α] : Logic.Popper.Basis1.HasExistential (L.Formula α) α (Logic.FirstOrderLogic.semanticBasis3 L α).toBasis1 (Logic.FirstOrderLogic.basis3ext L α)
Show details
| Logic.FirstOrderLogic.hasExistential L α = { ex := Logic.FirstOrderLogic.ex, ex_isExistential := ⋯ }
Complexity: 3932 (size of the value term)
Outer dependencies: Logic.FirstOrderLogic.basis3ext, Logic.FirstOrderLogic.semanticBasis3, Logic.Popper.Basis1.HasExistential, Logic.Popper.Basis3.toBasis1
Inner dependencies: Logic.FirstOrderLogic.SUB, Logic.FirstOrderLogic.ex, Logic.FirstOrderLogic.exists_fresh_ne, Logic.FirstOrderLogic.realize_SUB, Logic.FirstOrderLogic.realize_ex, Logic.FirstOrderLogic.realize_nonDep_update, Logic.Popper.Basis1.Follows, Logic.Popper.Basis1.IsExistential, Logic.Popper.Basis1.Mutual, Logic.Popper.Basis3.follows_toBasis1, Logic.Popper.NonDep
Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.Formula, FirstOrder.Language.Formula.Realize, FirstOrder.Language.Structure, Function.update, Function.update_comm, Function.update_self, Infinite
Used by: (none)
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.