Flypitch.FOL.Semantics interprets the syntax and proof system from the preceding files in first-order structures. It defines term and formula realization, semantic consequence, and proves the soundness of the natural-deduction rules.

structure Flypitch.fol.Structure (L : Language) : Type (u + 1)

An L-structure consists of a carrier type and interpretations of the symbols of L.

• carrier : Type u
• fun_map {n : ℕ} : L.functions n → dvector self.carrier n → self.carrier
• rel_map {n : ℕ} : L.relations n → dvector self.carrier n → Prop

@[implicit_reducible]

instance Flypitch.fol.instCoeSortStructureType {L : Language} : CoeSort (Structure L) (Type u)

Equations

• Flypitch.fol.instCoeSortStructureType = { coe := fun (S : Flypitch.fol.Structure L) => S.carrier }

def Flypitch.fol.realize_term {L : Language} {M : Structure L} (v : ℕ → M.carrier) {l : ℕ} : preterm L l → dvector M.carrier l → M.carrier

Interpret a partially applied term in a structure under a valuation.

Equations

• Flypitch.fol.realize_term v (&k) x_3 = v k
• Flypitch.fol.realize_term v (Flypitch.fol.preterm.func f) x✝ = M.fun_map f x✝
• Flypitch.fol.realize_term v (t₁.app t₂) x✝ = Flypitch.fol.realize_term v t₁ (Flypitch.dvector.cons (Flypitch.fol.realize_term v t₂ Flypitch.dvector.nil) x✝)

theorem Flypitch.fol.realize_term_congr {L : Language} {M : Structure L} {v v' : ℕ → M.carrier} (h : ∀ (n : ℕ), v n = v' n) {l : ℕ} (t : preterm L l) (xs : dvector M.carrier l) : realize_term v t xs = realize_term v' t xs

Realization depends only on the values of the valuation on free variables of the term.

