Positive occurrences of transitive closure

TC.Positive φ s holds when every closure operator of φ occurs at polarity true when φ itself occurs at polarity s, with negation flipping the polarity. Sentences with TC.Positive φ true form the FO(positive TC) fragment of [Imm87], Section 3, written with negations pushed through by polarity: a closure may occur under an even number of negations. TC.width φ is the largest tuple width of a closure in φ.

This is a polarity of closure operators. It is unrelated to the polarity of relation variables checked by Operator.Formula.checkPolarity.

Main definitions

• Cslib.Logic.FO.TC.Positive: closures occur positively.
• Cslib.Logic.FO.TC.width: the largest closure tuple width.

Main results

• Cslib.Logic.FO.TC.positive_relabel, Cslib.Logic.FO.TC.positive_exs: renaming free variables and quantifying a block of them preserve closure polarity.

References

• N. Immerman, Languages That Capture Complexity Classes, Section 3

def Cslib.Logic.FO.TC.Positive {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} : Operator.Formula L shape Γ α → Bool → Prop

Positive φ s: every closure operator of φ occurs at the polarity true when φ itself occurs at polarity s; negation flips the polarity.

def Cslib.Logic.FO.TC.width {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} : Operator.Formula L shape Γ α → ℕ

The largest width of a closure operator in a formula.

@[simp]

theorem Cslib.Logic.FO.TC.positive_relabel {L : FirstOrder.Language} {Γ : List ℕ} {α β : Type w} (g : α → β) (φ : Operator.Formula L shape Γ α) (s : Bool) : Positive (Operator.Formula.relabel g φ) s ↔ Positive φ s

Renaming free variables does not change the polarity of closure operators.

@[simp]

theorem Cslib.Logic.FO.TC.positive_exs {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} (n : ℕ) (φ : Operator.Formula L shape Γ (α ⊕ Fin n)) (s : Bool) : Positive (Operator.Formula.exs n φ) s ↔ Positive φ s

Quantifying a block of variables does not change the polarity of closure operators.