Negation closure of a set of formulas

Fragment.negationClosure S is the smallest fragment containing S that is also closed under formal negation φ ↦ φ.not. It is an external syntactic operator on sets, placed beside Fragment.generated: Fragment itself gains no field, in keeping with the frozen fragment audit, which keeps formal-negation closure out of the structure. Fragment.NegationClosed is the corresponding predicate on fragments.

Countability is by the same finite-path encoding as Fragment.generated, with one extra step tag for negation (private scaffolding; only negationClosure_countable is published).

def FirstOrder.Language.Fragment.NegationClosed {L : Language} (A : L.Fragment) : Prop

A fragment closed under formal negation.

Equations

• A.NegationClosed = ∀ {n : ℕ} {φ : L.BoundedFormulaω Empty n}, ⟨n, φ⟩ ∈ A → ⟨n, φ.not⟩ ∈ A

theorem FirstOrder.Language.Fragment.negationClosed_top {L : Language} : top.NegationClosed

inductive FirstOrder.Language.Fragment.NegationClosedFrom {L : Language} (S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) : (n : ℕ) × L.BoundedFormulaω Empty n → Prop

Component-and-negation closure of a set of formulas, as an inductive reachability predicate: the rules of GeneratedFrom plus formal negation.

• base {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {p : (n : ℕ) × L.BoundedFormulaω Empty n} (h : p ∈ S) : NegationClosedFrom S p
• imp_left {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {n : ℕ} {φ ψ : L.BoundedFormulaω Empty n} : NegationClosedFrom S ⟨n, φ.imp ψ⟩ → NegationClosedFrom S ⟨n, φ⟩
• imp_right {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {n : ℕ} {φ ψ : L.BoundedFormulaω Empty n} : NegationClosedFrom S ⟨n, φ.imp ψ⟩ → NegationClosedFrom S ⟨n, ψ⟩
• all_body {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {n : ℕ} {φ : L.BoundedFormulaω Empty (n + 1)} : NegationClosedFrom S ⟨n, φ.all⟩ → NegationClosedFrom S ⟨n + 1, φ⟩
• iInf_comp {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {n : ℕ} {φs : ℕ → L.BoundedFormulaω Empty n} (k : ℕ) : NegationClosedFrom S ⟨n, BoundedFormulaω.iInf φs⟩ → NegationClosedFrom S ⟨n, φs k⟩
• iSup_comp {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {n : ℕ} {φs : ℕ → L.BoundedFormulaω Empty n} (k : ℕ) : NegationClosedFrom S ⟨n, BoundedFormulaω.iSup φs⟩ → NegationClosedFrom S ⟨n, φs k⟩
• neg {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {n : ℕ} {φ : L.BoundedFormulaω Empty n} : NegationClosedFrom S ⟨n, φ⟩ → NegationClosedFrom S ⟨n, φ.not⟩

def FirstOrder.Language.Fragment.negationClosure {L : Language} (S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) : L.Fragment

The negation closure: the smallest negation-closed fragment containing S.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.Fragment.subset_negationClosure {L : Language} (S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) : S ⊆ (negationClosure S).toSet

theorem FirstOrder.Language.Fragment.negationClosed_negationClosure {L : Language} (S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) : (negationClosure S).NegationClosed

theorem FirstOrder.Language.Fragment.generated_le_negationClosure {L : Language} (S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) : generated S ≤ negationClosure S

theorem FirstOrder.Language.Fragment.negationClosure_le {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {A : L.Fragment} (hSA : S ⊆ A.toSet) (hA : A.NegationClosed) : (negationClosure S).toSet ⊆ A.toSet

The negation closure is below every negation-closed fragment containing S.

theorem FirstOrder.Language.Fragment.negationClosure_toSet_eq {L : Language} {A : L.Fragment} (hA : A.NegationClosed) : negationClosure A.toSet = A

A negation-closed fragment is its own negation closure.

Countability: the closure-path encoding

closureStep extends componentStep by the tag 5 for negation; the rest is the argument of Fragment.generated_countable verbatim. The scaffolding is private: only negationClosure_countable is consumed.

theorem FirstOrder.Language.Fragment.negationClosure_countable {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (hS : S.Countable) : (negationClosure S).toSet.Countable

Countability: the negation closure of a countable set is countable.