theorem Flypitch.fol.realize_term_subst {L : Language} {M : Structure L} (v : ℕ → M.carrier) {l : ℕ} (n : ℕ) (t : preterm L l) (s : term L) (xs : dvector M.carrier l) : realize_term (v[realize_term v (s ↑ n) dvector.nil // n]) t xs = realize_term v (t[s // n]) xs

Semantic substitution for terms is computed by changing the valuation at the substituted variable.

theorem Flypitch.fol.realize_term_subst_lift {L : Language} {M : Structure L} (v : ℕ → M.carrier) (x : M.carrier) (m : ℕ) {l : ℕ} (t : preterm L l) (xs : dvector M.carrier l) : realize_term (v[x // m]) (t ↑' 1 # m) xs = realize_term v t xs

Lifting a term corresponds semantically to extending the valuation by a fresh element.

def Flypitch.fol.realize_formula {L : Language} {M : Structure L} {l : ℕ} : (ℕ → M.carrier) → preformula L l → dvector M.carrier l → Prop

Interpret a preformula under a valuation and arguments for its unapplied relation slots.

Equations

• Flypitch.fol.realize_formula x✝ Flypitch.fol.preformula.falsum x_5 = False
• Flypitch.fol.realize_formula x✝ (t₁ ≃ t₂) xs = (Flypitch.fol.realize_term x✝ t₁ xs = Flypitch.fol.realize_term x✝ t₂ xs)
• Flypitch.fol.realize_formula x✝¹ (Flypitch.fol.preformula.rel R) x✝ = M.rel_map R x✝
• Flypitch.fol.realize_formula x✝¹ (f.apprel t) x✝ = Flypitch.fol.realize_formula x✝¹ f (Flypitch.dvector.cons (Flypitch.fol.realize_term x✝¹ t Flypitch.dvector.nil) x✝)
• Flypitch.fol.realize_formula x✝ (f₁ ⟹ f₂) xs = (Flypitch.fol.realize_formula x✝ f₁ xs → Flypitch.fol.realize_formula x✝ f₂ xs)
• Flypitch.fol.realize_formula x✝ (∀' f) xs = ∀ (x : M.carrier), Flypitch.fol.realize_formula (x✝[x // 0]) f xs

theorem Flypitch.fol.realize_formula_congr {L : Language} {M : Structure L} {l : ℕ} {v v' : ℕ → M.carrier} (h : ∀ (n : ℕ), v n = v' n) (f : preformula L l) (xs : dvector M.carrier l) : realize_formula v f xs ↔ realize_formula v' f xs

Realization of formulas is invariant under pointwise-equal valuations.

theorem Flypitch.fol.realize_formula_subst {L : Language} {M : Structure L} {l : ℕ} (v : ℕ → M.carrier) (n : ℕ) (f : preformula L l) (s : term L) (xs : dvector M.carrier l) : realize_formula (v[realize_term v (s ↑ n) dvector.nil // n]) f xs ↔ realize_formula v (subst_formula f s n) xs

Formula substitution is semantically the same as updating the valuation at the substituted variable.

theorem Flypitch.fol.realize_formula_subst0 {L : Language} {M : Structure L} {l : ℕ} (v : ℕ → M.carrier) (f : preformula L l) (s : term L) (xs : dvector M.carrier l) : realize_formula (v[realize_term v s dvector.nil // 0]) f xs ↔ realize_formula v (subst_formula f s 0) xs

Specialization of realize_formula_subst to substitution at variable 0.

theorem Flypitch.fol.realize_formula_subst_lift {L : Language} {M : Structure L} {l : ℕ} (v : ℕ → M.carrier) (x : M.carrier) (m : ℕ) (f : preformula L l) (xs : dvector M.carrier l) : realize_formula (v[x // m]) (lift_formula_at f 1 m) xs = realize_formula v f xs

Lifting a formula is semantically neutral when the valuation is extended at the lifted index.

def Flypitch.fol.satisfied_in {L : Language} (M : Structure L) (f : formula L) : Prop

A closed formula is satisfied in M when every valuation realizes it.

Equations

• Flypitch.fol.satisfied_in M f = ∀ (v : ℕ → M.carrier), Flypitch.fol.realize_formula v f Flypitch.dvector.nil

def Flypitch.fol.all_satisfied_in {L : Language} (M : Structure L) (T : Set (formula L)) : Prop

Every formula in T is satisfied in M.

Equations

• Flypitch.fol.all_satisfied_in M T = ∀ ⦃f : Flypitch.fol.formula L⦄, f ∈ T → Flypitch.fol.satisfied_in M f

def Flypitch.fol.satisfied {L : Language} (T : Set (formula L)) (f : formula L) : Prop

Semantic consequence of a single formula from a set of assumptions.

Equations

• T ⊨ f = ∀ (M : Flypitch.fol.Structure L) (v : ℕ → M.carrier), (∀ g ∈ T, Flypitch.fol.realize_formula v g Flypitch.dvector.nil) → Flypitch.fol.realize_formula v f Flypitch.dvector.nil

def Flypitch.fol.all_satisfied {L : Language} (T T' : Set (formula L)) : Prop

Semantic consequence of every formula in T' from T.

Equations

• Flypitch.fol.all_satisfied T T' = ∀ ⦃f : Flypitch.fol.formula L⦄, f ∈ T' → T ⊨ f

def Flypitch.fol.«term_⊨_» : Lean.TrailingParserDescr

Equations

• Flypitch.fol.«term_⊨_» = Lean.ParserDescr.trailingNode `Flypitch.fol.«term_⊨_» 51 52 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊨ ") (Lean.ParserDescr.cat `term 52))

theorem Flypitch.fol.satisfied_in_trans {L : Language} {M : Structure L} {T : Set (formula L)} {f : formula L} (hMT : all_satisfied_in M T) (hTf : T ⊨ f) : satisfied_in M f

Semantic consequence can be composed with satisfaction in a specific structure.

theorem Flypitch.fol.all_satisfied_in_trans {L : Language} {M : Structure L} {T T' : Set (formula L)} (hMT : all_satisfied_in M T) (hTT' : all_satisfied T T') : all_satisfied_in M T'

Satisfaction of a theory in a structure is closed under semantic consequence.

theorem Flypitch.fol.satisfied_of_mem {L : Language} {T : Set (formula L)} {f : formula L} (hf : f ∈ T) : T ⊨ f

Any member of a theory is a semantic consequence of that theory.

theorem Flypitch.fol.all_satisfied_of_subset {L : Language} {T T' : Set (formula L)} (h : T' ⊆ T) : all_satisfied T T'

Semantic consequence is monotone in the conclusion set.

theorem Flypitch.fol.satisfied_trans {L : Language} {T₁ T₂ : Set (formula L)} {f : formula L} (h₁₂ : all_satisfied T₁ T₂) (h₂f : T₂ ⊨ f) : T₁ ⊨ f

Semantic consequence composes transitively.

theorem Flypitch.fol.all_satisfied_trans {L : Language} {T₁ T₂ T₃ : Set (formula L)} (h₁₂ : all_satisfied T₁ T₂) (h₂₃ : all_satisfied T₂ T₃) : all_satisfied T₁ T₃

Pointwise semantic consequence composes transitively.

theorem Flypitch.fol.satisfied_weakening {L : Language} {T T' : Set (formula L)} (h : T ⊆ T') {f : formula L} (hTf : T ⊨ f) : T' ⊨ f

Weakening assumptions preserves semantic consequence.

theorem Flypitch.fol.formula_soundness {L : Language} {Γ : Set (formula L)} {A : formula L} (h : Γ ⊢ A) : Γ ⊨ A

Every derivable formula is semantically valid from the same assumptions.