Negation-closed fragments of L_{ω₁ω}

A fragment of L_{ω₁ω} is negation-closed when the negation of each member is a member. The syntax has no formal negation: ¬φ is φ.imp ⊥. Since a fragment is closed under components, a negation-closed fragment contains ⊥ at every arity at which it has a member, but at no other arity: no ⊥ is added unconditionally. In particular the empty fragment is negation-closed, and the negation closure of the empty set is empty.

The negation closure of a set S of formulas is the least negation-closed fragment containing it. It contains, for instance, the iterated negations ¬φ, ¬¬φ, … of each member φ of S and of its components. Unlike the formation closure, the negation closure adds no atomic formulas, so the negation closure of a countable set is countable over every language, however many symbols it has.

Main definitions

• FirstOrder.Language.Fragment.NegationClosed: a fragment containing the negation of each member.
• FirstOrder.Language.Fragment.negationClosure: the least negation-closed fragment containing a set of formulas.

Main results

• FirstOrder.Language.Fragment.NegationClosed.not_mem_iff: in a negation-closed fragment, a negation is a member exactly when the formula is.
• FirstOrder.Language.Fragment.NegationClosed.bot_mem: a negation-closed fragment contains ⊥ at the arity of each member.
• FirstOrder.Language.Fragment.negationClosure_le_iff: leastness of the negation closure.
• FirstOrder.Language.Fragment.negationClosure_empty: the negation closure of the empty set is the empty fragment.
• FirstOrder.Language.Fragment.negationClosure_countable: over any language, a countable set has a countable negation closure.

References

• D. Marker, Lectures on Infinitary Model Theory, Cambridge University Press, 2016, Chapter 1.

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

A fragment is negation-closed when the negation of each member is a member.

• not_mem {n : ℕ} {φ : L.BoundedFormulaω Empty n} : ⟨n, φ⟩ ∈ A → ⟨n, BoundedFormulaInf.not φ⟩ ∈ A

  The negation of a member is a member.

@[simp]

theorem FirstOrder.Language.Fragment.NegationClosed.not_mem_iff {L : Language} {A : L.Fragment} (hA : A.NegationClosed) {n : ℕ} {φ : L.BoundedFormulaω Empty n} : ⟨n, BoundedFormulaInf.not φ⟩ ∈ A ↔ ⟨n, φ⟩ ∈ A

In a negation-closed fragment, a negation is a member exactly when the formula is.

theorem FirstOrder.Language.Fragment.NegationClosed.bot_mem {L : Language} {A : L.Fragment} (hA : A.NegationClosed) {n : ℕ} {φ : L.BoundedFormulaω Empty n} (h : ⟨n, φ⟩ ∈ A) : ⟨n, ⊥⟩ ∈ A

A negation-closed fragment with a member of arity n contains ⊥ at arity n.

theorem FirstOrder.Language.Fragment.negationClosed_bot {L : Language} : ⊥.NegationClosed

The empty fragment is negation-closed.

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

The top fragment is negation-closed.

theorem FirstOrder.Language.Fragment.NegationClosed.sInf {L : Language} {𝒜 : Set L.Fragment} (h : ∀ A ∈ 𝒜, A.NegationClosed) : (InfSet.sInf 𝒜).NegationClosed

An intersection of negation-closed fragments is negation-closed.

theorem FirstOrder.Language.Fragment.NegationClosed.inf {L : Language} {A B : L.Fragment} (hA : A.NegationClosed) (hB : B.NegationClosed) : (A ⊓ B).NegationClosed

The intersection of two negation-closed fragments is negation-closed.

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

The negation closure of a set of formulas: the least negation-closed fragment containing it.

theorem FirstOrder.Language.Fragment.mem_negationClosure {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {p : (n : ℕ) × L.BoundedFormulaω Empty n} : p ∈ negationClosure S ↔ ∀ (A : L.Fragment), A.NegationClosed → S ⊆ ↑A → p ∈ A

A formula belongs to the negation closure of S exactly when it belongs to every negation-closed fragment containing S.

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

The negation closure is negation-closed.

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

A set of formulas lies in its negation closure.

theorem FirstOrder.Language.Fragment.negationClosure_le_iff {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {A : L.Fragment} (hA : A.NegationClosed) : negationClosure S ≤ A ↔ S ⊆ ↑A

Leastness. The negation closure of S lies below a negation-closed fragment exactly when S does.

theorem FirstOrder.Language.Fragment.negationClosure_mono {L : Language} {S T : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (h : S ⊆ T) : negationClosure S ≤ negationClosure T

The negation closure is monotone.

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

The fragment generated by S lies below its negation closure.

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

A negation-closed fragment is its own negation closure.

@[simp]

theorem FirstOrder.Language.Fragment.negationClosure_empty {L : Language} : negationClosure ∅ = ⊥

The negation closure of the empty set is empty: no ⊥ is added at an arity without a member.

Countability of the negation closure

The negation closure of S is the union of countably many stages: start from S, and at each stage add the negations of the members of the previous stage, closing under components. Each stage of a countable set is countable, whatever the language, since generating a fragment preserves countability.

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

Countability. The negation closure of a countable set of formulas is countable, over any language.